Re: Equality; higher order KIF/CGsphayes@cs.uiuc.edu
Date: Tue, 12 Oct 1993 14:56:05 +0000
To: firstname.lastname@example.org (Fritz Lehmann)
Subject: Re: Equality; higher order KIF/CGs
Cc: email@example.com, firstname.lastname@example.org, email@example.com,
> 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.
Well it might not be very attractive, but it always works, and its the
'standard' way to axiomatise equality in first order. Of course one can
always summarise it in a schema (Leibnitz law) to make it look neater, but
that still doesnt take one even to second-order order logic, since this
schema is always equivalent to a finite set of its instances.
Heres why beta-reduction is so different. This schema has roughly this form:
(lambda x. PHI[x])(t) IFF PHI[t]
for any wff PHI and term t. This has as instances expressions in which PHI
can be as complicated a first-order expression as one likes, including
inner bound variables etc etc., so this inference, say, is justified by it:
(lambda x. (IF (Exists y)R(x,y) THEN f(x)=f(f(x)) ))(g(a))
If one sets out to find a first-order theory which emulates
lambda-conversion, no matter how ingenious the notation invented, even
allowing such things as a function-name generating faculty, there isnt any
finite collection of first-order axioms from which all the instances of
this schema can be inferred.
This is a fairly profound difference between two kinds of schema, I think:
although lambda-conversion and Leibnitz' law are both usually written as
schemata and can be quickly stated as higher-order assertions, one is much
more essentially higher-order than the other. The equality schema is a
convenient way of writing an essentially first-order intuition, but
lambda-conversion is fundamentally beyond first-order quantification
I dont have any references for this intuition, it came to me years ago
while thinking about higher-order theoremproving (which was at one time a
very hot topic). If anyone has any comments or pointers to this idea in the
logical literature I would be very interested.
>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.
Yes. And I have a little doubt. While I agree that it often seems natural
to use R' and even sometimes R'', can you find a singe plausible excuse for
R''', let alone R'..(50)..', say? I'm bothered by the way that letting
recursion loose creates so many wildly implausible schemes when we really
only wanted three, or maybe two, of them. Maybe recursion was a little too
strong a tool to use?
>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.)
OK, I can also share a little balking. Why not say unbounded rather than
infinite, though? You dont have to get transfinite in order to insist that
infinite sets exist. And if you stay this side of infinite (along with
Herbrand) then why don't you admit that in fact things are always finite?
If you do, then Leibnitz law looks very first-order once again.
Incidentally, we can cope with the integers, or anything else that has a
recursive characterisation, without needing more than finitely many 1PC
instances of Leibnitz: once one has all the relation and
function-substitution instances, further instantiation (eg over the
relevant Herbrand universe) is just ordinary first-order.
(I know that such 1PC theories of the integers, say, have nonstandard
models. My attitude is: tough, thats the way life is! If one had
uncomputable resources available, one could eliminate these nonstandard
models. But one doesnt.)
My intuition is that while first-order quantification can be conceptualised
as shorthand for an infinite, or unbounded, conjunction, and has a certain
simplicity that it inherits from this intuition, higher-order
quantification unfortunately cant be thought of in this comfortable way.
This isnt obvious, and indeed was discovered this century, but its true.
The ordinary intuitions about quantification just don't extend past first
order. Thats why I am always suspicious that when someone tells me they
want higher-order quantifiers, they really mean first-order with
higher-order sugar on them. Im all in favor of the sugar, of course, for
languages that people have to use (contrast KIF), provided one doesnt
forget what one is really eating.
>..... 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.
Well, decideablity yes; but higher-order, taken seriously, takes us way
beyond that: completeness is impossible. Bear in mind what that really
means: that the set of truths is *uncomputable*. To claim that an
implemented system is based on a semantics relative to which computability
is provably impossible, seems to me to be just wishful thinking. You might
intend or hope that is what your expressions mean, but they don't, in fact.
Exactly what they do mean is an open question, but I bet that whatever it
is, it has a first-order description.
[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."
Well, they can say this, but only if one provides a theory of what
'characters' are. And that seems quite a reasonable requirement. Claiming
that you can say this in higher-order means that you are assuming that the
logic has this notion somehow built into it. Even that seems reasonable
until one knows about higher-order incompleteness and so forth, at which
point I tend to balk, and ask where the confidence comes from that one
really has captured this uncapturable semantics?
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
Nonmonotonic can be first order, thats orthogonal. The reason for taking
nonmon seriously is that there is ample evidence that people want to use
it, and it really *can't* be reduced to monotonic first-order logic.
>An interlingua should be grounded
>on classical logic, but classical logic is n-adic, n-order.
Depends on your classes ;-)
Beckman Institute (217)244 1616 office
405 North Mathews Avenue (217)328 3947 or (415)855 9043 home
Urbana, IL. 61801 (217)244 8371 fax
firstname.lastname@example.org or Phayes@cs.uiuc.edu