I hope I am not being utterly naive in replying that the
problem I see is that once one records a result as theorem
of set theory, it loses its significance to constructivists.
Who knows, they might ask, what troublesome aspects of set
theory, such as the power set axiom or the law of the
excluded middle, was used in support of such a result, given
merely that it is a theorem of set theory?
1. If the result came originally from a "constructively correct"
theory, then going through set theory shouldn't harm it.
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.
3. Actually, for AI reasons, I don't give much weight to constructive
correctness.
4. Is there another proposal for an intermediate language?