Return to Revisions

$\def\prf{\mathrm{Prf}}\def\pr{\mathrm{Pr}}\def\con{\mathrm{Con}}\def\f{\ulcorner\bot\urcorner}\def\ha{\mathsf{HA}}$Let $\prf(x,y)$ be the formalized proof predicate for either HA or PA (it doesn’t matter), and $$\begin{align*} \pr(y)&\equiv\exists x\,\prf(x,y),\\ \con&\equiv\neg\pr(\f),\\ T&=\ha+\con\lor\neg\con,\\ \phi(x)&\equiv\con\lor\prf(x,\f). \end{align*}$$ Clearly $\ha\subseteq T\subseteq\mathsf{PA}$. We have $$T\vdash\forall x\,(\phi(x)\lor\neg\phi(x))$$ as assuming either $\con$ or $\neg\con$, $\phi(x)$ reduces to the decidable formula $\prf(x,\f)$. Since $\exists$ distributes over $\lor$, $$T\vdash\exists x\,\phi(x)\equiv\con\lor\pr(\f).$$ This is an instance of excluded middle, hence $$T\vdash\neg\neg\exists x\,\phi(x).$$ However, $$T\nvdash\exists x\,\phi(x):$$ if we assume for contradiction $\exists x\,\phi(x)$ is provable in $T$, then it is in particular provable in $\ha+\neg\con$, thus $$\ha\vdash\neg\con\to\pr(\f).$$ Using the numerical existence property for negative extensions of HA, there is $n\in\mathbb N$ such that $$\ha\vdash\neg\con\to\prf(\overline n,\f).$$ However, HA/PA is consistent, hence $n$ is not actually a code of a proof of $\bot$. Thus the decidable sentence $\prf(\overline n,\f)$ is false, and therefore refutable in HA. It follows that $$\ha\vdash\con,$$ contradicting Gödel’s theorem.