**Mail folder:**Interlingua Mail**Next message:**sowa: "Re: Equality; higher order KIF/CGs"**Previous message:**Fritz Lehmann: "You answered; they didn't"**Maybe in reply to:**phayes@cs.uiuc.edu: "Re: Equality; higher order KIF/CGs"**Reply:**sowa: "Re: Equality; higher order KIF/CGs"

Message-id: <199310121954.AA26200@dante.cs.uiuc.edu> Reply-To: cg@cs.umn.edu Date: Tue, 12 Oct 1993 14:56:05 +0000 To: fritz@rodin.wustl.edu (Fritz Lehmann) From: phayes@cs.uiuc.edu X-Sender: phayes@dante.cs.uiuc.edu Subject: Re: Equality; higher order KIF/CGs Cc: phayes@cs.uiuc.edu, boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@isi.edu

Hi Fritz > 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)) R(g(a),b) then f(g(a))=f(f(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 machinery. 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 >PhD, though.] Nyah, nyah. > 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 >nonmomonotonic stuff). 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 ;-) Pat ---------------------------------------------------------------------------- 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 hayes@cs.stanford.edu or Phayes@cs.uiuc.edu