From owner-qed Sat Aug 13 12:50:08 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA02054 for qed-out; Sat, 13 Aug 1994 12:47:36 -0500
Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id MAA02049 for ; Sat, 13 Aug 1994 12:47:30 -0500
Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA06289; Sat, 13 Aug 94 10:47:24 -0700
Date: Sat, 13 Aug 94 10:47:24 -0700
From: John McCarthy
Message-Id: <9408131747.AA06289@SAIL.Stanford.EDU>
To: boyer@CLI.COM
Cc: qed@mcs.anl.gov
In-Reply-To: <9408131433.AA25801@rita> (boyer@cli.com)
Subject: Re: set theory
Reply-To: jmc@cs.stanford.edu
Sender: owner-qed@mcs.anl.gov
Precedence: bulk
The proposition I was advancing was more modest than basing all
proof-checking and proof-finding on set theory.
I was proposing set theory as an intermediary that would permit a
theorem proved in one system to be translated to other systems and
used there without being proved again.
The full utility of qed requires such an intermediary, and it must be
powerful expressively. Is there another candidate?
*****
There is also a more ambitious idea. It is that other systems
represent restrictions of set theory to a particular collection of
formulas, to the use of a particular set of theorems as derived proof
rules and to a particular class of proof strategies. I would like to
see this more ambitious idea demonstrated, e.g. for the Boyer-Moore
system.
*****
This idea is distinct from the more modest idea above, and it is
mostly laziness that makes me put them in the same message. Please
react to them separately.