Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF
fritz@rodin.wustl.edu (Fritz Lehmann)
Date: Fri, 9 Sep 94 10:31:38 CDT
From: fritz@rodin.wustl.edu (Fritz Lehmann)
Message-id: <9409091531.AA08687@rodin.wustl.edu>
To: cg@cs.umn.edu, interlingua@isi.edu, srkb@cs.umbc.edu
Subject: Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF
Cc: 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, sowa@turing.pacss.binghamton.edu, tony@ontek.com,
zeleny@math.ucla.edu
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
Chris Menzel answered my initial request that the international
CSMF standard for transmitting logical descriptions should allow for
true higher-order semantics in addition to First-Order imitations.
First a clarification of the current question. Menzel wrote
----begin quote----
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.
----end quote-----
I'm leaving KIF alone. At AAAI-94 in Seattle, the internal KIF
committee decided (again) to be limited to First-Order semantics,
apparently due to perceived shortcomings of current second-order
unification algorithms. John Sowa wants "IRDS" Conceptual Graphs to
mirror KIF's semantics closely, and he also is using a First-Order
semantics (but perhaps with standard numbers as primitive since they are
undefinable in First-Order). My concern is that First-Orderism not be
_required_ of all users. Some people may intend "all relations" to mean
_all_relations_ rather than the Henkin-method's _almost_all_. Some
people may want to have the genuine "connected" predicate, etc. I hope
the Conceptual Schema Modeling Facility (CMSF) will include classical
logic (with genuine higher order semantics) as an optional alternative
to the First-Order imitation. The syntax and semantics of Conceptual
Graphs or of KIF would be the same, but the CSMF would have provision
for a "semantics switch" for those who prefer not to live with the
First-Order limitations embraced by Mike Genesereth and John Sowa.
As for "added apparatus", the ungainly apparatus of elaborate,
kludgy axiom-schema-based imitations and Henkin's "all doesn't mean
all", etc. seem quite an addition compared with the classical ability to
quantify over relations.
Rather than rehash a technical debate which is still a major
dividing line among logicians and model-theorists, let me point out that
the KIF/CG First-Order approach reflects an older and still popular
approach to model theory, which may be said to have culminated in Chang
& Keisler's first edition of "Model Theory" in 1973. Newer model theory
has gone far beyond First-Orderism. Take a look at the definitive new
book by Wilfrid Hodges, "Model Theory", or the massive "Model-Theoretic
Logic" edited by Barwise and Feferman, or the new book by Shapiro. It
is crystal clear that the field has largely turned its back on First-
Orderism. Chang & Keisler have adapted to this somewhat in their recent
third edition. It was evident from last year's email debate that no-one
associated with KIF was familiar with (or perhaps even aware of) higher-
order model theory (except maybe Menzel?). I had hoped that someone
might in the last year have studied basic results like those of Fraisse
and Ehrenfeucht, and the major books just cited, and be able to speak
informedly on the subject.
I'm not a model-theorist and I don't want to be one nor talk about
it much, but anyone can see from browsing those books that the expertise
exhibited to date by the current suitors of the CSMF committees doesn't
include this field. Menzel says things which I am not confident enough
to refute, but which appear at first sight to contradict the known
results in introductory model-theory surveys. He says:
------
First, virtually all the notions in Fritz's list are definable (call
it "definable_1) in first-order set theory in familiar ways
-----
Both connectedness and planarity of graphs were in my list -- J. A.
Makowsky: "Originally, Ehrenfeucht-Fraisse games were used to prove
that certain concepts are not definable by first order formulas even if
restricted to finite structures. Among such we find the connectivity
and planarity of graphs." (Handbook of Logic in Computer Science
p.779). Is Menzel's statement, with "first-order set theory",
consistent with this result? Some of the deepest theorems in model
theory follow from Ehrenfeucht-Fraisse (reportedly Lindstrom's Theorem,
Beth's Theorem and Buchi's Theorem, and Fagin's 0-1 law for finite
relational structures). I would hope that someone experienced in this
area can advise on the merits of my request, rather than people
oblivious to advanced model theory.
I must correct a mistake in my original message. I should have said
"Non-Standard (and Robinsonian) Numbers" instead of "Non-Standard
(Robinsonian) Numbers." The logician Mikhail Zeleny kindly corrected
this with the following helpful remarks:
-----begin Zeleny quotes--------
When you talk of Robinson natural numbers, you conflate two distinct
and incompatible concepts. The Robinson reals are non-Archimedian
infinitesmals, or numbers r that fail to satisfy the axiom that for
any real q, there exists an integer n, such that nr>q. On the other
hand, the non-standard "natural numbers" are those that fall outside
of the initial omega-sequence of the hereditary successors of 0 in the
deviant models of the Peano Arithmetic. All countable non-standard
models have the structure of the true natural numbers, followed by
rationally many copies of the integers, and it is the latter that
contain the bizarre elements you may have in mind. But note that in
no model of the PA, are there any numbers distinct from 8, falling
between 7 and 9, since 9 is defined as S(S(S(S(S(S(S(S(S(0))))))))),
while 7 is taken to be S(S(S(S(S(S(S(0))))))), and it is easy to prove
that similarly construed 8 is the sole successor of the former and the
sole predecessor of the latter. (Richard Kaye has a good book on the
models of the Peano Arithmetic in the Oxford Logic Guides series.)
...
The interrelation of the two
concepts is via non-categoricity only. Both are artefacts and
consequences of the first-order limitations.
Shapiro's book will
contain a lot of relevant material. The intuitive argument goes from
compactness: consider an infinite set of formulae of the form C != N,
with the parameter N ranging over the integers. Any finite subset
thereof is satisfiable by taking C to be greater than the sup of all N
involved therein; consequently the infinite set itself is likewise
satisfiable. We proceed to inquire into the identity of C; since 0
has no predecessors, it must be greater than all of the standard
integers involved in its definition. Since all numbers but 0 have
unique predecessors, it must be embedded in an infinitely descending
order of other non-standard integers. The closure properties under
addition and multiplication yield the remainder of the order-theoretic
structure.
...
I would fain regard it as a transcendental argument
favoring the indispensability of property quantifiers.
-----end Zeleny quotes--------
For problem of "how many between 7 and 9?" I was thinking of the
peculiar Robinsonian "8.0's" clustering at the standard real 8.0 which
are infinite in number in a First-Order-based system; I shouldn't have
said "integer" for this.
Cris 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.
>Christopher Menzel.
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). The following are listed as further counterexamples
-- classes of structures undefinable even in infinitary First-Order
logic: Complete partial and linear orderings; complete lattices and
complete distributive lattices; complete Boolean algebras and complete
atomic Boolean algebras; completely distributive Boolean algebras (p.
323) free abelian groups (p. 324). I haven't read any of Dana Scott's
own papers which define domains First-Order; I do know that he put a lot
of effort into the Barwise and Feferman collection which was a major
turning point _away_ from First-Orderism. I don't know the effect on
these results of adding "first order set theory", but I suspect that the
resulting structures are nonisomorphic (due at least to countability
differences) with the true higher-order-defined cases.
The problem is that I am not competent to defend the newer model-
theory technically, and I am convinced that the other side of this
debate knows almost as little about it as I do. Ideally, an
international standard for logic should be based on some expertise
rather than guessing. Meanwhile, we need a standard soon, so let's
adopt one with the option of using either First-Order semantics or
higher-order semantics. As a potential implementer of common-sense
ontologies for practical use, I may not want the First-Order
peculiarities imposed on me. Give me a choice, within the standard.
Yours truly, Fritz Lehmann
GRANDAI Software, 4282 Sandburg Way, Irvine, CA 92715, U.S.A.
Tel:(714)-733-0566 Fax:(714)-733-0506 fritz@rodin.wustl.edu
=============================================================
].