Re: International STANDARD FOR LOGIC: CSMF/CG/KIF
Michael Zeleny <zeleny@math.ucla.edu>
Date: Fri, 9 Sep 94 17:24:50 PDT
From: Michael Zeleny <zeleny@math.ucla.edu>
Message-id: <9409100024.AA22982@oak.math.ucla.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU, srkb@cs.umbc.edu,
E.Hunt@cgsmtp.comdt.uscg.mil, bhacker@nara.gov,
duschka@cs.stanford.edu, genesereth@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,
cmenzel@kbssun1.tamu.edu, fritz@rodin.wustl.edu
Subject: Re: International STANDARD FOR LOGIC: CSMF/CG/KIF
Cc: zeleny@math.ucla.edu
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
From: Chris Menzel <cmenzel@kbssun1.tamu.edu>
>Fritz,
>
>Thank you very much for your thoughtful reply. You wrote:
>> Chris Menzel said of Scott domains:
FL:
>>>>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.
CM:
>>>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.
FL:
>>Scott structures include continuous lattices. The required lattice
>>definition "For every subset X \subseteq B, the supremum \bigvee X
>>exists" is second order and strongly so (Dickmann, in Barwise &
>>Feferman, p. 324).
CM:
>Sorry, I was unclear; I should have said Scott domains were
>"definable_1" in set theory in the sense introduced in my previous
>post, i.e., the definitions (stated in the language of set theory)
>pick out the right notions in a standard model of set theory. They
>are of course not first-order definable in the stronger sense that
>guarantees nothing unintended falls under the definition; for that you
>need to ensure that the "for every subset X \subseteq B" quantifier,
>if written in a second-order language, does indeed range over all
>subsets of B, and that's just what true second-order semantics
>guarantees. My question, once again, had *not* to do with the
>undeniable value and importance of higher-order model theory, but with
>whether, *in the context of an Interlingua*, using a higher-order
>language with the stipulation that it be interpreted with full
>higher-order model theory buys you any more than using first-order set
>theory with the stipulation that it be interpreted in a standard
>model.
I think this question is posed too narrowly. Given that mathematics
(with the conspicuous exception of category theory) can be reduced to
set-theoretic notions, your point is trivially true. But two distinct
questions can be posed in its wake: what is a natural language for
formalizing the higher-level notions of different branches of math,
and what is the correct interpretation of that language. Similarly
for other types of discourse subject to formalization. Clearly, it is
not the case that opting for a higher-order formalism will prevent an
unintended interpretation of the variables, any more than choosing to
express everything in the first-order ZFC will rule out non-standard
countable models thereof. So the choice between these alternatives
must be motivated by other considerations. I recommend the data of
descriptive linguistics, as adduced below. If you can account for
them in a natural way within a first-order formalism, you must know
something that the linguists don't. Have a go at it.
From: Chris Menzel <cmenzel@kbssun1.tamu.edu>
>Fritz Lehmann wrote to Pat Hayes:
FL:
>>...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]...
CM:
>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.
Chris fails to address the point -- some notions, like identity,
qualitative comparisons, sentences like "there are more cats than
dogs" do not lend themselves to a natural first-order formalization,
except by the unsatisfactory means of introducing them as irreducible
primitives.
CM:
>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 so far as this argument is correct, it militates against all
attempts to capture concepts in uninterpreted syntax. But given the
necessity of interpretation, a more expressive formalism is preferable
to a less expressive one.
CM:
>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.
The point concerning the pervasiveness of non-standard interpretations
suffices to dispel some of the previously raised semantic concerns,
but does not mitigate the poverty of first-order syntax.
CM:
>Minor observations:
FL:
>>[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')."
CM:
>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.
Not quite. All non-standard models are order-isomorphic to N + Z A,
where A is a dense linear order without endpoints. In particular, all
ccountable non-standard models are order-isomorphic to N + Z Q. Here
N is the order type of the naturals, Z is the order type of the
integers, and Q is the order type of the rationals. A beautiful
discussion of this result will be found in Richard Kaye's book,
_Models of Peano Arithmetic_.
FL:
>>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.
CM:
>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.
No question about that -- but first-order model theory is not the
place to look for support of the "first-order thesis". Model
theorists simply do not concern themselves with formal or informal
arguments that call for type distinctions. Consider:
Socrates is wise.
Wisdom is a virtue.
___________________
Socrates has a virtue.
This argument is valid in second-order logic. Try representing it in
a first-order formalism!
Other examples of first-order expressive failure readily come to mind.
Consider predicate adverbials:
My puppy Cosmo smells strongly.
Note that this is not the same as a propositional modifier:
It is strongly true that my puppy Cosmo smells.
The best approximation attainable in a first-order formalism is:
My puppy Cosmo smells and my puppy Cosmo is strong.
Not very convincing!
You will have a similar problem with relative adjectives:
Cosmo is a small Akita.
The first-order formalization is:
Cosmo is small and Cosmo is an Akita.
Whence it follows:
Cosmo is small.
Not at 90 pounds, he isn't!
Other examples will be found in any good treatment of formal semantics.
FL:
>>Pat, to answer your specific questions:
FL:
>>>>...[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.]
PH:
>>>Well now, "cannot" is a very strong word. How many of these could
>>>be expressed as KIF ontologies, I wonder?
FL:
>> 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.
CM:
>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.
Given that the true set theory is ZFC^2 with second-order Replacement,
just as the true Peano arithmetic is PA^2 with second-order Induction,
this comment is quite beside the point. (See Kreisel's comments in
his model theory book with Krivine, the AMS set theory symposium, and
many other places.) I think Chris is confusing the possibility of
Henkin-style first-order misinterpretation of any formalism, with the
right question of what constitutes the *correct* formalism for a given
purpose. If the order of explanation and understanding is that an
open sentence is an instance of a property, then property quantifiers
are called for. The converse Quinian order -- that properties are
mere generalizations of open sentences -- seems counterintuitive.
>=================================================================
>Christopher Menzel | Internet -> cmenzel@tamu.edu
>Philosophy, Texas A&M University | Phone ----> (409) 845-8764
>College Station, TX 77843-4237 | Fax ------> (409) 845-0458
>=================================================================
cordially, don't
mikhail zeleny@math.ucla.edu tread
writing from the disneyland of formal philosophy on
"Le cul des femmes est monotone comme l'esprit des hommes." me