To study the Gödel incompleteness theorems we need to choose and study an appropriate logical theory and set of formal rules, and in this an appropriate minimal theory of arithmetic. For the logical theory, we take first-order logic. There are a few choices for the minimal first-order theory or arithmetic, including $Q$ and also theories in a purely relational language, which are convenient for some reasons, but I prefer to concentrate on a slightly stronger theory $\text{DOR}$ because it has a clear algebraic meaning. This page introduces the reader to $\text{DOR}$.

As explained in The Mathematics of Logic

, there is a system -
first-order logic - which is described precisely by proof rules that
could be programmed into a computer to check, which is expressive
enough for everyday mathematics, and in which all everyday
mathematical proofs can be formalised.

We write $\Sigma \u22a2\sigma $ to say that from additional non-logical axioms $\Sigma $ the system can derive $\sigma $, i.e. there is a formal proof of $\sigma $ in the system with additional non-logical axioms $\Sigma $. You might think that to make progress with such a system it would be necessary to produce many many detailed and boring formal proofs. (They are all long!) But it happens that $\Sigma \u22a2\sigma $ is equivalent to a related notion, $\Sigma \models \sigma $, and we can use this instead. $\Sigma \models \sigma $ means that every structure (an algebraic object like a group or a ring) that makes $\Sigma $ true must make $\sigma $ true.

The implication
$\Sigma \u22a2\sigma $ implies
$\Sigma \models \sigma $

is called the Soundness Theorem, as it says the system
$\u22a2$ is sound

, or correct

, and the implication
$\Sigma \models \sigma $ implies $\Sigma \u22a2\sigma $

is
known as the Completeness Theorem as it says that $\u22a2$ is
strong enough

or complete

so as to formalise all informal
mathematical proofs. Both these results are discussed in The
Mathematics of Logic

and the Completeness Theorem is proved fully
there. A sketch proof of the Soundness Theorem is also give, and
further details of it are available on these web pages. Our approach
here is to use $\models $ throughout, and appeal to Soundness and
Completeness to see that what we said about $\models $ applies
equally well to $\u22a2$. In particular, we can concentrate on
the semantic meaning of our non-logical axioms, rather than the formal
semantics of how they are to be written down.

The first-order
theory we are about to introduce is an algebraic theory in what
I consider as the usual

language of arithmetic, ${L}_{A}$.
This language has two constants, $0$ and $1$, two binary
function symbols $+$ and $\times $, and a binary relation
$<$. These symbols are all thought of in the usual way as zero,
one, addition, multiplication and order, and in particular they are
interpreted in $\mathbb{N}$ in the usual way. The ${L}_{A}$
structure $\mathbb{N}$, or more properly
$(\mathbb{N},0,1,+,\times ,<)$,
is called the *standard model* of arithmetic.
(Note that in all this discussion zero will be considered as a natural
number.) Other popular languages omit one or two of these symbols
(for example, $<$ is strictly speaking not needed as it is
usually possible to define it from addition) or add the successor
function $S\left(x\right)=x\mathrm{+1}$.

The axioms that follow say what it means for an
${L}_{A}$-structure to be the *nonnegative part of a
discretely ordered ring*. The set of these axioms could more accurately and
precisely be given the name ${\text{DOR}}^{\u2a7e0}\left({L}_{A}\right)$
to indicate the precise algebraic content and the choice of language we made.
This is a bit long-windeed to write and we will usually write
${\text{DOR}}^{\u2a7e0}$ or just $\text{DOR}$.
The same theory is often called ${\text{PA}}^{-}$.

Definition.

- $\forall x\u200a\forall y\u200a\forall z\u200a\left(\right(x+y)+z=x+(y+z\left)\right)$
- $\forall x\u200a\forall y\u200a(x+y=y+x)$
- $\forall x\u200a\forall y\u200a\forall z\u200a\left(\right(x\times y)\times z=x\times (y\times z\left)\right)$
- $\forall x\u200a\forall y\u200a(x\times y=y\times x)$
- $\forall x\u200a\forall y\u200a\forall z\u200a(x\times (y+z)=(x\times y)+(x\times z\left)\right)$
- $\forall x\u200a((x+0=x)\wedge (x\times 0=0))$
- $\forall x\u200a(x\times 1=x)$
- $\forall x\u200a\forall y\u200a\forall z\u200a\left(\right(x<y\wedge y<z)\to x<z)$
- $\forall x\u200a\neg (x<x)$
- $\forall x\u200a\forall y\u200a(x<y\vee x=y\vee y<x)$
- $\forall x\u200a\forall y\u200a\forall z\u200a(x<y\to x+z<y+z)$
- $\forall x\u200a\forall y\u200a\forall z\u200a\left(\right(0<z\wedge x<y)\to (x\times z<y\times z\left)\right)$
- $\forall x\u200a\forall y\u200a(x<y\to \exists z\u200a(x+z=y))$
- $0<1\wedge \forall x\u200a(0<x\to (x=1\vee 1<x\left)\right)$
- $\forall x\u200a(0=x\vee 0<x)$

