FOM: Translatability

[Till Mossakowski]

Consider the following facts:

1. Boolean algebras and Boolean rings are intertranslatable.
2. Classical propositional logic and Boolean algebras are 
   intertranslatable.
3. Intuitionistic higher-order logic and topoi are 
   intertranslatable.
4. Intuitionistic propositional logic and Heyting algebras are 
   intertranslatable.
5. All relevant mathematics is translatable to ZFC.
6. Group theory is translatable to ZFC.

What are the exact gains and losses of each translation?
In which cases, or for which purposes, does intertranslatability mean
that exactly the interesting things are preserved, and the
non-interesting things need not be preserved?
What are the (properties of the) notions of translation behind the
scene?
Which properties do translations have to satisfy to be relevant for
f.o.m.?

Much has been said to these questions on FOM already. One position 
might be summarized as: 1. to 4. have essential losses, while 5. and 6. 
don't, but instead have clear gains. Another (well, a bit extreme) 
position might be just the other way round. Perhaps it helps to 
address this in a more focused form.

Till Mossakowski