Re: Equality; higher order KIF/CGs

sowa <sowa@turing.pacss.binghamton.edu>
Reply-To: cg@cs.umn.edu
Date: Tue, 26 Oct 93 21:05:42 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9310270105.AA24976@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, phayes@cs.uiuc.edu
Subject: Re:  Equality; higher order KIF/CGs
Cc: boley@dfki.uni-kl.de, chrikey1.ucthpx@f4.25.fidonet.org,
        interlingua@isi.edu

Fritz and Pat,

I'm sorry that I haven't had time to respond to your discussions about
higher-order logic vs. first-order logic.  Perhaps I'll be able to give
a more detailed statement later, but let me make a couple of very brief
comments now:

 1. The CG syntax is capable of representing HOL, but I don't believe
    that there is any need to do so.

 2. FOL with explicit types or sorts can express everything that can be
    expressed in HOL, but the model theory does not give the same denotations
    if you limit the sorts to a finite or even countable number of individuals.

 3. But if you allow uncountable numbers of individuals in any sort, then
    you can capture exactly the same denotations that you would have in HOL.

 4. However, a language with an uncountable number of individuals in its
    sorts must somehow come to grips with the problem of naming or somehow
    identifying which one you are talking about.  And no language with a
    finite alphabet can generate more than a countable number of names.

 5. In any case, the metalanguage facilities of both KIF and CGs provide
    sufficient resources to define any countable number of new constructs,
    rules of inference, axiom schemata, etc.  In particular, the rules of
    lambda conversion can easily be formulated as metalanguage expressions
    in either KIF or CGs.

 6. Natural language statements about X and Y having or not having the same
    properties, attributes, characters or whatever are not formal statements
    in HOL.  If you can formalize them, I'll show you how to translate your
    HOL statements into a sorted FOL.

Bottom line:  I would love to see anyone come up with a serious kn. rep.
problem that can be formalized in HOL, but not in the version of KIF/CG
semantics that we are providing.  (And by serious, I rule out things
that presuppose uncountable garbage, since as I have said many times,
I have grave doubts that any such things exist.)

John