On $\alpha$-largeness and the Paris-Harrington principle in $\mathrm{RCA}_0$ and $\mathrm{RCA}_0^{\displaystyle{*}}$

We examine, within $\mathrm{ RCA}_0$, the treatment by Ketonen and Solovay on the use of $\alpha$-largeness for giving an upper bound for the Paris--Harrington principle. This proof works fine in $\mathrm{ RCA}_0^{ \displaystyle{ *}}$ for every fixed standard dimension. We also show how to modify the arguments to work within $\mathrm{ RCA}_0^{ \displaystyle{ *}}$ for unrestricted dimensions. To the author's knowledge, this is the first time that it is confirmed that the treatment can be done within $\mathrm{ EFA}$ without some transfinite induction added.

Categories: math.LO