FOM: HA and PA

[Joe Shipman]

Friedman:
>>To factor out this difficulty when coming to HA, a very good idea is
to use
HA* instead of HA. HA* is a well known extension of HA by adding
ordinary
induction for all primitive recursive presentations of actual well
orderings. There is no requirment that well foundedness be proved in any

particular way. So a problem is: when is a sentence of PA provable in
HA*?
Incidentally, a sentence is provable in PA* if and only if it is true.<<

This is very interesting -- a nonrecursive axiomatization!  The
decomposition of "constructive proof" (an informal concept) into "proof
that a primitive recursive relation R is a well-ordering" and "proof
from HA + 'R is a well-ordering' " allows the constructivist to
gradually extend his system by accepting more countable ordinals,
analogously to a classical mathematician working in in RCA0 extending
his system by accepting more set existence axioms.  This suggests a form
"reverse constructive mathematics" could take -- show the equivalence
(over HA) of various arithmetical theorems with the well-orderedness of
primitive-recursively presented relations.

Harvey, how do you show your last assertion?  Is there a simple way to
pass from an arithmetical sentence to a primitive-recursively presented
relation whose well-orderedness is equivalent (over PA) to the
sentence?  And what partial results exist on which theorems of PA are
provable in HA*?

-- Joe Shipman