> 3. Actually, for AI reasons, I don't give much weight to constructive
> correctness.
You are not alone. A *lot* of people give little or no weight to
constructive correctness, and for a number of reasons. It is
nevertheless true that a quite substantial portion of the people
currently working on mechanical proof-checking *are* concerned about
constructive matters. This is perhaps a quite inevitable state of
affairs -- perhaps many of those who are motivated to get things as
correct as possible are bound to pay attention to the critics of
current mathematical orthodoxy and its classical, set theoretic
practice.
> 1. If the result came originally from a "constructively correct"
> theory, then going through set theory shouldn't harm it.
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. Admittedly, to you this may be
of no concern.
> 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.
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 should correct a previous message and identify the "only
one disjunct on the righthand side" syntactic restriction of classical
logic to intuitionistic logic I mentioned as being an intuitionistic
sequential calculus of Gentzen, which is presented in Kleene's
"Introduction to Metamathematics". A most knowledgeable friend, in
correcting me, adds that the essential difference is in the right
negation rule, which can only be applied when the right hand side is
empty.)
> 4. Is there another proposal for an intermediate language?
It seems to me that the alternative to set theory as the single
intermediate language is not another single, universal, intermediate
language but a number of languages, all tied together with
metamathematical connections. Metamathematical results could be
mechanically proof-checked with checkers for some of the weaker sorts
of logics that proof theorists have long used. I think that Hilbert
and Bernays recommended something like Skolem's primitive recursive
arithmetic as the basis upon which to do metamathematics, but
Feferman's FS0 seems much more usable, e.g., it has "cons" and
quantifiers. Perhaps something even weaker will suffice, thus
accommodating those who suspect that the full set of primitive
recursive functions is a fantasy. Perhaps we won't need a logic with
functions of more than polynomial complexity in order to prove that,
say, any proof of a certain class of theorems in the Coq logic can
always be transformed to a proof of a related theorem in the Mizar
logic. One can make some progress merely by writing and executing
functions that actually do such proof transformations, but I suspect
that it will be eventually be practically necessary to prove the
correctness of such functions, rather than to run them, simply because
the transformed proof objects will be too large. I suspect that such
correctness proofs, a kind of baby metamathematics, can be carried out
in weak logics that are widely supported.
It would be divine if there could be agreement on a single, very
strong, universal language, but I doubt that such agreement is to be
found. It seems sensible for us to see what we can agree upon, if
anything, and then treat what we cannot agree upon not as doctrinal
issues that separate us but merely as interesting logical variations
that support results which can sometimes be transformed from one
variation to another. I imagine that ring theorists don't disparage
group theorists, but rather take advantage of their theorems as much
as possible. But currently, the users of the many mechanical proof
checking systems manage to depend upon the results of the use of other
systems about as little as one might imagine.
Bob