INTERNATIONAL STANDARD FOR LOGIC: CSMF

dam@ai.mit.edu (David McAllester)
From: dam@ai.mit.edu (David McAllester)
Date: Fri, 9 Sep 94 17:06:07 EDT
Message-id: <9409092106.AA03548@spock>
To: tony@ontek.com
Cc: fritz@rodin.wustl.edu, jksharp@sandia.gov, msmith@vax2.cstp.umkc.edu,
        sharadg@atc.boeing.com, roger@ci.deere.com,
        sowa@turing.pacss.binghamton.edu, msingh@bcr.cc.bellcore.com,
        bhacker@nara.gov, scott@ontek.com, tony@ontek.com, skperez@mcimail.com,
        genesereth@cs.stanford.edu, duschka@cs.stanford.edu,
        E.Hunt@cgsmtp.comdt.uscg.mil, cg@cs.umn.edu, interlingua@isi.edu,
        srkb@cs.umbc.edu
In-reply-to: Anthony K. Sarris's message of Fri, 9 Sep 94 11:31:06 PDT <9409091831.AA01006@ontek.com>
Subject: INTERNATIONAL STANDARD FOR LOGIC: CSMF
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk

I have not generally taken part in interlingua discussions but have
been generally concerned by the emphasis on first order semantics.  It
is well known, and stated in previous messages, that you can't even
define the concept of "connected to" in a graph in first order logic.
This has important PRACTICAL implications.  Let Arc and Con be two
binary relations and Phi(Arc, Con) be a formula which claims to state
that Con(x,y) is true if and only if there is a path of arcs form x to
y where Arc(x,y) means there is an arc from x to y.  I challenge the
supporters of a purely first order system to write this definition.
When most people write Phi(Arc,Con) in first order logic they get
something such that

forall x P(x) ^ Arc(x,y) => P(y)
plus Phi(Arc,Con)

does NOT imply

forall x P(x) ^ Con(x,y) => P(y).

A concept language which can not define the concept of connected in a graph
would seem to be of limited utility.

   As far as I'm concerned, the most important aspect of higher-order logic is
   support for context and other forms of modalization.

Well, I would also like to be able to define "connected to".

   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
   standard.

The most widely used mechanical verification system is HOL, a
mechanized fully higher order logic.  HOL is more widely used, I
believe, (in terms of actual number of users) than any mechanized first
order system.  The reason is simple --- first order systems do not
provide sufficient expressive power to describe most of the concepts
that hardware designers use, and most users of formal systems are currently
hardware design verifiers.  If KIF stays with first order semantics
then I don't think that any hardware design team would ever select it
for respresting hardware concepts.  The simple concept of an n-bit
ripple carry adder can not be expressed in first order logic.

The problem, in practice, is mathematical induction.  Many truths can
only be proved if we have some form of induction principle.  Induction
principles are naturally second order.  First order induction schemes
are HARDER to compute with than higher order principles invoked with
higher order matching and unification.  Higher order unification may be
bad, but wait till you try to use a first order induction scheme!.

In summary, induction principles seem to be a necessity.  Higher order
induction principles seem more computationally tractable than first
order induction schemes.  If we try to sidestep the problem by using a
first order syntax with an intended model, we will still need
induction principles to reason about the standard model, so we are
back where we started.

	David