Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

SUO: Re: IFF Thread 1: Why Category Theory?


¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

AP = Adam Pease
JF = Jim Farrugia

AP: Maybe at this point you and Robert could revisit
    the message I sent on Aug 20:

    http://suo.ieee.org/email/msg06027.html

    to which Robert ultimately replied that he didn't have time to answer:

    http://suo.ieee.org/email/msg06380.html

    Robert had provided an example of using IFF to formalize
    a set of English statements.  I did the same formalization
    in SUO-KIF alone, and concluded that IFF did not offer any
    formal content that could be used in practical inference.
    I would welcome specific rebuttal.

JF: Many of the 32 messages from our recent first round of comments on the IFF
    starter documents dealt with the topic "Why Category Theory" for the IFF.

JF: Please consider this new thread a vehicle for continuing a focused
    discussion on that topic.

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤

Jim,

A few recommendations:

1.  Category theory is an 'alternative' foundation for doing mathematics.
    It was designed to capture many aspects of the way that most working
    mathematicians actually do and think about mathematics and to formalize
    what they had been doing all along.  It is optimized for actually doing
    mathematics and for discovering new stuff.  It was invented by folks who
    were unhappy with the way that formalisms like FOL and set theory got in
    the way of actually doing and discovering new mathematics.  Set theory and
    FOL are not good for doing or for discovering mathematics -- at best they are
    good for writing up the results of what one customarily achieves some other way.

2.  Trying to embed category theory in FOL,
    much less in the innards of KIF, well,
    you saw 'Alien' did you not?

3.  This style of "formalizing" natural language propositions, say,
    "Orpheus loves Eurydice" as "There exists an instance of loving
    in which Orpheus is the lover and Eurydice is the lovee", has
    been lambasted in the logical, linguistic, cognitive science,
    and AI literatures for as long as I can remember, and I am
    amazed, well, not so much anymore, to see it rearing its
    ugly head here again.  Don't go there.  And no, I do not
    have time to be doing other folks' homework for them.

Jon Awbrey

¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