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
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).
If $T\vdash \alpha\rightarrow\neg\Box\Box\alpha$ then $T\not\vdash\alpha$.
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:
- 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$.
- 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.