FOM: HA and PA

[Harvey Friedman]

Reply to Shipman 6/28/00 10:08AM:

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 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.

This particular formulation is probably not in the cards. However reverse
constructive mathematics makes sense, and needs more development.

>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*?

Every true sentence without "therexist", "or", is provable in HA*. Every
true Sigma-0-3 sentence is true.

Let A be a true sentence of PA. Look at the tree of unsecured sequences for
finding a Skolem function for its negation. This is actually well founded.
Make up an arithemtically defined function which is, demonstrably, a Skolem
function for its negation if and only if it is false. Then in PA* it is
provable that this made up function is not a Skolem function for its
negation, by transfinite induction on the tree. Hence A.