Re: Higher-order KIF & Conceptual Graphs
phayes@cs.uiuc.edu
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