Equality; higher order KIF/CGsfritz@rodin.wustl.edu (Fritz Lehmann)
Date: Fri, 8 Oct 93 08:10:59 CDT
From: firstname.lastname@example.org (Fritz Lehmann)
Subject: Equality; higher order KIF/CGs
Cc: email@example.com, firstname.lastname@example.org, email@example.com,
Dear Pat Hayes, firstname.lastname@example.org
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
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
4282 Sandburg, Irvine, CA 92715 714-733-0566