Equality; higher order KIF/CGs

fritz@rodin.wustl.edu (Fritz Lehmann)
Reply-To: cg@cs.umn.edu
Date: Fri, 8 Oct 93 08:10:59 CDT
From: fritz@rodin.wustl.edu (Fritz Lehmann)
Message-id: <9310081310.AA15617@rodin.wustl.edu>
To: phayes@cs.uiuc.edu
Subject: Equality; higher order KIF/CGs
Cc: boley@dfki.uni-kl.de, cg@cs.umn.edu, chrikey1.ucthpx@f4.25.fidonet.org,
        interlingua@isi.edu


Dear Pat Hayes,              phayes@cs.uiuc.edu

	Thanks for describing to me the reduction of 
equality-definition to First-Order via a finite schema 
made of "Relation-symbol X Argument-place" instances, 
depending on a finite vocabulary of available 
relation-symbols.  This seems like an unappealing 
kludge which nonetheless works for some systems.
But there's no solace for me in relying on a finite 
vocabulary of relation-symbols in the syntax to make
semantics (for equality or anything else) First Order.
As soon as you allow what I require for KRep, and what 
ordinary discourse already uses (relations among 
relations, and among different-ordered relations, 
and individuals), then an infinite zoo of these 
relation-symbols springs up.  This even in a universe
having just two atomic 'individuals' and without allowing 
singletons or empties in the models.  Forms are:  a; b; 
R(a,b); R'(a,R); R''(b,R,R'); etc.  Of course this
begs the original logic-order question.
And it looks similar to your description 
of nested formulae in "beta-conversion" -- have you a
reference for this?

	(I say infinite rather than transfinite since 
I still balk at diagonalization and all its progeny.)

	When an email message gets no answer I 
never know whether it was too boring, too lame to warrant a 
response, or too convincing to question.  It may just 
be that frank discussion of KIF occurs in a more exclusive 
email forum than Interlingua.  I recommend higher-
order KIF and Conceptual Graphs for practical convenience. 
Suppose there were some decent reduction to First Order 
via types, schemas, Henkin or what-not (though I doubt it); 
then perhaps the handy higher-order and mixed-order 
constructs which people need could be "syntactic 
sugar", as long as the semantics is done _right_.
(An uninterpreted "holds(p,x)" relation/link won't do.)
But give us these constructs, _with_ semantics, dumping
decidability if necessary.    [A similar point was reached
by the KL-ONErs on tractability (and decidability too); even 
purists have now dumped worst-case tractability of 
subsumption, to let people actually say what they 
want to say.  Tractability is good for getting a 
PhD, though.]

	At present, KIF and CGs are unable even to 
express -- with semantics -- Peirce's (or 
Leibniz's) basic sentence: "Given any two things, 
there is some character which one posseses and the 
other does not."  Poignant, since all the First-Order
model theory of KIF and CGs depends on there being 
such distinct things.  I don't know whether the CYC 
Epistemological Language can say it.

	It could simply be that the major KIF players 
decided on limiting KIF's logic to First-Order a 
long time ago and "the deal is done" (although, if 
so, one should wonder at their openness to the 
nonmomonotonic stuff).  An interlingua should be grounded 
on classical logic, but classical logic is n-adic, n-order.

                       Yours truly, Fritz Lehmann
                           fritz@rodin.wustl.edu
4282 Sandburg, Irvine, CA 92715    714-733-0566