I was proposing set theory as an intermediary that would permit a
theorem proved in one system to be translated to other systems and
used there without being proved again.
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?
It is indeed useful to consider the idea that "other systems represent
restrictions of set theory to a particular collection of formulas".
But how this could be done in a way satisfactory to constructivists, I
am not sure. A troublesome aspect is that even axiom-free first order
logic uses the law of the excluded middle freely, whereas, as best I
understand it, constructivists object to the use of the law of the
excluded middle except in contexts in which all predicate and function
symbols are recursive, e.g., I believe it is a constructivist theorem
that every integer is either a prime or not a prime, because there is
an effective check for primality.
There are versions of first order logic (such as Kleene's presentation
of natural deduction) which make it syntactically easy to tell when a
given first order logic proof is constructive (in Kleene's case, never
more than one formula on the righthand side of the sequent arrow). So
perhaps there is an agreeable universal calculus that is, on the one
hand, strong enough to contain first order logic and set theory but
which is also, on the other hand, a calculus with a subset of proofs
easily recognizable as constructive and strong enough to contain all
the work of constructivism.
Bob