Re: SUO: Vote 2001-02: IFF Foundation Ontology
Yang, Chris is right about this. Category theory is NOT the "dominant
underpinning to formal semantics
over the past 30 years". Set theory and model theory are (based on set
theory). It may however change in the future.
Chris, I don't think the response will highlight a shortcoming in logic;
instead it will be along the lines of something equivalent to logic but
more general.
In fact, though I don't have a quick answer, you might look at an older
text: J.Lambek and P.J.Scott's Introduction to Higher Order Categorical
Logic, 1986, Cambridge U. Press. It tries to explicitly reconcile logic
and category theory. I can't say I've ever gotten through the entire
text myself, but it's useful. There are some deep connections between,
for example, Cartesian closed categories and the typed lambda calculus,
and topoi and certain logics.
I can relate a bit of my experience (those easily bored, delete and move
on), on how I approached category theory. Originally I investigated
categorial grammar in linguistics, found it rather ad hoc logically,
though of course it was based on Montague and Bar-Hillel in general: but
why forward function application, etc., though they intuitively feel
good? Then I read Moortgat, 1988, who tried to formalize a Generalized
Categorial Grammar based on the Lambek calculus (yes, the same Lambek as
above), give it a logical formulation (Lambek's original was a syntactic
calculus). I liked Moorgat's work, based my dissertation's formal
underpinnings on it: I was mainly interested in logical semantics. And
so I went back and read Lambek, tried to track the subsequent
literature, discovered that category theory was kind of busting out in
theoretical computer science, including the denotational semantics of
programming languages. So, in 1994-95, at Boeing we did a self-study on
category theory for a year (on our lunch hours). At the end of that
year, we covered basic category theory and its applications such as the
typed lambda calculus, den. semantics, etc. There were five of us: a
math Ph.d, and three others who had undergrad backgrounds in math and
cs. At the end, all were writing proofs in category theory. 2 of the
three later went for math. degrees (since they liked it so much): one an
MS, another a PhD.
Category theory is a general theory on the level of set theory, but is
focused on structure purely. You might also look at the Barwise and
Seligman book: Information Flow Theory. This is what Bob Kent's IFF is
based on: an application of category theory. I noted Bob's work a few
years ago, when he was developing OML and CKML, much prior to DAML,
etc., for ontology representation and thought it good. I still do. It
still seems to me the best way to represent semantic mappings, i.e., for
ontology integration. The Barwise and Seligman book will help here.
So, it's hard but understandable. In 20 years, it will probably be like
set theory is today. Available tools? Not much: Specware and comparable
Kestrel Institute tools, databases of defined categories for
mathematicians.
Leo
Chris Menzel wrote:
>
> Yang Yun wrote:
> > - Received 2001-02: IFF Foundation Ontology
> >
> > - I vote YES that this group should commence work on IFF Foundation
> > Ontology.
> >
> > Comments:
> >
> > Category theory is the dominant underpinning to formal semantics
> > over the past 30 years.
>
> I think that is inaccurate, at least if you are using the term "formal
> semantics" in the way that it is used among linguists, logicians, and
> philosophers. The dominant underpinning of formal semantics since it
> was invented has been, and, I believe, remains, standard set theory.
> Category theory -- which, I agree, is elegant and powerful, and can also
> serve as a foundation for formal semantics -- is not even mentioned in
> standard introductory texts in logic or formal linguistic semantics, and
> is used spottily at best -- when a category theoretic representation
> proves particularly vivid -- in more advanced texts on formal model
> theory like Chang & Keisler and Hodges.
>
> Me, I don't care. I'm all for using whatever framework is most powerful
> and appropriate. But can you, or anyone, provide us with one concrete
> example of a shortcoming in the traditional framework of first-order
> syntax, proof theory, and model theory that would necessitate moving to
> a framework as abstract and (to most) unfamiliar as category theory?
>
> -chris
>
> --
>
> Christopher Menzel # web: philebus.tamu.edu/~cmenzel
> Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
> College Station, TX 77843-4237 # vox: (979) 845-8764
--
_____________________________________________
Dr. Leo Obrst The MITRE Corporation
mailto:lobrst@mitre.org Intelligent Information Management/Exploitation
Voice: 703-883-6770 7515 Colshire Drive, M/S W640
Fax: 703-883-1379 McLean, VA 22102-7508, USA