Gödel's second incompleteness theorems

Question

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$

Answer 1

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$.