**Mail folder:**Interlingua Mail**Next message:**Nicola Guarino: "Cognitive and Ontological Foundations of Knowledge Engineering"**Previous message:**phayes@cs.uiuc.edu: "Re: Higher-order KIF & Conceptual Graphs"**In-reply-to:**sowa: "Re: Higher-order KIF & Conceptual Graphs"

Message-id: <199401220440.AA26568@dante.cs.uiuc.edu> X-Sender: phayes@dante.cs.uiuc.edu Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Fri, 21 Jan 1994 22:45:22 +0000 To: sowa <sowa@turing.pacss.binghamton.edu>, cg@cs.umn.edu, fritz@rodin.wustl.edu, interlingua@ISI.EDU From: phayes@cs.uiuc.edu Subject: Re: Higher-order KIF & Conceptual Graphs

At 8:27 PM 1/21/94 -0500, John Sowa wrote: >Fritz, > >Please do not include me under the first-orderites. As I have been >trying to get across in message after message to these lists, >the approach of using metalevel reasoning together with sorted logic >gives us the ability to do the same kinds of things that are done >in higher-order logic with exactly the same semantics. Thats an open question right now as far as Im concerned, but I would love to have a reference to a precise account of how it works, if one exists. >As Mike Genesereth pointed out, the only difference is whether you >specify up front the range of quantification; i.e. in the FOL case, >you specify the sets over which you permit quantifiers to range, >whereas in "true" HOL, you allow those sets to be implicit. I am puzzled by this. In the discussions between Fritz and me, the 'classical' HOL semantics is the one that 'specifies' the ranges of the HO quantifiers, while the Henkin models of HOL - which make it essentially first-order in its expressive power - allow higher-order quantifiers to range more freely (insisting only that the domains contain enough entities to provide a denotation for every wellformed expression, which might reasonably be taken as a kind of minimal constraint on a model theory.) To illustrate, suppose we propose an interpretation in which the first-order domain is the set N of the integers. Then the classical second-order domain in this interpretation, ie the set which the quantifier in (Forall P)(P x) ranges over, is fixed: it is the set 2!N of all subsets of N. The quantifier in (Exists P)(P (P 12)) must range over the set 2!(2!N), and so forth. Thus, in a classical model, specifying the lowest (first-order) domain completely fixes the ranges of all the higher-order quantifiers. Notice that this means that in the case cited, these HO quantifiers must range over uncountable sets. In a Henkin interpretation, however, they are much more free. If the first-order domain is N, the second-order domain is any subset of 2!N which contains denotations for every predicate (lambda-)definable in the language under discussion. Notice that this can always be a countable set. So there is a great range of freedom in these 'first-orderish' interpretations which is not available in classical interpretations. Whether this interpretive freedom is a Good Thing may reasonably be discussed on various philosphical grounds, but that it exists when we construct upwards from a first-order basis is just a fact. And this illustrates why Henkin models are essentially first-order. If we just lump together all the domains into one big set, regarding them now as sorts, and think of the HO quantifiers as 'really' being first-order quantifiers ranging over sorts now rather than orders, then every Henkin interpretation looks first-order; but, more importantly, every first-order interpretation (suitably sorted, and assuming they satisfy appropriate comprehension schemata) can be made back into a Henkin higher-order: so these Henkin HO interpretations are 1:1 with suitably sorted first-order interpretations of a (rich enough kind of) FO theory. Thats a brief summary of why we call these Henkin interpretations first-order, by the way. I do not yet understand how any kind of metalevel reasoning process can encompass enough expressive power to ensure that only uncountable interpretations are possible, since there are only ever countably many expressions in any countable language, even one with metalinguistic reasoning capabilities and access to schema of various kinds. You can add in lambda-conversion, and you still don't get enough expressive power to nail down those higher-order quantifiers to being *exactly* 2!N. It seems to require some kind of Divine Right. Pat Hayes ---------------------------------------------------------------------------- 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