**Mail folder:**SRKB Mail**Next message:**David McAllester: "INTERNATIONAL STANDARD FOR LOGIC: CSMF"**Previous message:**John McCarthy: "Re: INTERNATIONAL STANDARD FOR LOGIC: CSMF"

Date: Sun, 11 Sep 94 10:52:49 CDT From: fritz@rodin.wustl.edu (Fritz Lehmann) Message-id: <9409111552.AA05949@rodin.wustl.edu> To: cg@cs.umn.edu, interlingua@isi.edu, srkb@cs.umbc.edu Subject: "Contexts: logic-order for the CSMF standard" Sender: owner-srkb@cs.umbc.edu Precedence: bulk

John Sowa wrote about the proposed Conceptual Schema Modeling Facility standard (ISO/IEC JTC1/SC21/WG3/CSMF), or "CSMF": ---begin quote--------- Fritz, If it will make you any happier, please be assured that we are indeed "allowing" true higher-order logic within the KIF and CG frameworks. As I have repeated many, many, many times, we are NOT providing an FOL framework. We are providing an infinite hierarchy of metalanguages, all of which have a first order structure. In that structure, we can define new axioms for languages, including any version of HOL that you please -- that includes TRUE HOL, with all its works and pomps, including quantification over all subsets of any set. All of the examples that you cited can indeed be handled. I have shown how to do some of them. You can take it from there. ---pause quote----- Yes, you are "allowing" classical higher order logic in the same sense that you are "allowing" fuzzy logic, probabilistic logic, self- contradictory logic, Three Stooges logic, Neo-Albanian mereology and Quantum Taxidermy. That is, anything can be put in a box. However, you and Genesereth do not in your current proposal _provide_ any of these to the CSMF standard, only First-Order logic with "first order sets". Nor do you (as far as you have revealed in the year or so since you made this claim) have the expressive power to give the correct semantics in the outermost context for sentences occurring in the "higher-order" inner contexts (which are in languages provably inexpressible in First-Order logic). If the context-boxes are "opaque", without any lifting of theories from within a context to the surrounding context, then the contexts are mere quoted "black blobs" (not even black-boxes since there are no intelligible inputs and outputs) and this certainly fails to interpret higher order statements correctly in the outer model-theoretic semantics of the CSMF standard itself. If you _can_ lift theories from within a context to the surrounding context, then you must translate (via some mapping) from the inner language to the outer language while preserving the model-theoretic semantics. If KIF or "IRDS" Conceptual Graphs were the official languages of the outermost context, i.e. of the CSMF standard itself, with your current choice to limit expressiveness of these to First- Orderism, then any such translation will FAIL to capture the correct semantics for the standard. What is said in higher-order logic within a context would be MIS-interpreted by the CSMF standard. If someone defines "8.0" correctly in higher-order logic context, it could mean "an infinite class of non-isomorphic 8.0-like First-Order-numbers" in the outermost context. A different computer reading this may never be able to determine that "8.0" is the actual number. (If you take numbers as primitives instead, then substitute "connected", "planar" or any of the other concepts proven to be definable only in higher-order logic). ---resume quote----- Meanwhile, I am trying to finish my book. I will include therein many more examples, many more exercises, and answers to the more interesting exercises in the back. It will all become clear in due course. John Sowa ---end quote------- Since you and Mike Genesereth are promoting Conceptual Graphs and KIF to the Conceptual Schema Modeling Facility standards subcommittee Working Group (ISO/IEC JTC1/SC21/WG3/CSMF) in Seattle starting around tomorrow, "due course" for your clarification is now, I would think. Someone said that the hope is to get all these formal matters decided by December of this year. If the CSMF standard includes a hierarchy of nested metalanguages and contexts, then the outermost context and the standard itself should be based on classical logic. That is, formulae quantifying only over individuals would have First-Order semantics, but formulae quantifying over predicates, sets, functions and relations would have genuine ("strongly") higher- order semantics. If you and Mike Genesereth wish to offer an axiom-schema- based (or Henkin-semantics based) "weakly higher-order" (actually First-Order) semantics for formulae with higher-order syntax, then _that_ should be in an inner context along with your specification of its limited model-theoretic semantics. The full CSMF system (the outermost context of any information expressed in the standard) would be able to interpret the pseudo-higher-order sentences "lifted" from your "First-Order only" context as first- order sentences quantifying over a finite or countable domain of individuals within the CSMF's full semantic domain. Those who wish to adhere to your First-Order sub-language would be free to do so, but others (who may want "connected" to mean connected) can use the classical higher-order language of the outermost context, and that would be the initial "semantic interface" between two communicating systems. Because classical logic has more expressive semantics than the First-Order-only version, you can "lift" in one direction and preserve meaning, but not in the other direction. So CSMF itself would be based on classical logic, and the First-Order-only version would be in an optional defined context. (The syntaxes would be nearly identical.) This is what I recommend, unless you are able to show the Working Group some new way in which nested First-Order metalanguages can actually give correct, interpreted, strongly higher-order model-theoretic semantics to higher-order formulae -- in the common, standard, outermost CSMF language, not hidden in some quoted "black blob". 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 ============================================================= ~c jksharp@sandia.gov, msmith@vax2.cstp.umkc.edu, sharadg@atc.boeing.com ~c roger@ci.deere.com, sowa@turing.pacss.binghamton.edu ~c msingh@bcr.cc.bellcore.com, bhacker@nara.gov, scott@ontek.com ~c tony@ontek.com, skperez@mcimail.com, genesereth@cs.stanford.edu ~c duschka@cs.stanford.edu, E.Hunt@cgsmtp.comdt.uscg.mil ~c zeleny@math.ucla.edu, kennett@u.washington.edu