From owner-qed Sun Aug 14 11:34:47 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id LAA04359 for qed-out; Sun, 14 Aug 1994 11:34: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 LAA04354 for ; Sun, 14 Aug 1994 11:34:31 -0500 Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA10192; Sun, 14 Aug 94 09:34:26 -0700 Date: Sun, 14 Aug 94 09:34:26 -0700 From: John McCarthy Message-Id: <9408141634.AA10192@SAIL.Stanford.EDU> To: boyer@CLI.COM Cc: qed@mcs.anl.gov In-Reply-To: <9408141553.AA25876@rita> (boyer@cli.com) Subject: Re: More replies to JMC Reply-To: jmc@cs.stanford.edu Sender: owner-qed@mcs.anl.gov Precedence: bulk I wrote: > 1. If the result came originally from a "constructively correct" > theory, then going through set theory shouldn't harm it. and Bob Boyer replied: I don't know what you mean by "harm"? How does one "harm" a wff? More seriously, the point I was making is that a constructivist doesn't put much store in a proposition about which all that is known is that it is a theorem of set theory I see I was cryptic. Suppose a result to have been proved in the Boyer-Moore system, and that system is constructive enough for person A. Now suppose the result is translated into set theory and from there into A's favorite system. From A's point of view, constructive pedigree of the result should not have been harmed by its passage through set theory. He would then confidently use it to prove something further in his own system. McCarthy: > 2. If the result was derived in set theory and people are motivated to > take the trouble, they can label the result with what was used in > deriving it. Boyer: Perhaps there is a good scheme for such labeling, but I don't know it. The question comes down to defining "what was used in deriving it". If this is nothing but a full Hilbert-Goedel style FOL proof, it's not clear to me that a constructivist is going to be able, in general, to tell whether there is any constructive content to a given set theory theorem. I see I didn't say what I had in mind. Suppose we use an enriched set theory as David MacAllester advocates, and so do I. Suppose one of the enrichments is a weaker form of the power set rule acceptable to some flavor of constructivist. Suppose the proof of some result in set theory uses only the weaker rule. Suppose further that the logic includes a set of constructively correct rules. Suppose that the proof checker stores with the proof the rules that were used. Assuming all that we can make a mechanical constructivist rabbi that will certify that the proof is constructively kosher in his sect of constructivism.