# Gödel's second incompleteness theorems

Usually Gödel's second incompleteness theorem is interpreted thus: "No sufficiently strong formal theory can prove its own consistency, assuming it is consistent", but in the book Per Lindstroem "Aspects of incompleteness", in Chapter 2 we prove Theorem 7, which, as far as I understand, is about, that a certain sentence, which encodes statement of the consistency of the theory, can still be proved in it. So, is this interpretation of the second incompleteness theorem is not entirely correct?

We say that $\tau^*(x)$ binumerates T in T if for every sentence $\phi$:

1. $\phi\in T\leftrightarrow T\vdash\tau^*(\phi)$
2. $\phi\not\in T\leftrightarrow T\vdash\neg\tau^*(\phi)$

Statement $\phi\in T$ means that $\phi$ is axiom of T. $(\tau|x)(y)$ means $\tau(y)\land y\le x$ • What does "binumerating" mean? Mar 22, 2018 at 20:26
• A crucial detail is missing in the claim above : "No sufficient strong formal theory can prove its own consistency, ASSUMING IT IS CONSISTENT" Mar 22, 2018 at 20:26
• @Taroccoesbrocco it is mean that there is the formula in the language in arithmetic such that: 1. $T\vdash \phi \leftrightarrow T\vdash \tau^*(\phi)$ 2. $T\not\vdash \phi \leftrightarrow T\vdash ~\tau^*(\phi)$ Mar 22, 2018 at 20:28
• @SmolinVlad I suspect there is a typo ... Mar 22, 2018 at 20:40
• I assume "$\theta(\psi)$" is shorthand for "$\theta([\psi])$," where "$[\psi$]" is the Godel number for the sentence $\psi$. If so, then I think (unless I'm missing something) no binumerating formulas exist for "reasonable" $T$: if $\tau^*$ binumerates $T$ in $T$ by this definition, then $\{\varphi: T\not\vdash\varphi\}$ is computably enumerable; since $\{\varphi: T\vdash\varphi\}$ is always computably enumerable for "reasonable" $T$, this means that if a formula binumerating $T$ in $T$ exists and $T$ is "reasonable" then the deductive closure of $T$ is computable, and this can't happen. Mar 22, 2018 at 21:10

This is a well known example that I believe is originally due to Feferman, "Arithmetization of Metamathematics in a General Setting", Fund. Math. 49, 1960. To phrase it more directly, let $\tau(n)$ be a formula that defines the set of axioms of a consistent theory $T$ extending PA, and let $\tau'(n)$ be $$\tau'(n) \equiv \tau(n) \land \text{Con}\{\tau(1), \ldots, \tau(n) \}$$

Then $\tau'(n) \leftrightarrow \tau(n)$ holds for each standard $n$, but $T$ cannot prove $(\forall n)[\tau(n) \leftrightarrow \tau'(n)]$.

Also, if we let $T'$ be the theory enumerated by $\tau'$ then PA will prove $T'$ is consistent. This is because $\tau'$ is careful not to include any axiom that could possibly lead to an inconsistency with axioms $\tau'$ has already accepted for smaller $n$.

The reason Feferman proposed this is to illustrate the intensional character of the provability predicate. Two formulas can define the same theory in the standard model, while not being provably equivalent.

This was previously asked in a different way on MathOverflow; see my answer there.

Here is another example that may be even more striking. Let $T$ and $S$ be effective theories with $\text{PA}\vdash \text{Con}(S) \to \text{Con}(T)$, where $\tau$ enumerates the theory $T$, and let $$\tau''(n) \equiv \text{Con}(S) \land \tau(n).$$ Then, working in PA, we can reason by cases:

• If Con(S) then we have $\text{Con}(T)$ by assumption, and also $(\forall n)[\tau(n) \leftrightarrow \tau''(n)]$, so the theory $T''$ enumerated by $\tau''$ is consistent.

• Otherwise, if $\lnot \text{Con}(S)$, then $\tau''(n)$ is identically false, and so again the the theory $T''$ enumerated by $\tau''$ is consistent.

Thus PA proves $\text{Con}(T'')$ (defined using $\tau''$) even if $T$ is something like ZFC whose consistency is not provable in PA.

The issue, of course, is that PA does not prove in general that $(\forall n)[\tau(n) \leftrightarrow \tau''(n)]$ and so PA cannot always tell that $T''$ is the same as $T$.

• Beat me to it (and a much better answer), +1! Mar 22, 2018 at 22:01
• Feferman's example is sometimes glossed as "PA proves that the largest consistent initial segment of the PA axioms gives a consistent theory". Of course, "the largest consistent initial segment of the PA axioms" is the entire set of PA axioms, but that is exactly what is not provable in PA! Mar 22, 2018 at 22:07