By induction on $n$ variables I can show that for any meta-natural number $n$, PA proves well-foundedness of $\omega^n$. However it is well known that PA proves well-foundedness of $\omega^\omega$ since its proof-theoretic ordinal is $\varepsilon_0$. How can I prove this in PA?
6
-
$\begingroup$ It seems to me that one can define in PA the concept $\omega^n$ for a natural number variable $n$, and can prove in PA with induction "For all natural numbers $n$, $\omega^n$ is well-founded". From this it readily follows that one can define and prove well-founded $\omega^\omega$. $\endgroup$– Sridhar RameshCommented Aug 11, 2023 at 19:26
-
1$\begingroup$ I feel that this question is fairly basic and perhaps would be more suited for Math.StackExchange. Though, in short the answer is that in order to prove in $\mathsf{PA}$ an instance $\mathsf{TI}_{\omega^\omega}[\varphi]$: $\forall \alpha<\omega^\omega(\forall \beta<\alpha\,\varphi(\beta)\to\varphi(\alpha))\to\forall \alpha<\omega^\omega\,\varphi(\alpha)$ of the scheme of transfinite induction for $\omega^\omega$, one, for example, could prove in $\mathsf{PA}$ by induction that for all $n$: $\forall \alpha<\omega^\omega(\mathsf{TI}_{\alpha}[\varphi]\to \mathsf{TI}_{\alpha+\omega^n}[\varphi])$. $\endgroup$– Fedor PakhomovCommented Aug 11, 2023 at 20:45
-
3$\begingroup$ Over in mathoverflow.net/a/139015/297 , I wrote out a proof that, if PA proves that X is well ordered, then PA proves that $\omega^X$ is well-ordered. Another answer to that question recommended Pohlers "Proof Theory: An Introduction" as a good source for this material. $\endgroup$– David E SpeyerCommented Aug 11, 2023 at 21:30
-
3$\begingroup$ Maybe it's just because I am self-taught in logic, but I don't think this is basic at all! It seemed pretty hard to me, and I didn't come across any books which did this. $\endgroup$– David E SpeyerCommented Aug 11, 2023 at 21:31
-
$\begingroup$ @DavidESpeyer I think that in some form this (the lower bound for the proof-theoretic ordinal of $\mathsf{PA}$) is covered in any book I know that presents the ordinal analysis of PA, e.g. Takeuti, Pohlers, Girard. $\endgroup$– Fedor PakhomovCommented Aug 12, 2023 at 10:16
|
Show 1 more comment