David's comments the above objective:
> Objective 4 seems to dictate a syntactic approach to verifying
> translators. If f is a translator from system S1 to system S2 the
> correctness theorem states that if S1 |- Phi then S2 |- f(Phi). I was
> confused about the role of PRA here and assumed that a central use of
> PRA would force the translation f(Phi) to be a "meta" formula rather
> than a "Platonic" formula (one that talks directly about arbitrary
> sets). But nothing here is preventing f(Phi) from being a direct
> (Platonic) set-theoretic formula. PRA seems adequate once we are
> committed to a syntactic approach to verifying translators.
>
If we have n systems, then we need n*(n-1) translators.
Sounds like a bit of work unless n = 1.
Another approach is to have one, very strong system, into which anything
can be translated, and from which we can translate, but not everything,
into weaker systems. This needs only 2(n-1) translators.
-- Piotr (Peter) Rudnicki