INTERNATIONAL STANDARD FOR LOGIC: CSMF
dam@ai.mit.edu (David McAllester)
From: dam@ai.mit.edu (David McAllester)
Date: Mon, 12 Sep 94 10:30:45 EDT
Message-id: <9409121430.AA03876@spock>
To: jmc@cs.stanford.edu
Cc: fritz@rodin.wustl.edu, tony@ontek.com, E.Hunt@cgsmtp.comdt.uscg.mil,
bhacker@nara.gov, cg@cs.umn.edu, duschka@cs.stanford.edu,
genesereth@cs.stanford.edu, interlingua@isi.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,
srkb@cs.umbc.edu, fritz@rodin.wustl.edu
In-reply-to: John McCarthy's message of Sun, 11 Sep 1994 03:18:38 -0700 <9409111018.AA23545@SAIL.Stanford.EDU>
Subject: INTERNATIONAL STANDARD FOR LOGIC: CSMF
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
Both John McCarthy and Chris Menzel have correctly pointed out that
first order set theory provides all of the power of higher order logic
(and then some). But set theory derives much of its inferential power
from the comprehension schema:
exists y "y = {z in x : Phi[z]}"
This schema is used to form subsets of x from formulas of the form
Phi[z]. So, as in PA, second order quantification is simulated by a
first order schema. HOL uses direct higher order quantification and
replaces the above comprehension principle with the ability to write
lambda predicates (and lambda functions). This seems like a more
computationaly tractable approach.
I think main concerns are pragmatic. I suspect we all agree that
lambda expressions, quantification over sets and functions, recursive
definitions, and mathematical induction are pragmatically useful. I'm
willing to believe that John Sowa he can find a way of doing these
things with an appropriate first order meta-theory. However, it seems
building these features directly in at the level of the base logic,
and hence avoiding an otherwise necessary meta level, may result in a
"friendlier" system.
David