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.

  • 1
    $\begingroup$ $\lnot (p \land \lnot p)$ is a tautology; thus provable in propositional calculus alone and thus provable in every theory $T$. $\endgroup$ – Mauro ALLEGRANZA Jan 21 '16 at 19:23
  • $\begingroup$ @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. $\endgroup$ – Asaf Karagila Jan 22 '16 at 11:53
  • $\begingroup$ @Asaf Karagila: already added - I think it was a point of confusion in the question, where the OP thought there would be a contradiction. $\endgroup$ – Carl Mummert Jan 22 '16 at 11:55
  • $\begingroup$ You're right, of course, @Noah $\endgroup$ – 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.