Discretely ordered rings

1. Introduction

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 $DOR$ because it has a clear algebraic meaning. This page introduces the reader to $DOR$ .

2. First order logic

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 $Σ ⊢ σ$ to say that from additional non-logical axioms $Σ$ the system can derive $σ$ , i.e. there is a formal proof of $σ$ in the system with additional non-logical axioms $Σ$ . 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 $Σ ⊢ σ$ is equivalent to a related notion, $Σ ⊨ σ$ , and we can use this instead. $Σ ⊨ σ$ means that every structure (an algebraic object like a group or a ring) that makes $Σ$ true must make $σ$ true.

The implication $Σ ⊢ σ$ implies $Σ ⊨ σ$ is called the Soundness Theorem, as it says the system $⊢$ is sound, or correct, and the implication $Σ ⊨ σ$ implies $Σ ⊢ σ$ is known as the Completeness Theorem as it says that $⊢$ 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 $⊨$ throughout, and appeal to Soundness and Completeness to see that what we said about $⊨$ applies equally well to $⊢$ . 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.

3. The language and axioms for discretely ordered rings

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 $ℕ$ in the usual way. The $L_{A}$ structure $ℕ$ , or more properly $(ℕ, 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 (x) = x +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 ${DOR}^{⩾ 0} (L_{A})$ 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 ${DOR}^{⩾ 0}$ or just $DOR$ . The same theory is often called ${PA}^{-}$ .

Definition.

$\forall x \forall y \forall z ((x + y) + z = x + (y + z))$
$\forall x \forall y (x + y = y + x)$
$\forall x \forall y \forall z ((x \times y) \times z = x \times (y \times z))$
$\forall x \forall y (x \times y = y \times x)$
$\forall x \forall y \forall z (x \times (y + z) = (x \times y) + (x \times z))$
$\forall x ((x + 0 = x) \land (x \times 0 = 0))$
$\forall x (x \times 1 = x)$
$\forall x \forall y \forall z ((x < y \land y < z) \to x < z)$
$\forall x \neg (x < x)$
$\forall x \forall y (x < y \lor x = y \lor y < x)$
$\forall x \forall y \forall z (x < y \to x + z < y + z)$
$\forall x \forall y \forall z ((0 < z \land x < y) \to (x \times z < y \times z))$
$\forall x \forall y (x < y \to \exists z (x + z = y))$
$0 < 1 \land \forall x (0 < x \to (x = 1 \lor 1 < x))$
$\forall x (0 = x \lor 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 $DOR$ , and all $L_{A}$ -theories will contain the axioms of $DOR$ . Therefore we can use the standard abbreviations for $L_{A}$ terms, such as $x^{2} (x + 1) + x y$ for $(((x \times x) \times (x + 1)) + (x \times y))$ since by commutativity and associativity the first expression is unambiguous in $DOR$ .

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

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

Exercise.

Explain how, given a model of $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 \forall y \exists z x + z = y$ . Thus justify calling $DOR$ the axioms for the nonnegative parts of discretely ordered rings.

The next few results show that the map $n \mapsto cterm (n)$ is an embedding of the standard model $ℕ$ onto an initial segment of every model of $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 $DOR$ that $\forall x \forall y (x < y \to (x + 1) ⩽ y)$ .

Theorem.

Suppose $n, m \in ℕ$ and $n < m$ . Then $DOR ⊢ cterm (n) < cterm (m)$ .

Proof.

Induction on $m$ .

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

Theorem.

Suppose $n, m, k \in ℕ$ and $n + m = k$ . Then $DOR ⊢ cterm (n) + cterm (m) = cterm (k)$ .

Proof.

Induction on $m$ .

Theorem.

Suppose $n, m, k \in ℕ$ and $n \times m = k$ . Then $DOR ⊢ cterm (n) \times cterm (m) = cterm (k)$ .

Proof.

Induction on $m$ , using the previous result.

Theorem.

For each $n \in ℕ$ it is provable in $DOR$ that $\forall x (x < cterm (n) \to x = cterm (0) \lor x = cterm (1) \lor \dots \lor x = cterm (n - 1))$ .

Proof.

Induction on $n$ .

Because of these results we are justified is identifying each $n \in ℕ$ with the value of the canonical term $cterm (n)$ in each model of $DOR$ .

4. Provability in DOR

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

Definition.

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

Definition.

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

We say a $L_{A}$ sentence is true if it is true in the standard model $ℕ$ .

Proposition.

Suppose $t$ is a closed term of $L_{A}$ with value $n \in ℕ$ in the standard model. Then $DOR ⊢ t = clterm (n)$ .

Proof.

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

Theorem.

Suppose $σ$ is a $Δ_{0}$ sentence of $L_{A}$ , i.e. is bounded and has no free variables. Suppose $σ$ is true. Then $DOR ⊢ σ$ .

Proof.

Exercise. Use an induction on $Δ_{0}$ sentences, showing that for every such sentence $σ$ , either $DOR ⊢ σ$ or $DOR ⊢ \neg σ$ . Then observe that, for any sentence $τ$ , by the soundness theorem if $DOR ⊢ τ$ then $ℕ ⊨ τ$ . The theorem follows as if $σ$ is true we cannot have $ℕ ⊨ \neg σ$ .

Definition.

A formula $θ (\overline{x})$ is $Σ_{1}$ if it is of the form $\exists u_{1} \exists u_{2} \dots \exists u_{n} ϕ (\overline{u}, \overline{x})$ for some tuple of variables $\overline{u}$ and some $Δ_{0}$ formula $ϕ (\overline{u}, \overline{x})$ . We allow the tuple $\overline{u}$ to be empty, so that any $Δ_{0}$ formula is by definition also $Σ_{1}$ .

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

Theorem.

Suppose $σ$ is a $Σ_{1}$ sentence of $L_{A}$ and is true. Then $DOR ⊢ σ$ .

Proof.

If $σ$ is $\exists u_{1} \exists u_{2} \dots \exists u_{n} ϕ (\overline{u})$ and true, let $k_{1}, k_{2} \dots k_{n} \in ℕ$ such that $ℕ ⊨ ϕ (k_{1}, k_{2} \dots k_{n})$ . Then (using canonical terms to represent these natural numbers) $ϕ (k_{1}, k_{2} \dots k_{n})$ is a true $Δ_{0}$ sentence hence provable in $DOR$ . Hence by -introduction $DOR ⊢ σ$ .

Definition.

A formula $θ (\overline{x})$ is $Π_{1}$ if it is of the form $\forall u_{1} \forall u_{2} \dots \forall u_{n} ϕ (\overline{u}, \overline{x})$ for some tuple of variables $\overline{u}$ and some $Δ_{0}$ formula $ϕ (\overline{u}, \overline{x})$ . Again, $\overline{u}$ may be empty, so that any $Δ_{0}$ formula is by definition also $Π_{1}$ .

Exercise.

Suppose $σ$ is a $Π_{1}$ sentence of $L_{A}$ and is false. Then $σ$ is refutable in $DOR$ , i.e. $DOR ⊢ \neg σ$ .

It turns out that there are $Σ_{1}$ sentences $σ$ which are neither provable in $DOR$ nor refutable in $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 $DOR$ are not $Σ_{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 $Σ_{1}$ sentence; and (c) every true $Σ_{1}$ sentence is provable in $R$ .