proofs of second incompleteness

Richard Kimberly Heck richard_heck at
Mon Sep 5 23:49:06 EDT 2022

On 9/5/22 11:59, martdowd at wrote:
> FOM:
> Does anyone know of any proofs of the second incompleteness theorem, 
> other than the standard proof-theoretic proof that
>  1) if PA is consistent then "I am not provable" is not provable
>  2) this can be formalized

The proof that Bezboruah and Sheparadson gave of G2 for Q is not of this 
kind. The proof is actually given for a deductively stronger system 
people now call PA- (and shows that PA- does not prove the consistency 
of ANY r.e. theory even pure logic). But this is still a weak system, 
interpretable in Q, and their proof does not work for stronger systems, 
so it's very much a special case.

Thomas Jech gave a purely semantic proof of G2 for ZFC, here:

Jech describes a way of proving this for PA by using the fact tha ACA_0 
proves the completeness theorem and is a conservative extension of PA. 
But I'm curious whether there's a more direct proof using the 
arithmetized completeness theorem and some coding of sufficiently 
complex (but still arithmetical) sets. The arithmetized completeness 
theorem implies that every consistent theory has a model of pretty low 


Richard Kimberly (Riki) Heck
Professor of Philosophy
Brown University

Office Hours: Monday 2-3, Wednesday 3-4
Personal link:

Pronouns: they/them/their

Email:rikiheck at
Google Scholar:
Research Gate:
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220905/5256acc6/attachment-0001.html>

More information about the FOM mailing list