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

Question

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.

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.