In the following, $T$ is assumed to be a theory of Arithmetic strong enough to represent all computable functions and relations, including the provability relation $Proof(y,x)$ which holds if $y$ is the number of a proof of the sentence represented by $x$. Hence if $n$ is a Godel number of a proof of $\psi$ in $T$ then $T\vdash Proof(\underline{n},\ulcorner\psi\urcorner)$ and otherwise $T\vdash \neg Proof(\underline{n},\ulcorner\psi\urcorner)$. We represent $\exists v Proof(v,\ulcorner\psi\urcorner)$ by the expression $\Box\psi$.

I have so far proved the following in an exercise

  1. Show that if $T\vdash \Box\Box\alpha\rightarrow\alpha$ then $T\vdash \alpha$. (A proof that is nearly a copy of the proof of Lob's Theorem).

  2. If $T\vdash \alpha\rightarrow\neg\Box\Box\alpha$ then $T\not\vdash\alpha$.

  3. If $T\vdash \Box\neg\alpha\rightarrow\alpha$ then $T\not\vdash\neg\alpha$.

I next need to prove that if $T\vdash \alpha\rightarrow\Box\neg\alpha$ and $T\vdash \alpha$ then $T$ is $\omega$-inconsistent.

The given definition of $\omega$-inconsistent is the existence of a formula with one free variable, $\varphi(v)$, such that $T\vdash \exists v \varphi(v)$ and yet for every $n\in\mathbb{N}$ we have that $T\vdash\neg \varphi(\underline{n})$. My working hypothesis is that I should choose to investigate $\varphi(v)=Proof(v,\ulcorner\alpha\urcorner)$. The instructions don't make it clear whether the intention here is that these statements hold for all sentences $\alpha$ or just for some sentence $\alpha$--I've been trying to do the proofs while remaining agnostic about it.

A hint is given, that the following theorems could be helpful:

  1. For any $\gamma$ if $T\vdash \gamma\leftrightarrow \neg \Box\gamma$ then $T\vdash \gamma\leftrightarrow CON(T)$ where $CON(T)$ is $\neg\Box 0\ne 0$.
  2. If $T^* = T+\neg CON(T)$ then $Proof^*$ is a provability predicate in $T^*$, constructed analogously to $Proof$ in $T$. We can abbreviate $\exists v Proof^*(v,\ulcorner\gamma\urcorner)$ as $\Box^*\gamma$.

Here's what I have so far. I thought about using the contrapositive of the first assumption $T\vdash \neg\Box\neg\alpha\rightarrow\neg\alpha$. If for contradiction we further had $T\vdash \neg\alpha\rightarrow\neg\Box\neg\alpha$ then theorem 1 would apply and we could argue $T\vdash \neg\alpha\leftrightarrow CON(T)$ from which it would follow that $T\vdash \neg CON(T)\rightarrow \alpha$ so by the deduction theorem $T^*\vdash\alpha$ so by the second theorem $T^*\vdash \Box^*\alpha$. The contrapositive of the assumption for contradiction is $T\vdash\Box\neg\alpha\rightarrow\alpha$ which from the third exercise implies $T\not\vdash \alpha$. However by the second assumption $T\vdash \alpha$ so in fact this seemed like a waste of time. I get to say now that $T\not\vdash \Box\neg\alpha\rightarrow\alpha$ but this turns out not to have needed the theorems. I don't see how else to use the theorems.

Moreover, I'm not really clear on why I would do all this--I don't see what $T\not\vdash \Box\neg\alpha\rightarrow\alpha$ does for me now that I have it. This whole process of trying to use the two theorems seems irrelevant to proving $\omega$-inconsistency.

I've also tried proving $\omega$-inconsistency directly but not seeing a way. I can easily show $T\vdash \Box\alpha$ which is the same as half of what $\omega$-inconsistency, $T\vdash \exists v Proof(v,\ulcorner\alpha\urcorner)$. But I seem to also need to show that for all $n\in\mathbb{N}$ we have that $T\vdash \neg Proof(\underline{n},\ulcorner\alpha\urcorner)$ which is where I'm stuck.


1 Answer 1


You're right that you should prove $\omega$-inconsistency directly (and I don't quite see the point of the hint given). But you're missing a nice trick - non-uniformity.

