Re: Higher-order KIF & CGs (Fritz Lehmann)
Date: Mon, 1 Nov 93 01:16:17 CST
From: (Fritz Lehmann)
Message-id: <>
Subject: Re: Higher-order KIF & CGs

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 

	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

	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 

	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 

	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


>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