Re: International STANDARD FOR LOGIC: CSMF/CG/KIF
Chris Menzel <cmenzel@kbssun1.tamu.edu>
From: Chris Menzel <cmenzel@kbssun1.tamu.edu>
To: fritz@rodin.wustl.edu
Cc: cg@cs.umn.edu, interlingua@ISI.EDU, srkb@cs.umbc.edu,
E.Hunt@cgsmtp.comdt.uscg.mil, bhacker@nara.gov,
duschka@cs.stanford.edu, jksharp@sandia.gov,
msingh@bcr.cc.bellcore.com, msmith@vax2.cstp.umkc.edu,
roger@ci.deere.com, scott@ontek.com, sharadg@atc.boeing.com,
skperez@mcimail.com, tony@ontek.com
In-reply-to: <9409080359.AA02268@rodin.wustl.edu> (fritz@rodin.wustl.edu)
Subject: Re: International STANDARD FOR LOGIC: CSMF/CG/KIF
Message-id: <94Sep9.015145cdt.9762@kbssun1.tamu.edu>
Date: Fri, 9 Sep 1994 01:51:35 -0500
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
Fritz Lehmann wrote to Pat Hayes:
...I fully support the quick adoption of a logic standard for
knowledge interchange, but the standard should include classical
logic ("strongly" higher-order, with quantification over
predicates, functions and relations) and not limit the logic
standards definition to "First-Orderism" (quantifying only over
individuals) unless there is a very good practical reason given for
it. "First-Order-Only" should be an _option_ (which would include
"weakly higher-order" schema-based or Henkin semantics) but not a
requirement.
Here briefly are _some_ of the troubling proved consequence of
First-Orderism....
ANY FIRST-ORDER-ONLY-BASED LANGUAGE... CANNOT DEFINE [lengthy list
deleted]...
This issue came up last year, and I raised a question about
higher-orderism of the sort that Fritz so energetically defends. I
recall some agreement, but don't recall seeing an answer. I would
challenge Fritz to provide one, for it still seems to me there is
little if anything to be gained by going higher-order so long as
you've got enough set theory (e.g., as much as in the current version
of KIF). I'll try to express my concern clearly; if I'm wrong, I'd
greatly appreciate correction.
First, virtually all the notions in Fritz's list are definable (call
it "definable_1) in first-order set theory in familiar ways:
well-foundedness, natural number, finitude, countability, etc. To say
these notions are definable_1 in set theory is to say that the
relevant definitions pick out the correct notions (or adequate
representations thereof) in all *intended*, or standard, models of set
theory, i.e., cumulative hierarchies possibly built over some set of
nonsets. The problem, of course, is that, being first-order, there
are *unintended* models of set theory in which, for example, things
besides the "genuine" natural numbers of the model are included in the
"natural number" predicate, or in which nonwellfounded relations end
up sneaking into the "wellfounded relation" predicate. This can't
happen in true second- (or higher-) order logic. The notions in
question are all definable (call it "definable_2") in the sense that
there are higher-order formulas which do succeed in picking out all
and only the right kinds of objects in *any* model; one can, for
example, formulate second-order sentences which are true only of the
countable sets in a model, or are true only of the well-founded
relations, etc. Second-order Peano Arithmetic, in particular, is true
only in domains isomorphic to N, and hence succeeds in defining the
notion "natural number" where first-order PA does not.
There is, however, a fly in this ointment. Henkin showed how to
define the notion of a "general model" for a higher-order language,
which yields a logic that is esssentially first-order: the trick is
simply that you don't require that the n-place variables of order m+1
range over ALL the subsets of n-tuples of order m individuals. That
is, more generally, one quantifies over some, but not necessarily ALL,
of the properties, relations, functions, etc. of order m individuals.
Here is what seems to me to be the rub: there is nothing, save our
intentions, that "pins down" whether, in using a higher-order
language, we are endowing it with a full higher-order semantics or
simply with the semantics of a watered-down general model (hence,
whether we're *really* doing higher-order logic at all). But if so,
then we are in the same epistemological boat that we were in with
first-order set theory: either way we simply have to state our
semantic intentions; we cannot enforce them in any more robust way (in
particular, in a knowledge base or a so-called higher-order theorem
prover). Thus, when I claim that R is a well-ordering because ALL
subsets of the field of R have an R-least element, whether I choose to
write this as a second-order statement that I intend to be interpreted
with a full second-order semantics, or as a statement of first-order
set theory that I intend to be interpreted in a standard model, as I
see it, macht nichts.
In sum: Higher-order languages have no less (and no more) of a problem
with unintended models than first-order languages. So avoid the added
apparatus and just do it all in first-order set theory. Corollary: in
this regard, leave KIF alone.
Minor observations:
[FOL] CANNOT DEFINE ORDINARY NATURAL NUMBERS - it can only define
Non-Standard (Robinsonian) Numbers, using pseudo-Peano axioms. If
I ask a Knowledge Base, "How many integers are between 7 and 9,
inclusive?" I want it to answer "three: 7, 8, and 9.", but the
First- Order-based system's answer is: "An infinite number of
mutually non- isomorphic, nonstandard integers (including
'Robinsonian infinitesimals')."
This is not so. All nonstandard models of first-order arithmetic
start with an initial sequence that is isomorphic to N followed by any
number of copies of the integers. In particular, it is a theorem of
first-order PA that there are exactly three integers that are >= 7 and
=< 9.
Some logicians who admire completeness, compactness, and Lowenheim-
Skolem-ness are willing to put up with the very peculiar
consequences and limitations of First-Orderism. Other logicians,
including probably all advanced model-theoretic logicians, are not
willing to put up with it.
Few, if any, model theorists would describe the expressive limitations
of first-order logic as something to put up with. They are usually
viewed as a very interesting and important object of study. And the
vast amount of research in first-order model theory, described for
example in Chang and Keisler's classic *Model Theory*, attests pretty
eloquently to the fact that the subject has managed to hold the
undivided attention of more than a few competent logicians.
Pat, to answer your specific questions:
>>...[CCAT can use concepts that] cannot be expressed
>>in current KIF (like "actors", Sowa-contexts, connected structures,
>>planarity, standard numbers, transitive closures, Buchi automata,
>>Montague grammars, power structures, Propositional Dynamic Logics,
>>etc.)[
>>That is, CCAT could include more general Conceptual Graphs not
>>restricted to the KIF-equivalent IRDS Conceptual Graphs.]
>Well now, "cannot" is a very strong word. How many of these could
be >expressed as KIF ontologies, I wonder?
Unless I am mistaken, none. "Actors" in Conceptual Graphs are
procedural. Genesereth has stated often that KIF is declarative
and not procedural. To provide declarative semantics for
procedures requires correct treatment of recursive functions,
functions of functions, and programs which loop infinitely and
never halt; this requires "reflexive" algebraic structures of
partial functions like the continuous lattices of Dana Scott, which
leads to domain theory and necessary distinctions which are
strongly higher-order.
Once again, mere quantification over functions, functions of
functions, etc. does not necessarily mean you are using a higher-order
logic. These are all first-order objects in set theory. Scott
domains in particular are definable (and typically, are defined, even
in Scott's own papers) in first-order set theory.
=================================================================
Christopher Menzel | Internet -> cmenzel@tamu.edu
Philosophy, Texas A&M University | Phone ----> (409) 845-8764
College Station, TX 77843-4237 | Fax ------> (409) 845-0458
=================================================================