Friedman's enormous integers in real life. Are the examples unprovable in Peano?

Question

I'm interested in Harvey Friedman's paper on Enormous integers in real life.

Are all of the examples that Friedman describes in the paper unprovable in Peano Arithmetic? Given Friedman's work on Boolean Relation Theory, I assumed that they were all examples of incompleteness. I know that his Goodstein and Tree examples are unprovable in Peano.

What would be the proof theoretic strength that you would assign to each of his examples?

Answer 1

Most of the examples in the paper are provable in Peano Arithmetic. Assuming that the lower bounds given are relatively tight (Friedman gives upper bounds for some but not all of the examples), we get the following strengths:

1. This has growth rate of approximately $F_3(n)$, or an exponential tower. It will not be provable in Exponential Function Arithmetic, but provable in a stronger theory like Primitive Recursive Arithmetic.

3-7. These have growth rate of approximately $F_\omega(n)$, or the Ackermann function. These statements will not be provable in Primitive Recursive Arithmetic, but will be provable if you add one quantifier induction.

8. This has growth rate $F_{\omega^\omega}(n)$, equivalent to an $n$-ary Ackermann function. The theorem is not provable in PRA + one quantifier induction, but will be provable in PRA + 2 quantifier induction (and therefore Peano Arithmetic).

9-10. These have growth rate $F_{\varepsilon_0}(n)$. The corresponding theorems are not provable in PA, but are provable in a stronger theory like ACA (which stands for Arithmetical Comprehension Axiom).

11. This has growth rate $F_{\theta(\Omega^\omega,0)}(n)$. The theorem is not provable in $\Pi^1_2 + \text{BI}$, but is provable in $\Pi^1_1 - \text{CA}_0$.

12. The witness function for theorem 12.2 grows as $F_{\varepsilon_0}(n)$, whereas the witness function for theorem 12.4 grows as $F_{\theta(\Omega^\omega,0)}$, with corresponding results concerning their provability.