**Mail folder:**Interlingua Mail**Next message:**Fritz Lehmann: "hiher-order KIF & Conceptual graphs"**Previous message:**phayes@cs.uiuc.edu: "Re: A proposal of "sorts""**In-reply-to:**phayes@cs.uiuc.edu: "Re: Higher-Order KIF and Conceptual Graphs"

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. ====================================================