Here is a longer explanation of my current understanding. PRA seems
motivated by a series of reasonable objectives.
Objective 1. The QED project should keep track of what axioms are used for each theorem
proved.
I think this objective is reasonable but arguable. I am not convinced that
careful accounting of axioms is needed since most mathematicians aren't
going to care about the details of the foundation --- any sufficiently rich
foundation will be equivalent to ZFC for all practical purposes in "ordinary" mathematics.
However, assuming that we do want to keep track of what principles are used
for any given theorem then the QED data base should consist of a set of
pairs of theorems and systems --- a theorem and a name of the system in which
it can be proved.
Objective 2. We want to build and use translators between the logics of the various systems
so that each system can use results proved by other systems in constructing still more
proofs.
This seems reasonable. However, if a single system captures the
hearts and minds of mathematicians then the logic of that system could
become a defacto standard and translation could become irrelevant. No
matter how strong our cooperative tendencies are, I think that
ultimately the nature of machine verification will be decided in a
free market fasion with mathematicians playing the role of consumers.
A single system will probably dominate.
Objective 3. Translators between systems should be formally verified.
This seems reasonable but arguable. I think an unverified translator is better than
no translator. Given the current state of the art in verification,
verified code useually requires an order of magnitude more time to construct.
There are two approaches to machine verifying intersystem translations --- syntactic
and semantic. One can either prove that the translations preserve provability
or that the translations preserve truth. Proving that the translations
preserve truth requires a logic in which the semantics of the two systems in question
can be defined. This is problematic because defining the semantics of a system
requires a stronger system. For example the semantics of ZFC can not be defined in ZFC.
A natural way around this is to make a stronger system by assuming the existence of
large cardinals. A system for verifying that translations preserve truth would have
to assume cardinals larger than those assumed by any of the systems being translated.
I find this perfectly acceptable and the easiest approach
to verifying translations since working semantically is often more efficient
(gives shorter proofs). But the semantic approach to verifying translators
is in conflict with the following objective.
Objective 4. The logic in which translations are verified should be as
primitive as possible so as to be acceptable to the widest possible variety
of logicians.
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.
Objective 5. All pairs of a theorem and a system in the central data base should
be verified in a central uncontroversial logic (such as PRA).
This is the most controversial objective. Doing this greatly increases
the cost of constructing each individual system because the systems
must now output PRA proofs of metaformulas of the form S |- Phi.
Every decision procedure used in the system must be built to construct
a trace of its execution that can be converted to a PRA proof. It
also dictates a syntactic approach to proving the correctness of the
translators. In my opinion it greatly increases the cost of QED.
I think cost (person years) is going to be the main obstical.
David