# Trying to understand self-reference as it relates to Godel's Second Incompleteness Theorem

As noted in this post, I'm trying to understand how a sufficiently powerful consistent theory $T$ can prove statements about itself without contradicting Godel's Second Incompleteness Theorem. Let $Prb_T \sigma$ represent $T \vdash \sigma$, $Cons T = \neg Prb(0=1)$. I know that assuming $T$ is consistent, $T \vdash Cons T$ is a contradiction. I also know from this answer that $T \vdash \neg (0 = 1)$ is true. but what about:

1. $T \vdash Prb_T Cons T$

2. $T \vdash \neg(p \wedge \neg p)$

3. $T \vdash Prb_T(\neg (p \wedge \neg p))$

4. $T \vdash (Prb_T(Cons T) \rightarrow \neg Cons T)$

5. $T \vdash (Prb_T(\neg(p \wedge \neg p)) \rightarrow \neg (p \wedge \neg p))$

I'm thinking that 4 and 5 are both formulazations of the theorem within $T$ so they are valid. If that's correct then 1 should not be valid since it would imply $\neg (Cons T)$. I'm not sure though about 2 and 3.

• $\lnot (p \land \lnot p)$ is a tautology; thus provable in propositional calculus alone and thus provable in every theory $T$. – Mauro ALLEGRANZA Jan 21 '16 at 19:23
• @Carl: You might want to even add that it is possible for a consistent theory $T$ to prove $\lnot\operatorname{Con}(T)$. For example, $\sf PA+\lnot\operatorname{Con}(PA)$ is such example. – Asaf Karagila Jan 22 '16 at 11:53
• @Asaf Karagila: already added - I think it was a point of confusion in the question, where the OP thought there would be a contradiction. – Carl Mummert Jan 22 '16 at 11:55
• You're right, of course, @Noah – Carl Mummert Jan 22 '16 at 18:07

Here $T$ is a sufficiently strong, effective theory of arithmetic, $\text{Pvbl}$ is the formalized provability predicate of $T$, and $\text{Con}(T)$ is the formalized statement of $T$'s consistency.

The case of #1, $T \vdash \text{Pvbl}(\text{Con}(T))$, is interesting.

If $T$ is satisfied by the standard model of arithmetic, then we have for each $\phi$ that $T \vdash \text{Pvbl}(\phi)$ if and only if $T \vdash \phi$ (weaker assumptions on $T$ will also cause that equivalence to hold). By the second incompleteness theorem, it is impossible for $T \vdash \text{Con}(T)$. So if $T$ is sufficiently reasonable (e.g. if it is satisfied by the standard model), then we will have $T \not \vdash \text{Pvbl}(\text{Con}(T))$. The usual term for this property is "soundness", and in particular the $T$ here would be sound for $\Sigma_1$ formulas such as $\text{Pvbl}(\phi)$.

On the other hand, we know in general that $T \not \vdash \text{Con}(T)$. So $T + \lnot \text{Con}(T)$ is consistent. Let $R = T + \lnot \text{Con}(T)$. Then, for all $\phi$, we will have $R \vdash \text{Pvbl}_R(\phi)$, assuming that we take the "natural" effective axiomatization of $R$.

The proof is as follows. First, $R \vdash \lnot \text{Con}(T)$, which means that $R \vdash \text{Pvbl}_T(\phi)$ for all $\phi$, because $R$ can formalize the usual arguments showing that every sentence is provable from an inconsistent theory. Second, $R \vdash \text{Pvbl}_T(\phi) \to \text{Pvbl}_R(\phi)$, because $T$ is a subtheory of $R$ and because we chose the axiomatization of $R$ so that $R$ can prove $T$ is a subtheory of $R$.

So, if we take the $T$ in the question to be this $R$, we will have $R \vdash \text{Pvbl}_R(\text{Con}(R))$. Of course, we do not have $R \vdash \text{Con}_R$. In particular, the theory $R$ is not satisfied by the standard model, even though it is consistent. This is because $R$ proves the existence of numbers (such as a coded proof of $\text{Con}(R)$) which cannot be found in the standard model. Even more precisely, the theory $R$ is not sound for $\Sigma_1$ sentences;

We can also see that $R$ proves $\lnot \text{Con}(R)$. This does not contradict anything - it is possible for a theory to "prove it is inconsistent", even if the the theory is actually consistent, as this example shows.

So the answer to #1 is that more information about $T$ is needed to know whether $T \vdash \text{Pvbl}( \text{Con}(T))$.

Carl has addressed the most interesting of the bullet points. To round out his answer:

2 is certainly true (via LEM), and 3 is true by reflection (if I prove $p$, then I prove that I prove $p$).

4 is indeed a formalization of Godel's theorem, and is true for sufficiently strong theories.

Finally, let's look at 5. 5 has the form $T\vdash \alpha\implies \beta$, where we already know (2) that $T\vdash\beta$. So, without any attention paid to $\alpha$, we know that $T\vdash \alpha\implies\beta$. So 5 is true, trivially.