Most of these axioms should be familiar as axioms for an ordered ring.
The last one makes it the *nonnegative* part of such a ring, and the penultimate one
(together with properties of addition) makes it a *discretely* ordered ring.

Unless explicitly stated otherwise, all ${L}_{A}$ structures in this section of the web pages will be considered to be models of $\text{DOR}$, and all ${L}_{A}$-theories will contain the axioms of $\text{DOR}$. Therefore we can use the standard abbreviations for ${L}_{A}$ terms, such as ${x}^{2}(x+1)+xy$ for $\left(\right((x\times x)\times (x+1))+(x\times y\left)\right)$ since by commutativity and associativity the first expression is unambiguous in $\text{DOR}$.

We also use $x>y$ for $y<x$, $x\u2a7dy$ for $(x<y\vee x=y)$ and so on.

The canonical closed terms, or numerals, for natural numbers are $0$, $\left(0\mathrm{+1}\right)$, $\left(\right(0\mathrm{+1}\left)\mathrm{+1}\right)$, $\left(\right(\left(0\mathrm{+1}\right)\mathrm{+1}\left)\mathrm{+1}\right)$, and so on. We denote these $\text{cterm}\left(0\right)$, $\text{cterm}\left(1\right)$, $\text{cterm}\left(2\right)$, $\text{cterm}\left(3\right)$, etc., or just $0,1,2,3,\dots $ when no confusion arises.

Exercise.

Explain how, given a model of $\text{DOR}$, you may construct from it in a natural way a model of all axioms except the last, which is to be replaced by $\forall x\u200a\forall y\u200a\exists z\u200ax+z=y$. Thus justify calling $\text{DOR}$ the axioms for the nonnegative parts of discretely ordered rings.

The next few results show that the map $n\mapsto \text{cterm}\left(n\right)$ is an embedding
of the standard model $\mathbb{N}$ onto an initial segment of every model of $\text{DOR}$.
Many of the proofs are missing or just hinted at. They are all easy. What is
perhaps not so easy is to attempt to prove these results *in the right order*.
Without following the order given here you might find them much harder.

Theorem.

It is provable in $\text{DOR}$ that $\forall x\u200a\forall y\u200a(x<y\to (x+1)\u2a7dy)$.

Theorem.

Suppose $n,m\in \mathbb{N}$ and $n<m$. Then $\text{DOR}\u22a2\text{cterm}\left(n\right)<\text{cterm}\left(m\right)$.

**Proof.**

Induction on $m$.

Observe that $\text{DOR}\u22a2\forall x\u200a\forall y\u200a(x<y\to \neg x=y)$ because of the order axioms. Also if $n>m$ or $n=m$ then as $\text{DOR}\u22a2\text{cterm}\left(m\right)<\text{cterm}\left(n\right)$ or $\text{DOR}\u22a2\text{cterm}\left(m\right)=\text{cterm}\left(n\right)$ respectively, it is impossible that in any model of $\text{DOR}$ we also have $\text{cterm}\left(n\right)<\text{cterm}\left(m\right)$. So there is a strong converse to the above theorem: if $n,m\in \mathbb{N}$ and in some model $M\models \text{DOR}$ we have $M\models \text{cterm}\left(n\right)<\text{cterm}\left(m\right)$ then $n<m$ in the naturals too. Similarly if $M\models \text{cterm}\left(n\right)=\text{cterm}\left(m\right)$ then $n=m$ in the naturals too. Therefore the mapping $n\mapsto \text{cterm}\left(n\right)$ is a one-to-one map from $\mathbb{N}$ to our model $M$ of $\text{DOR}$ for which $n<m$ holds in $\mathbb{N}$ if and only if $M\models \text{cterm}\left(n\right)<\text{cterm}\left(m\right)$ holds in $M$.

Theorem.

Suppose $n,m,k\in \mathbb{N}$ and $n+m=k$. Then $\text{DOR}\u22a2\text{cterm}\left(n\right)+\text{cterm}\left(m\right)=\text{cterm}\left(k\right)$.

**Proof.**

Induction on $m$.

Theorem.

Suppose $n,m,k\in \mathbb{N}$ and $n\times m=k$. Then $\text{DOR}\u22a2\text{cterm}\left(n\right)\times \text{cterm}\left(m\right)=\text{cterm}\left(k\right)$.

**Proof.**

Induction on $m$, using the previous result.

Theorem.

For each $n\in \mathbb{N}$ it is provable in $\text{DOR}$ that $\forall x\u200a(x<\text{cterm}(n)\to x=\text{cterm}(0)\vee x=\text{cterm}(1)\vee \dots \vee x=\text{cterm}(n-1\left)\right)$.

**Proof.**

Induction on $n$.

Because of these results we are justified is identifying each $n\in \mathbb{N}$ with the value of the canonical term $\text{cterm}\left(n\right)$ in each model of $\text{DOR}$.

We are going to give some very important definitions, and examine some classes of sentences provable in $\text{DOR}$.

Definition.

