# If $T\vdash \alpha\rightarrow \Box\neg\alpha$ and $T\vdash \alpha$ then $T$ is $\omega$-inconsistent

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.

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.

• 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. May 5, 2017 at 22:37
• 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. May 5, 2017 at 22:44
• @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) May 5, 2017 at 22:47
• 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. May 5, 2017 at 22:47
• 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)$". May 6, 2017 at 2:07