Incompleteness theorems and bounded reverse mathematics

[Richard Heck]

On 12/17/20 12:03 PM, Timothy Y. Chow wrote:
> There was a recent question on MathOverflow about whether the
> incompleteness theorems can be proved without exponentiation.
>
> https://mathoverflow.net/q/378777
>
> The short answer seems to be yes, but I'm posing this question here on
> FOM because I am curious as to whether this is a "folklore fact" or
> whether it has been written down in detail somewhere.
>  

I would think that Wilkie and Paris [1] answer this question
affirmatively, by showing that the *second* incompleteness theorem holds
for I\Delta_0 + \Omega_1 (S^1_2, more or less). As usual, that involves
showing how the proof of the *first* incompleteness theorem can be
formalized within I\Delta_0 + \Omega_1. See, in particular, Theorem 6.5,
which says that the derivability conditions can be proven in I\Delta_0 +
\Omega_1.

Their proof is very model-theoretic. If I remember correctly, Visser
gives a more proof-theoretic argument somewhere, but I can't find it at
the moment.

Riki

[1] A.J. Wilkie and J.B. Paris, "On the Scheme of Induction for Bounded
Arithmetic Formulas", /Annals of Pure and Applied Logic/ 35 (1987), 261-302