Suppose $T\vdash\alpha\implies\Box\neg\alpha$ and $T\vdash\alpha$. Then there are two possible cases.

  • $T$ is inconsistent. In this case, $T$ is certainly $\omega$-inconsistent!

  • $T$ is consistent. We have $T\vdash \alpha$ by assumption, so since $T$ is consistent we must have $T\not\vdash\neg\alpha$. But at the same time, we clearly have $T\vdash\Box\neg\alpha$. This is an $\omega$-inconsistency: the first part says that no natural number codes a $T$-proof of $\neg\alpha$, while the second says that $T$ thinks that some number codes a $T$-proof of $\neg\alpha$.

The key point is that consistency buys us an additional fact: that $T\not\vdash\neg\alpha$. Using that the proof is easy, and the other case ($T$ inconsistent) is trivial. This kind of nonuniformity is often useful in such arguments.

  • $\begingroup$ I certainly "feel" the argument. But it seems to me, given the strict definition of $\omega$-inconsistency, that I need to show that for all $n\in\mathbb{N}$ we have $T\vdash \neg Proof(\underline{n},\ulcorner\alpha\urcorner)$. I would instinctively suppose that there is some $n$ such that $T\not\vdash \neg Proof(\underline{n},\ulcorner\alpha\urcorner)$ and try to produce a contradiction. This seems to be the same as $n$ being a proof of $\alpha$. Is it then immediate that from $T\vdash \Box\neg\alpha$ there must be a proof of $\neg\alpha$? This then seems to entail full inconsistency. $\endgroup$
    – Addem
    May 5, 2017 at 22:37
  • $\begingroup$ I think actually my biggest issue is how I officially handle $T\vdash \Box\neg\alpha$. It seems like my instincts take me father with this than I'm supposed to go: It tells me there is a proof of $\neg \alpha$ and all of the sudden I'm talking about full inconsistency--I must be over-stepping somewhere in this area but not seeing where. In fact I recall that, for some reason, we are not allow to infer from $T\vdash\Box\alpha$ that $T\vdash \alpha$. But then what I can do with it seems unclear. $\endgroup$
    – Addem
    May 5, 2017 at 22:44
  • $\begingroup$ @Addem "$T\vdash\Box\neg \alpha$" just says that $T$ proves the sentence "$T$ proves $\alpha$". There's no reason to assume that this means that $T$ actually proves $\alpha$, even if $T$ is consistent - consistent things can be wrong about lots of stuff! That handles one side of the confusion - what about the other, that you mention in your first comment? Well, this comes down to what consistent (sufficiently strong) theories can prove . . . (cont'd) $\endgroup$ May 5, 2017 at 22:47
  • $\begingroup$ Consistent theories (which are strong enough - extending Robinson's $Q$ will do the job) are $\Sigma_1$-correct - they prove any true $\Sigma_1$ sentence. Now, "$n$ is not a code for a $T$-proof of $\neg\alpha$" is $\Sigma_1$ (in fact, $\Sigma_0$), so - since $T$ actually doesn't prove $\neg\alpha$ - $T$ proves "$n$ isn't a code for a $T$-proof of $\neg\alpha$" for every natural number $n$. And this, together with "$T\vdash\Box\neg\alpha$, constitutes an $\omega$-inconsistency. $\endgroup$ May 5, 2017 at 22:47
  • $\begingroup$ Wait, I think there's a typo. $T\vdash \Box\neg \alpha$ says that $T$ proves that there is a proof of $\neg \alpha$. I would expect that to mean that it proves $\neg \alpha$, by following the proof that it proves it. But in any case, this all confuses me partly for the notation I'm not familiar with but also because I don't see how we can get around talking about the need, as in the definition of $\omega$-consistency, for "for all $n\in\mathbb{N}$ we have $T\vdash\neg Proof(\underline{n},\ulcorner\alpha\urcorner)$". $\endgroup$
    – Addem
    May 6, 2017 at 2:07

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.