Incompleteness theorems and bounded reverse mathematics
Timothy Y. Chow
tchow at math.princeton.edu
Thu Dec 17 12:03:12 EST 2020
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
More information about the FOM
mailing list