**Mail folder:**SRKB Mail**Next message:**Chris Menzel: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Previous message:**Chris Menzel: "Re: International STANDARD FOR LOGIC: CSMF/CG/KIF"**Reply:**Chris Menzel: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Reply:**Anthony K. Sarris: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"

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 ============================================================= ].