If $t$ is a term of ${L}_{A}$ we use the abbreviation
$\forall x<t\u200a\dots $ for
$\forall x\u200a(x<t\to \dots )$. We use
$\exists x<t\u200a\dots $ for
$\exists x\u200a(x<t\wedge \dots )$. These quantifiers are said to be
*bounded*.

Definition.

A formula of ${L}_{A}$ is *bounded* or ${\Delta}_{0}$
if all quantifiers occurring in it are bounded. That is, ${\Delta}_{0}$ is
the least collection of formulas of ${L}_{A}$ containing all atomic formulas
and closed under the syntactical boolean operations of
$\wedge $, $\vee $, $\to $, $\neg $ and under bounded quantification.

We say a ${L}_{A}$ sentence is *true* if it is true in the standard model
$\mathbb{N}$.

Proposition.

Suppose $t$ is a closed term of ${L}_{A}$ with value $n\in \mathbb{N}$ in the standard model. Then $\text{DOR}\u22a2t=\text{clterm}\left(n\right)$.

**Proof.**

By induction on the term $t$ and how it is made from $+,\times ,0,1$.

Theorem.

Suppose $\sigma $ is a ${\Delta}_{0}$
*sentence*
of ${L}_{A}$, i.e. is bounded and has no free variables.
Suppose $\sigma $ is true. Then $\text{DOR}\u22a2\sigma $.

**Proof.**

Exercise. Use an induction on ${\Delta}_{0}$ sentences, showing that for every such sentence $\sigma $, either $\text{DOR}\u22a2\sigma $ or $\text{DOR}\u22a2\neg \sigma $. Then observe that, for any sentence $\tau $, by the soundness theorem if $\text{DOR}\u22a2\tau $ then $\mathbb{N}\models \tau $. The theorem follows as if $\sigma $ is true we cannot have $\mathbb{N}\models \neg \sigma $.

Definition.

A formula $\theta \left(\stackrel{\_}{x}\right)$ is ${\Sigma}_{1}$ if it is of the form $\exists {u}_{1}\u200a\exists {u}_{2}\u200a\dots \exists {u}_{n}\u200a\varphi (\stackrel{\_}{u},\stackrel{\_}{x})$ for some tuple of variables $\stackrel{\_}{u}$ and some ${\Delta}_{0}$ formula $\varphi (\stackrel{\_}{u},\stackrel{\_}{x})$. We allow the tuple $\stackrel{\_}{u}$ to be empty, so that any ${\Delta}_{0}$ formula is by definition also ${\Sigma}_{1}$.

Using this, we can extend the previous theorem slightly, though its proof is needed to get the slightly more general result.

Theorem.

Suppose $\sigma $ is a ${\Sigma}_{1}$ sentence of ${L}_{A}$ and is true. Then $\text{DOR}\u22a2\sigma $.

**Proof.**

If $\sigma $ is $\exists {u}_{1}\u200a\exists {u}_{2}\u200a\dots \exists {u}_{n}\u200a\varphi \left(\stackrel{\_}{u}\right)$ and true, let ${k}_{1},{k}_{2}\dots {k}_{n}\in \mathbb{N}$ such that $\mathbb{N}\models \varphi ({k}_{1},{k}_{2}\dots {k}_{n})$. Then (using canonical terms to represent these natural numbers) $\varphi ({k}_{1},{k}_{2}\dots {k}_{n})$ is a true ${\Delta}_{0}$ sentence hence provable in $\text{DOR}$. Hence by $$-introduction $\text{DOR}\u22a2\sigma $.

Definition.

A formula $\theta \left(\stackrel{\_}{x}\right)$ is ${\Pi}_{1}$ if it is of the form $\forall {u}_{1}\u200a\forall {u}_{2}\u200a\dots \forall {u}_{n}\u200a\varphi (\stackrel{\_}{u},\stackrel{\_}{x})$ for some tuple of variables $\stackrel{\_}{u}$ and some ${\Delta}_{0}$ formula $\varphi (\stackrel{\_}{u},\stackrel{\_}{x})$. Again, $\stackrel{\_}{u}$ may be empty, so that any ${\Delta}_{0}$ formula is by definition also ${\Pi}_{1}$.

Exercise.

Suppose $\sigma $ is a ${\Pi}_{1}$ sentence of ${L}_{A}$ and is false. Then $\sigma $ is refutable in $\text{DOR}$, i.e. $\text{DOR}\u22a2\neg \sigma $.

It turns out that there are ${\Sigma}_{1}$ sentences $\sigma $ which are neither provable in $\text{DOR}$ nor refutable in $\text{DOR}$. The existence of such sentences will follow from our proof of the Gödel incompleteness theorems.

Exercise.

Note that most of the axioms of $\text{DOR}$ are not ${\Sigma}_{1}$. Examine the arguments above and find an infinite set $R$ of sentences of ${L}_{A}$ such that: (a) $R$ is a recursive theory; (b) every sentence in $R$ is a true ${\Sigma}_{1}$ sentence; and (c) every true ${\Sigma}_{1}$ sentence is provable in $R$.