Incompleteness theorems and bounded reverse mathematics

[martdowd at aol.com]

 Tin,
See section 4 of Cook75,  Everything needed to prove second incompleteness is provable in PV.https://dl.acm.org/doi/10.1145/800116.803756
- Martin Dowd

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.

 
 
 
-----Original Message-----
From: Timothy Y. Chow <tchow at math.princeton.edu>
To: fom at cs.nyu.edu
Sent: Thu, Dec 17, 2020 9:03 am
Subject: Incompleteness theorems and bounded reverse mathematics

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.

First of all there is some question as to what "without exponentiation" 
means.  The person who asked the question on MathOverflow was reading Ed 
Nelson's book "Predicative Arithmetic," and in that context, the natural 
question is perhaps whether the incompleteness theorems are interpretable 
in Q (Robinson's arithmetic).  That's an interesting question, but in what 
follows, I will regard "without exponentiation" as meaning provable in 
bounded arithmetic, say S^1_2.  So the question becomes a question in 
"bounded reverse mathematics."

A second issue is that in bounded arithmetic, it's problematic to talk 
about sets of axioms that are "hard to compute."  But I am happy to 
restrict attention to sets of axioms that can be expressed using a 
Sigma^b_1 formula.  Instead of "incompleteness theorem" we can speak of 
"incompleteness theorem schema," with one instance for every such 
Sigma^b_1 formula.

I looked at Buss's thesis, which carries out the arithmetization of syntax 
in the context of bounded arithmetic.  He proves the incompleteness 
theorems for S^1_2.  However, the proof of Theorem 9 for example appeals 
to Gentzen's cut-elimination theorem, and hence it is not automatic that 
Theorem 9 is provable in bounded arithmetic.

Checking some of the "usual suspects" such as Hajek and Pudlak's book and 
Cook and Nguyen's book did not turn up an explicit statement either.  For 
example in Hajek and Pudlak's book, there is a discussion of 
incompleteness theorems *for* weak systems but not, as far as I could see, 
a discussion of proving the incompleteness theorems *in* weak systems.

Tim
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20201218/19a0b22f/attachment.html>