Higher-order KIF and Conceptual Graphs
fritz@rodin.wustl.edu (Fritz Lehmann)
Date: Wed, 8 Dec 93 05:21:29 CST
From: fritz@rodin.wustl.edu (Fritz Lehmann)
Message-id: <9312081121.AA22839@rodin.wustl.edu>
To: boley@dfki.uni-kl.de, cg@cs.umn.edu, interlingua@ISI.EDU
Subject: Higher-order KIF and Conceptual Graphs
Dear John Sowa, sowa@turing.pacss.binghamton.edu
My tenaciousness is waning (I've done enough, and a noted
logician warned me to expect hours of fruitless debate with "the
die-hard First-Orderite") but, since you object to a particular
sentence of mine, I'll respond to that.
You said:
>I also object to a statement you made that I have "now departed from FOL
>by including numbers as primitives along with a cardinality function
>from a set to a number." That example I gave was purely first order.
>I can have a pure first-order statement in which one of my sorts or
>types happens to be the integers.
I had assumed, maybe wrongly, that by "natural numbers" you
had meant the natural numbers. If there is no formal semantics to
distinguish your numbers type from that of "red" or Pat Hayes'
example "VERY-BIG", then each number is merely an uninterpreted
typed monadic predicate of a set. In that case I was mistaken and
you have not departed from First-Orderism. In that case also
CARDINALITY({a,b,c})= 2 is semantically acceptable as is
CARDINALITY({x|x in INTEGER})= 106. I had assumed the contrary,
that you meant that the cardinality function must correctly count
the members of a set and that the set of natural numbers is
infinite.
If the latter is the case, then I'm missing your point. My
reasoning is: A. The concepts "natural number", "finite",
"connected" etc. are not First-Order definable. B. You say these
ARE definable using your number-type in Conceptual Graphs.
Therefore: C. Conceptual Graphs using the number-type must not be
First-Order. Is this flawed reasoning?
[You left out my "(wisely, I think)" in the middle of your
quote of my sentence. Remember, my private opinion is still that
the attempted reductions of the number concept to pure logic have
been baloney from the start. I'm with Kronecker, taking natural
numbers as God-given, but then I can't call them First-Order.]
You suggested that the metalevel capability of KIF/CGs is the
key to this debate. I'm unable to decide whether your many
citations of the metalevel feature as expanding expressiveness
have been valid or vacuous. Earlier you used this to say a First-
Order language can include higher-order logic. If I invent a
language with formal semantics and a metalevel/quotation ability,
is it fair for me to claim that my language now "incudes" every
other language, with correct semantics, because I can describe
those languages as objects? It seems to depend on how "opaque"
the metalevel/quotation mechanism is. If it's fully opaque, then
the embedded language is just a blob and statements in the
embedded language are mere uninterpreted strings at best. In that
case my claim would be true but vacuous. If it's transparent, and
if statements in the embedded language obtain their formal
semantics entirely by interpretation in the semantics of the outer
language, then they inherit all the limits on expressiveness of
the outer language, and my claim would be false. I gather from
your statements that there must be a third possibility.
Can we have things both ways? Manzano's introduction to
Meinke & Tucker's "Many Sorted Logic and Its Applications" has a
good discussion of the whole higher-order issue. He says of the
stronger and weaker versions, "And the little mermaid got two
beautiful legs (with a lot of pain as you might know). But even
in stories everything has a price, you know the little mermaid
lost her voice. ... Therefore one has to chose between expressive
power [higher-order] or a complete calculus [First-Order]. You
cannot be a mermaid and have an immortal soul." (He then
recommends a many-sorted Henkin-based approach.)
My position throughout this discussion has been that I favor
expressive power except when it makes no possible practical
difference. Some of the strongly higer-order examples in my list
do appear to have practical consequences, as I discussed earlier.
Yours truly, Fritz Lehmann
fritz@rodin.wustl.edu
4282 Sandburg, Irvine, CA 92715 USA 714-733-0566
PS: You ask whether the "HOL" language is really higher-order.
Strongly higher-order Beta-reduction is a built-in primitive of
HOL (p.273, p.344) and HOL can be used to prove Peano's
postulates for arithmetic including induction (p. 20). The model
universe U contains an infinite set I, and for any set X in U,
the powerset P(X) is also in U. (p.193-194) So P(I) is in U.
(Gordon & Melham, Intro. to HOL, Cambridge U. Press, 1993) This
looks strongly higher-order but I'm not sure.
====================================================