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.
The full utility of qed requires such an intermediary, and it must be
powerful expressively. Is there another candidate?
*****
There is also a more ambitious idea. It is that other systems
represent restrictions of set theory to a particular collection of
formulas, to the use of a particular set of theorems as derived proof
rules and to a particular class of proof strategies. I would like to
see this more ambitious idea demonstrated, e.g. for the Boyer-Moore
system.
*****
This idea is distinct from the more modest idea above, and it is
mostly laziness that makes me put them in the same message. Please
react to them separately.