Int. Standard for Logical CSMFs (Fritz Lehmann)
Date: Fri, 9 Sep 94 22:57:47 CDT
From: (Fritz Lehmann)
Message-id: <>
Subject: Int. Standard for Logical CSMFs
Precedence: bulk

Tony Sarris, 

    A few points, though I assume you have already left for
the Seattle meeting on the standard.  You say:
---begin quote---
Let me make clear that neither ANSI X3T2 nor ISO/IEC/JTC1/SC21/WG3 CSMF RG
is intending to develop an international standard for logic. ...
Also, what John Sowa and others involved directly with CGs
decide to do with CGs in general is largely independent of the ANSI X3T2
effort and X3H4 IRDS effort (which is now combined with the X3T2 effort
anyway). Again, we will drawn upon appropriate aspects of CGs, KIF, SUMM
and whatever else to form a suitable basis for supporting the CSMF
standards work.
---end quote---

     This is slightly reassuring since it suggests that the
relevant committees do not already "belong" to the first-
order-ites.  My impression is that the KIF committee has
from the start, which is perfectly OK, of course, since 
they invented KIF.   And please keep in mind that I am a
supporter of KIF, CGs and CSMF; as a keeper of ontologies,
I just don't want to force people into something basically
weird and confusing for no good reason.  They should be
able to say "connected" and mean it.

     Section 8 of the current draft for the CSMF standard
says: "The Normative Schema constructs comprise a rich
taxonomic scheme of static, dynamic and higher-order
syntax and semantics ..." I think First-Orderism would render
this claim false.

     You also said:
---begin quote---
Internationally, there may well be objections to utilizing anything outside
traditional FOL, as some national bodies have already expressed concerned
that higher-order logics are simply too vaguely defined -- i.e., that they
are largely the subject of research not general practice -- and are
therefore not appropriate for inclusion or application within an ISO
---end quote---

     I belive this view is mistaken.  Classical logic is
n-order, as in Principia Mathematica, and is more "traditional".
FOL dealing only with first-order matters is also fairly
traditional;  what is neither traditional nor uncontroversial
is using First-Order-ism to do higher order things.  KIF
and CGs definitely have predicates and relations and (some
yet-undecided notion of) numbers which definitely participate
in relations.  If the committee requires a full and clear
explanation of axiom-schema-based imitation higher-order,
or Henkin-semantics-based imitation, I think you will see
what a technical kludge it is.  The only reasons for it
historically are completeness, compactness and Lowenheim-
Skolemness.  I find the first and last of these to be
irrelevant to practical work, and the more I see of 
compactness the worse it looks.  See Mikhail Zeleny's
explanation of how the deviant models with
Non-Standard Numbers arise from it.  David McAllester
just pointed out that automated proof and verification are even
harder with the First-Order axiom schemata or Henkin's
method that with ordinary higher-order logic.   I hope
your European colleagues are not responding based on 
unexamined assumptions about logic formed in their
undergraduate introductions to it.  With luck they
will be well advised by knowledgeable logicians.

                          Yours truly,   Fritz Lehmann
GRANDAI Software, 4282 Sandburg Way, Irvine, CA 92715, U.S.A.
Tel:(714)-733-0566  Fax:(714)-733-0506