"Contexts: logic-order for the CSMF standard"
fritz@rodin.wustl.edu (Fritz Lehmann)
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