Delivery-Date:
From: dam@ai.mit.edu (David McAllester)
Date: Sat, 13 Aug 94 21:19:37 EDT
Message-Id: <9408140119.AA23180@wheaties>
To: jmc@cs.stanford.edu
Cc: boyer@CLI.COM, qed@mcs.anl.gov
In-Reply-To: John McCarthy's message of Sat, 13 Aug 94 16:01:43 -0700 <9408132301.AA07521@SAIL.Stanford.EDU>
Subject: set theory
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


  The full utility of qed requires such an intermediary [as set theory],
  and it must be
  powerful expressively.  Is there another candidate?

Well, consider set theory extended with the ability to define functions and
then use them in terms.  This is syntactically richer than the first order
language with one binary relation.  The term language could allow for various
kinds of recursive definitions and have a nontrivial type structure. I believe
that there is a great variety of languages which are can be viewed as syntactic
sugar for set theory.  I believe that the sugar is pragmatically important.
For example, in many such languages well-typedness can be checked
algorithmically.  Terms provide the syntactic structure necessary for
equational reasoning based on the substitution of equals for equals and for
term rewriting.  A translation into and out of pure set theory would lose the
struture used in both type checking and term rewriting.  It seems that a
syntactically rich variant of set theory is desirable.  But is not clear taht
any one such system will allow for all the heuristically useful syntactic
structure that people will invent in, say, future type systems.

        David