From owner-qed Sat Aug 13 20:20:23 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id UAA06825 for qed-out; Sat, 13 Aug 1994 20:19:51 -0500
Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id UAA06820 for <qed@mcs.anl.gov>; Sat, 13 Aug 1994 20:19:44 -0500
Received: from wheaties (wheaties.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA08967; Sat, 13 Aug 94 21:19:39 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by wheaties (4.1/AI-4.10) id AA23180; Sat, 13 Aug 94 21:19:37 EDT
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