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 <qed@mcs.anl.gov>; 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 <jmc@sail.Stanford.EDU>
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.