RE: SUO: Re: IFF Comments Requested
Re (Hayes):
> Well, if so, I'm tempted to ask, why is FOL offered as the basic
> axiomatization of topos theory for foundational reasons in the IFF
> document?
Indeed. Here is a proper concern -- the relations between FOL models and
theories, and topoi, and the distinction between theory and metatheory. I'd
like to see more exposition in the IFF about these matters.
From Goldblatt, Topoi (the Categorial Analysis of Logic), P. 287:
"... the concept of 'elementary topos' is co-extensive with that of 'model
for many-sorted higher-order intuitionistic free logic'..."
From Fourman, "The Logic of Topoi" (in Barwise, ed., Handbook of
Mathematical Logic):
"The purpose of this chapter is to give an expository presentation of the
correspondence between topoi and theories which makes precise Lawvere's
claim that 'the notion of topos summarises in objective categorical form the
essence of 'higher-order logic''."
Jay
> -----Original Message-----
> From: Pat Hayes [mailto:phayes@ai.uwf.edu]
> Sent: Wednesday, October 10, 2001 9:44 AM
> To: Leo Obrst
> Cc: standard-upper-ontology@ieee.org
> Subject: Re: SUO: Re: IFF Comments Requested
>
>
>
> > >
> >> Sixth. Let me back off from having FOM fun with y'all and
> get to the
> >> main point. The purpose of ontologies is to represent facts about
> >> worlds, not to play elegant games in the foundations of
> mathematics.
> >> Matthew West wants to describe oil flowing along
> pipelines, that kind
> >> of thing. Now, what connection, even of the most remote
> kind, can you
> >> suggest there is going to be between ANY such activity of
> describing
> >> the real world, and ANY of this mathematical gamesmanship of topos
> >> theory? So far, I can't see any.
> >
> >I think you are wrong, here, Pat. No, we are not here to play
> >mathematical games, but really do have pragmatic concerns
> just exactly
> >like Matt does.
>
> I'm sure you are: I didn't mean to criticize your motives,
> only your document.
>
> >However, we do need to build a framework which enables
> >us to cobble together different ontologies (theories) in a reasonable
> >fashion and perhaps even a framework to enable us to
> "compose" theories,
> >i.e., to be able to "place" theories in an overarching framework and
> >then link or (God help us) even "project" those theories'
> >"intersections". If we don't do this, who will? Personally, I think
> >category theory will help.
>
> Ah, now THAT does make sense. BUt this seems to be quite a different
> theme than the one in the IFF document. What you are saying here is
> that the category theory can provide a framework for a kind of
> structural meta-theory of ontologies; for talking about structural
> relationships between ontologies, as is done in the SpecWare system
> also. That isn't what the IFF seems to be saying at all, though: it
> is talking about categories being the *subject-matter* of ontologies.
> For example, your picture of categories in the structural meta-theory
> is quite compatible with the ontologies themselves being written in,
> say, DAML and being about, say, states of viscosity of different
> grades of crude oil.
>
> >
> >I intend to discuss your issues a bit further (and later),
> since I don't
> >see any incongruity between the "logic" view and the
> "category theory"
> >view. The category theory view is simply more general.
>
> Well, if so, I'm tempted to ask, why is FOL offered as the basic
> axiomatization of topos theory for foundational reasons in the IFF
> document?
>
> Pat
> --
> ---------------------------------------------------------------------
> IHMC (850)434 8903 home
> 40 South Alcaniz St. (850)202 4416 office
> Pensacola, FL 32501 (850)202 4440 fax
> phayes@ai.uwf.edu
> http://www.coginst.uwf.edu/~phayes
>
>
>