We have in the previous web pages set up the basic machinery of Gödel-numbering, representability of computable operations, the definition of $\omega $-consistency and so on to be able to prove the first incompleteness theorem.

The idea of the first incompleteness theorem is that, using
the diagonalisation lemma, for any recursive theory $T$
extending $\text{DOR}$ in the langauge ${L}_{A}$
there should be a ${L}_{A}$ sentence which says I am not
provable in $T$

. Now without the
diagonalisation lemma this seems a very difficult thing to write
down, but the trick of substitutions in the lemma makes this
possible. So we turn next to the theory $T$ and the
idea of provable

.

Sentences and formulas of ${L}_{A}$ can be given
Gödel-numbering as we have seen. But proofs in a recursive language
$L$ extending ${L}_{A}$ are finite strings of symbols and
so there is a Gödel-numbering of proofs too. Therefore, given $T$
we can consider the binary relation ${\mathrm{Proof}}_{T}(x,y)$
saying
$x$ is the Gödel-number of a proof from $T$ that
establishes the sentence with Gödel-number $y$

. This is just
a binary relation on natural numbers and it is therefore a sensible question
to ask how complicated it is. The key observation is that the rule of
first order logic are all computable, i.e. programmable on a computer,
and therefore there is a computer program that take a Gödel-number of
a proof and checks it follows the proof rules of first order logic.
If the set of axioms of $T$ is computable this program can
be modified to check that all the assumptions are axioms of $T$,
and thus we conclude that ${\mathrm{Proof}}_{T}(x,y)$ is a
recursive relation on the natural numbers.

Since it is a recursive relation on the natural numbers, there is a ${\Sigma}_{1}$ formula that represents it in $\text{DOR}$. To simplify notation we shall write this ${\Sigma}_{1}$ formula also as ${\mathrm{Proof}}_{T}(x,y)$. Now by diagonalisation there is a sentence $G$ of ${L}_{A}$ such that

$$\text{DOR}\u22a2G\leftrightarrow \forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231cG\u231d)$$This sentence $G$ can be thought of as asserting its own unprovability in $T$.

Let us first check that $G$ really is unprovable in $T$, provided $T$ is consistent and extends $\text{DOR}$. Suppose that $T\u22a2G$. Then there is a proof of $G$ in $T$ and hence a Gödel-number $x\in \mathbb{N}$ of this proof. Therefore the ${\Sigma}_{1}$ sentence ${\mathrm{Proof}}_{T}(x,\u231cG\u231d)$ is true and hence provable in $\text{DOR}$. But then $\text{DOR}$ proves $\neg \forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231cG\u231d)$ and hence $\text{DOR}$ proves $\neg G$. Since $T$ extends $\text{DOR}$, $T\u22a2\neg G$, which contradicts the consistency of $T$. Hence $T\u22acG$.

Now suppose $\neg G$ is provable in $T$, where $T$ is consistent and extends $\text{DOR}$. Then by the equivalence of $G$ and $\forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231cG\u231d)$ in $\text{DOR}$, $T$ proves $\neg \forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231cG\u231d)$ which is to say that $T$ proves $\exists x\u200a{\mathrm{Proof}}_{T}(x,\u231cG\u231d)$. But we also know from the previous paragraph that $G$ is not provable in $T$, which is to say that $\neg {\mathrm{Proof}}_{T}(n,\u231cG\u231d)$ is provable in $\text{DOR}$ and hence $T$ for each $n\in \mathbb{N}$. This is not a contradiction in itself, but does say that $T$ is $\omega $-inconsistent, i.e. for some $\theta \left(x\right)$, $T$ proves all of $\neg \theta \left(n\right)$ for all $n\in \mathbb{N}$ and also proves $\exists x\u200a\theta \left(x\right)$. This establishes the first incompleteness theorem.

Theorem.

Suppose $T$ is a recursive theory extending $\text{DOR}$ in a recursive language extending ${L}_{A}$. Suppose also that $T$ is $\omega $-consistent. Then there is a sentence $G$ such that $T\u22acG$ and $T\u22ac\neg G$.

We present two useful observations, which can both be verified by looking carefully at the proof just presented.

Theorem.

For each $\omega $-consistent recursive theory $T$ extending $\text{DOR}$ in a recursive language extending ${L}_{A}$ there is a consistent $\omega $-inconsistent extension of $T$.

Theorem.

For each $\omega $-consistent recursive theory $T$ extending $\text{DOR}$ in a recursive language extending ${L}_{A}$ there is a true ${\Pi}_{1}$ sentence $G$ of ${L}_{A}$ such that $T$ neither proves nor refutes $G$.

The importance of the second of these is that we have shown that $\text{DOR}$ proves all true ${\Sigma}_{1}$ sentences. It shows that no recursive theory can prove all true ${\Pi}_{1}$ sentences.