PRA as a foundation
David McAllester (dam@ai.mit.edu)
Fri, 14 Oct 94 17:51:28 EDT
At a recent meeting I was discussing the suggested use of primitive
recursive arithmetic (PRA) as a foudational logic for the QED project.
It seems to me that the logics of HOL, MIZAR, IMPs, or Ontic all have
the property that the vast majority of theorems stated in one of these
locics could be automatically translated in a useful way into
statements in any of the other logics. Hence any one of them could be
plausibly be used as a "lingua franca". However, the situation seems
quite different with PRA. As an example, consider the
Schroder-Burnstein theorem (SB) which states that if there is an
injection of A into B and an injection of B into A then there must be
a bijection between A and B. This can be stated in any of the above
mentioned logics and a translation of the statement between logics
would leave it in a recognizable and usable form. However, if I
translate the theorem from, say, MIZAR, into PRA it looks like "MIZAR
|- SB" because SB can not be stated in the first order language of
arithmetic. When I translate this back into, say, HOL using the
obvious translation of PRA thoerems into HOL I get "MIZAR |- SB".
This is MUCH more difficult to use than a direct statement of SB in
HOL, which is what I get from a direct translation from MIZAR to HOL.
(I am aware that MIZAR is more expressive than HOL so my translator
would handle only a subset of MIZAR and would translate theorems about
sets to polymorphic theorems which effectively quantify over types
rather than sets. There is no problem expressing SB as a polymorphic
theorem about types A and B.)
My concern is that use of PRA as a central logic would effectively
block communication between more expressive systems because
translations through PRA convert perfectly meaningful statements about
sets into hard to use meta-theorems about obscure proof
systems.
Has this concern been raised before? Are there any comments?
David