Re: blow away?
cmenzel@kbssun1.tamu.edu (Chris Menzel)
From: cmenzel@kbssun1.tamu.edu (Chris Menzel)
Message-id: <9309171851.AA22982@kbssun1.tamu.edu>
Subject: Re: blow away?
To: phayes@cs.uiuc.edu
Date: Fri, 17 Sep 1993 13:51:15 -0500 (CDT)
Cc: interlingua@ISI.EDU
In-reply-to: <199309142040.AA04842@dante.cs.uiuc.edu> from "phayes@cs.uiuc.edu" at Sep 14, 93 03:43:29 pm
X-Mailer: ELM [version 2.4 PL20]
Content-Type: text
Content-Length: 5591
Pat, sorry for the delay in replying.
: Chris Menzel writes
:
: >Pat Hayes writes:
: >:...... I bet we need some higher-order
: >: expressibility,...
: >
: >Certainly true in the sense that we need to be able to talk about
: >"higher-order" objects like properties- and relations-in-intension in
: >addition to more mundane entities. What is less clear is whether it
: >is necessary to go all the way to a full-blown higher-order logic,
: >i.e., with quantification over (some intensional counterpart of) the
: >full power set of (in general, the nth cartesian product of) the
: >domain of individuals, where we lose completeness and most of those
: >other nice, friendly properties of first-order logic.
:
: I agree, its not clear. And I don't think we need 'full-blown'
: higher-order logic. But consider the possibility of a second-order
: logic which is full-blown in this sense but restricted in other ways;
: a linear second-order logic, say; or a second-order logic whose
: quantification over predicates is restricted by some kind of context
: mechanism but otherwise full-blown (full-blown in a box, it might
: be called airbag logic).
Then, if I understand you, it's *not* full-blown in the above sense;
in fact, it sounds like just the sort of restriction that can keep
things semantically first-order, but give us a clean, ostensibly
second-order way of quantifying over intensions.
: I'm making these up as I go along, but my
: point was that we need to be experimenting, not standardising.
Granted, surely.
: Incidentally, what do you think of Henkin semantics for higher-order
: logic?
*Essentially*, higher-order logic interpreted in terms of Henkin's
so-called general structures is just sheep in wolves clothing (with
apologies to Quine): in effect, it's just a many-sorted first-order
theory, and hence no more expressively powerful (on the usual measures
of expressiveness) than a plain vanilla first-order theory, as you
note:
: There's a sense in which higher-order logic with Henkins semantics
: is first-order, but it sure doesn't FEEL like FOL when you are using
: it. And we get completeness back, so its fairly friendly.
That feeling is probably attributable to the presence of added
conditions on general structures that preserve some of the flavor of
true second-order logic; in particular the higher-order types in
general structures must be rich enough to guarantee the presence of
all *definable* relations. Thus, when translated into a many-sorted
language, the higher-order sentences that are valid in Henkin's
semantics are not in general valid in (many-sorted) first-order logic,
but are rather consequences of a certain first-order *theory*, viz.,
the (first-order translations of) all the "comprehension" sentences
(EF)(x1)...(xn)(Fx1...xn iff A), where "F" doesn't occur free in A
(just looking at the second-order case). Hence, while higher-order
logic with general structures doesn't increase essential expressive
power (unlike full-blown higher-order logic) there's still a lot more
lurking in the background. And that might constitute a "higher-order"
framework that is both appropriate and expressively adequate for
certain KRep needs, but which doesn't sacrifice the virtues of FOL.
: > At any rate,
: >because of this it would seem to be sound methodologically as far as
: >possible to try to satisfy the needs of KR with first-order extensions
: >to classical FOL.
:
: Well I agree, in fact. FOL seems the best foundation we have at the
: present, and it keeps getting re-invented. But look at some of the
: problems we have had working within it.
:
: I guess my most recurrent worry is this. One of the reasons we feel
: 'safe' with FOL is that while acknowledging that we will need extensions
: to it, we all feel that they will indeed be extensions, ie they can
: hardly be weaker than FOL. (After all, what would you take out? 'NOT',
: say? Nah...) But maybe this intuition is mistaken. Maybe in order to
: get the comfort back we will need to sacrifice some expressive power
: of FOL for something else, and do so in a systematic way which forces
: us to alter the semantic base significantly.
:
: This is related to a worry I expressed in earlier correspondence. We
: seem to need ways of describing sets of sentences which are different
: from any of the usual semantic frameworks, because these always give
: us (sub)languages, ie are always closed under some kind of inference.
: What could these be? If we find them, perhaps they will be more like
: what we need for the semantics of a representational language. Ie,
: perhaps thinking of assertional logics (of any kind) as the appropriate
: vehicles for representing thought may be misleading us. This has often
: been expressed before, but the replacements offered have usually turned
: out to be just FOL in disguise. I don't have any replacements,
: just a feeling that we may need a major conceptual leap, and a concern
: that talk of standardisation in Krep is more likely to smother than
: encourage the strength of imagination required. If we feel too
: comfortable we might doze off :-)
I have no comments other than that these trenchant remarks bear
rereading; so here they are again... :-)
--Chris
================================================================
Christopher Menzel Internet -> cmenzel@tamu.edu
Philosophy, Texas A&M University Phone ----> (409) 845-8764
College Station, TX 77843-4237 Fax ------> (409) 845-0458
================================================================