> 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.