Incompleteness theorems and bounded reverse mathematics

[Timothy Y. Chow]

On Fri, 18 Dec 2020, Richard Heck wrote:
> 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.
[...]
> [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

Thanks for this reference, and thanks also to Martin Dowd for a pointer to 
Cook's earlier paper, "Feasibly constructive proofs and the propositional 
calculus."

Goedel's second incompleteness theorem is a rather good test case for a 
discussion of what it means to "write down a correct and complete proof." 
Larry Paulson's 2015 paper, "A mechanised proof of Goedel's incompleteness 
theorems using nominal Isabelle," makes it clear that the published proofs 
of the 2nd theorem can all be criticized---by a sufficiently pedantic 
reader---as containing elided details or even misleading claims.  And this 
is even without asking for a demonstration that the proof can be 
formalized in bounded arithmetic.  So one has to be prepared to accept a 
certain amount of sketchiness; the question is how much leeway one is 
willing to grant.

Cook's paper admits that it provides only a sketch.  The paper by Wilkie 
and Paris is much more detailed and I think meets "normal" standards for a 
complete proof---though they explicitly "leave to the reader" a number of 
tedious verifications.

Tim