**Mail folder:**Interlingua Mail**Next message:**phayes@cs.uiuc.edu: "Re: Higher-order KIF & CGs"**Previous message:**sowa: "Re: Equality; higher order KIF/CGs"**Maybe in reply to:**Fritz Lehmann: "Higher-order KIF & CGs"**Reply:**phayes@cs.uiuc.edu: "Re: Higher-order KIF & CGs"

Reply-To: cg@cs.umn.edu Date: Mon, 1 Nov 93 01:16:17 CST From: fritz@rodin.wustl.edu (Fritz Lehmann) Message-id: <9311010716.AA28631@rodin.wustl.edu> To: phayes@cs.uiuc.edu Subject: Re: Higher-order KIF & CGs Cc: boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@isi.edu

Dear Pat Hayes: Discussing logic-order for KIF may be moot -- I don't know to what degree KIF is open to change. On one hand the initiators of KIF have pretty much settled on a first-order logic in LISP syntax. On the other hand the very few attempted "users" of KIF have squawked about its shortcomings and there have been no public responses (on this INTERLINGUA email list at least) nor announced corrective modifications in the language. Some Conceptual Graphs people (like Guy Mineau) have extended CGs to higher-order a la Gruber's Ontolingua, but I believe they have been limited to Sowa's (apparently uninterpreted) reifying of predicates/relations into individuals. You've raised pure mathematical concerns about using higher- order logic as a basis for an interlingua. I am concerned with practical, finite transmission of knowledge and concept-systems between real-world knowledge bases. This means that although human readablitiy may be a low priority, feasibility of expression ("machine elegance") is a high priority. That's what higher-order logic is good at. The fact that some construct may be reducible to a first-order semantics using, say, an equivalent countable number of first-order sentences (running over some available vocabulary) may be of interest to the mathematical logician but if this requires a corresponding effort in pure KIF then KIF fails. If every mention of 100 senators required (as in first-order logic) 4,950 explicit inequality statements between senators, that too would be a failure. So if there is some ingenious but far-fetched reduction to FOL, then _serious_ "syntactic sugar" is essential in the basic language definition. If not, then we need the real higher-order model- theoretic semantics. I wonder how broadly the epithet "sugar" may be construed. If one "sugar" sentence substitutes for an infinite (or indefinite or even intractably high) number of pure KIF/CG base sentences, I don't think I'll call it "sugar" any more. That's protein. Certainly such constructs need to be included in the "base model" of any useful interlingua. >> 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. Pat, I don't know that it would "always work" for KIF since KIF 3.0 allows an indefinite number of argument-places for a single relation. A relation need not have fixed "rank" or "arity" so "Relation X Argument-place" is not defined. Incidentally, I commend KIF for this excellent poly-arity feature which is a big improvement over Relational and Universal Algebra. It was adapted from LISP constructions like (AND X Y Z W Q) where the number of conjoined arguments is indefinite. Its usefulness is not restricted to commutative/symmetric operators/relations: consider (CYCLE X Y Z W Q) where the arguments are arrows drawn on a map. Also I think this means that my earlier suggestion for the model-theory, that the domain be "closed under direct product," needs to be modified to "closed under disjoint unions of direct products." >Heres why beta-reduction is so different. > [explanation omitted] >The equality schema is a >convenient way of writing an essentially first-order intuition, but >lambda-conversion is fundamentally beyond first-order quantification >machinery. Good. If beta-reduction of a lambda sentence has use in the practical world, then this is just another reason for using a true higher-order Krep language. I won't accede to your "essentially first-order" above for equality since, in your schema-method, a happenstance feature of _our_ syntax (finite vocabulary) determines a real feature of the _world's_ semantics (identity of differently qualified individuals). I'd rather say that individual equality/identity is essentially higher-order, but representable by a first-order schema kludge in systems with fixed finite vocabularies and arities. [A class identity like the identity in geometry of "equiangular triangles" and "equilateral triangles" has nothing to do with our finite vocabularies.] >>an infinite zoo of these >>relation-symbols springs up. >> . . .Forms are: a; b; >>R(a,b); R'(a,R); R''(b,R,R'); etc. >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? I haven't considered 50 levels, but I've thought about: when is it fruitless to consider more levels? R''' is indeed used: in category theory, one R''' is to R as the role of an object in a morphism is to a natural transformation. This reminds me of a maxim of mine: the smarter you are, the higher the order of your logic. Category theorists pride themselves on proofs using natural transformations as opposed to getting the same result using functors, or, worse, (ugh) sets of actual morphisms. I don't know whether they've ascended beyond natural transformations of functors of morphisms of objects, but I suspect so. The limit in the comprehensible number of levels appears to be a matter of unfortunate human mental limitation (which can be overcome -- with difficulty!) rather than a fundamental barrier. In precisely the same vein, Banach said "Good mathematicians see analogies between theorems or theories. The very best ones see analogies between analogies." Similarly, I vaguely recall that Ontek, Inc.'s manufacturing ontology system (a competitor of CYC created with the advice of Peter Simons and other ontological philosophers) uses 4th-order predicates. Perhaps they would not like to be stuck with a merely first-order communication language. >... 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.) That's real dedication to first-order-ism -- like a dog which loves its leash. I don't know if even Martin Davis, who always lobbies for first-order-ism, would go so far. If real-world users were told that KIF or Conceptual Graphs required them to have mysterious nonstandard numbers "outside" the real number line, they'd rebel. (They may not appreciate that the reals are just "dust" with plenty of room for nonstandard infinitesimals!) In truth, for interlingua purposes, we should take numbers as indefinable primitives: no Peano, no Princ.Math., no Goedel, no nuttin. I don't see what "uncomputable resources" has to do with purely formal semantics -- I gather from your whole discussion that model-theoretic semantics is provided for an interlingua only to be clear about what is meant in the abstract, without any assumption that we actually have to be able to compute every underlying Tarskian structure. We are not necessarily talking about _computation_ at all, just a communiction language with formal model-theoretic semantics. We can eliminate nonstandard numbers by (n-order) fiat. >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. Not just "people ...(contrast KIF)." Machines need "sugar" too, given your broad (logician's) definition of sugar -- see my comment above re "machine elegance". You allude nebulously to the pitfalls of true higher-order logic, but I suspect these turn out to be either A. loss of completeness and compactness, which are practically dispensable, or B. genuine but in fact desirable changes in semantics. You say: >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. I repeat my original comments to the INTERLINGUA list: "The usual objections to higher-order logic are that it is undecidable, uncompact, lacks the 0-1 property, etc. These are extraneous theoretical matters . . . They have no practical importance for transmission of descriptions of real-world entities. . . . We need to transmit finite taxonomies and descriptions of real-world things and laws and relations, in large but finite domains, ideally with the full (logical) expressiveness of very careful and precise natural language. . . . It's not enough to say "I like my logic to have formal completeness" -- demonstrate the practical penalty of incompleteness (in real world AI communication among our finite computers) or what ever else ails you about n-order logic." No-one has yet made the case that formal completeness has any practical importance for communicating knowledge systems. Give us REAL EXAMPLES of trouble caused by incompleteness. Incompleteness arises for example from the ability of a language to predicate a number which "corresponds" to the sentence doing the predicating. Or to a Turing Machine unknowingly describing itself. Skipping technicalities -- only a tiny proportion of the sentences in an undecidable language (or programs in a Turing Machine) are interpretable as self-referential and hence undecidable. [I don't necessarily mean this asymptotically.] The shortest undecidable sentence (program) is normally extremely long. It seems unlikely ever to be encountered in AI or Knowledge-base communication, unless by design. Can you clarify in plain, practical terms why completeness is really important for communicating Krep systems? (If you really think so.) You say "the set of truths is *uncomputable*" Yes, but so what? >> 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? I think it's perfectly clear what "character" means here; it means predicate. It asserts the existence of some predicate of an individual, so it's second-order. Current KIF/CG can't say it (with meaningful formal semantics). The sentence is in fact central to descriptions of relational databases. Your dire warning of "higher- order incompleteness and so forth" seems again like a shibboleth. This just one of umpteen potentially useful higher-order examples one could think of. Here's another: "All monotonic functions of 42 have positive values." Not very exotic -- but can anyone express it correctly in KIF? Or in Conceptual Graphs based on Sowa's existing phi-operator? >Nonmon 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. Yes it's orthogonal. (Digressing hopelessly, I know of no evidence whatsoever that "people want to use" nonmonotonic logics. They want to deal with conflicting information; since when do they demand new logics? Admittedly there are plenty of people around who want to _invent_ new logics. Things that belong in the deep theory/ontology are crammed into these "logics". But I don't want to talk about this can of worms here. One can at a time.) At first you seemed to say, as I do, that being merely first- order might be a drawback of KIF or CGs. Later you've been citing the familiar comforts of first-order from a mathematical logician's point of view. Theoretical underpinnings should be basically sound, but our knowledge-sharing purposes demand that practically useful expressiveness comes before those theoretical concerns and preferences of mathematical logicians which in practice turn out to be irrelevant. Yours truly, Fritz Lehmann 4282 Sandburg, Irvine, CA 92715 714-733-0566 fritz@rodin.wustl.edu =====================================================================