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.