**Mail folder:**Interlingua Mail**Next message:**Harold Boley: "Re: Higher-order KIF & CGs"**Previous message:**Fritz Lehmann: "Re: Higher-order KIF & CGs"**Maybe in reply to:**Fritz Lehmann: "Re: Higher-order KIF & CGs"**Reply:**Harold Boley: "Re: Higher-order KIF & CGs"

Message-id: <199311032226.AA12544@dante.cs.uiuc.edu> Reply-To: cg@cs.umn.edu Date: Wed, 3 Nov 1993 16:28:55 +0000 To: fritz@rodin.wustl.edu (Fritz Lehmann) From: phayes@cs.uiuc.edu X-Sender: phayes@dante.cs.uiuc.edu Subject: Re: Higher-order KIF & CGs Cc: boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@isi.edu

Hi Fritz Let me repeat a parable. A student comes up and announces that he ('he' because this guy is going to turn out to be an idiot) has a invented a formalism - he has called it BIG - which is so expressive that he can describe Niagara Falls in it. Impressed, I ask him to show me, and I see: Very-Big(Niagara-Falls). I ask him what justifies his claim that 'Very-Big' means very big, and he says it does because he, the student, invented this logic, and so he gets to define the semantics, and he has decided that its just a *logical truth* of BIG that 'Very-Big' denotes the property of being very big. Thats part of the semantics. He shows me another page with things like 'Meaning("Very-Big") = lambda x. (x is very big)' written on it. Now, how is this different from the claims that a FOL user makes that, say, "and" denotes conjunction? The difference is that FOL comes with an apparatus for making inferences which can be shown to correspond to the semantics that is being claimed for it. That correspondence is a completeness theorem. Without such a correspondence - or some similar account of how deduction relates to meaning - claims that formal symbols mean something are no better than my student's claims about BIG. In particular, a user of higher-order logic may claim that their second-order quantifiers range over all predicates, but I see no reason to accept such a claim, since given any inferential apparatus they they could possibly define, I can consistently interpret their second-order quantifiers as being essentially first-order (ie Henkian). They might protest that this isnt what they meant, but my first-order interpretation will justify the same theorems, so they won't be able to cite me a counterexample. Any claim that a higher-order logic is *really* higher-order must be based on faith rather than reason. (What they might be able to do, should we become embroiled in a debate, is show me that on my interpretation there are nonstandard models of arithmetic, say. And I repeat, I believe that there ARE nonstandard models of arithmetic. I even know what some of them are like. I put them in the same category as space-filling curves and other such topological wierdos.(see PS note) You say that we can eliminate nonstandard numbers by n-order fiat, but that sounds to me like BIG.) Thats why I dont regard completeness theorems as mere technical curiosities. Also, I think your point about Godel sentences is misleading: thats not the same sense of completeness. Look rather at a minimal logical vocabulary of FOL. It is very small, consisting maybe of the symbols OR, NOT, FORALL. Incompleteness means that one or more of these isnt going to quite mean what is supposed to. Which one? There are some answers to this (for example, restricting the language to Horn clauses means that OR doesnt quite mean what it usually does), but by and large it is difficult to see how to damage completeness in a way which preserves much of the essential character of FOL itself. Take out negation, say, and you just don't have the same kind of language. Of course real systems will often be incomplete for all sorts of practical reasons. But these are almost always traceable to, as it were, failures to search all of the space. But inmcompleteness of the underlying representation language is a gap in the search space itself, which is a more serious matter. Your point about equality would be a good one except that we know neat ways to overcome the apparent lack of expressibility. Closed-world assumptions handle the 100 senators nicely, for example. One might object that this involves the use of apparently higher-order 'schemas' or some such in order to be compactly stated. But thats the point: such things really are only abbreviations of large numbers of first-order axioms, introduced for reasons of computational and expressive elegance. That is *not* the same as a genuine second-order quantifier, as the model theory tells us so eloquently. And the semantic analysis of these languages should reflect the actual use, not make grand aspirations to an extraordinary expressibility which is both unnecessary and computationally impossible. I was interested that when challenged to go above third order you cited category theory. Yes, I can believe that category theory might find some of the more rarified heights useful. I expected you to cite Montague at me, who also found himself using fourth and maybe fifth orders, and was concerned with down-to-earth matters of language comprehension. Montague was clearly using the lambda-abstraction of type theory as a computational tool, and was not concerned with the veracity of his model theory. I would be very interested to find out more about Ontek's use; is it in any way related to Montague? Look, I think we may be arguing past each other. If you wish to argue for the computational usefulness of lambda-conversion, then of course I will agree and point to LISP. You ask for 'REAL EXAMPLES' of the trouble caused by incompleteness. But that misses the point. The systems behave the way they do. Its the semantic accounts of them that make them incomplete or not. You can use beta-conversion and fourth-order schemas all you like, but its the claim that this is all higher-order logic and I have to think of these things as quantifiers over uncountable sets of predicates, and hence the semantics justifies asserting by fiat that there just are no nonstandard models of arithmetic, that sticks in my craw. For example, you say: 'I think it's perfectly clear what "character" means here; it means predicate.' But thats not good enough. The question at issue is how many predicates there are. For example, are there uncountably many predicates of the integers? Diagonalisation arguments would certainly suggest so, but now let me turn the tables on you and ask why I should believe in these things, most of which could never possibly be named or conceptualised. Until one plays with it for a while, it is hard to appreciate just what an extraordinarly unintuitive idea an 'uncountable set' really is. For example, suppose we let you somehow catalog an infinite number of them in a finite lifetime (so you could name every integer) you still wouldnt have begun to name all of these things. You can return to another life infinitely many times, and in each one of them you can name infinitely many of them again: you still have only named so few of them that the set remaining might be dense. Is *this* what you are claiming to have quantified over when you write (forall P) ? Best wishes Pat Hayes PS. It important to clear up one misunderstanding that even you seem to have. That there are nonstandard models of arithmetic doesnt change the actual process of *doing* arithmetic one jot, nor any processes of reasoning about arithemtical entities. It just means that we have to accept that, if challenged, we have to be creatures of this uncertain century and admit that we have no means of being absolutely certain that we have the real line pinned down. My remark about uncomputable resources was only to indicate that to claim that our arithmetical talk really *must* refer to artithmetic could only be justified, ultimately, if we could claim to have processed infinitely many sentences. PPS. Your point about the multi-adicity of KIF screwing up some of the conventional instantiation schemes is a good one, and I think more work needs to be done on this in general. I agree that this is expressively very useful and natural, but it has given rise to a number of annoying technical problems, and maybe it needs to be looked at more carefully. ---------------------------------------------------------------------------- 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