Exercises on discretely ordered rings

Define the canonical term for a natural number $n \in ℕ$ by $cterm (0) = 0$ and for $n ⩾ 0$ , $cterm (n +1) = (cterm (n) + 1)$ .

Exercise 1.

Show that for $n, m, k \in ℕ$ with $n \times m = k$ we have $DOR ⊢ (cterm (n) \times cterm (m)) = cterm (k)$ . Be careful to state any induction hypothesis carefully.

An atomic $L_{A}$ formula is one of the form $t = s$ or $t < s$ , where $t, s$ are terms. A negated atomic $L_{A}$ formula is one of the form $\neg σ$ where $σ$ is atomic.

Exercise 2.

Given that $DOR ⊢ σ$ or $DOR ⊢ \neg σ$ for every atomic $L_{A}$ sentence $σ$ , show that $DOR$ proves all true $Δ_{0}$ sentences.

We write $⟨ u, v ⟩ = w$ for the $L_{A}$ -formula $(u + v) (u + v + 1) + 2 u = 2 w$ . It is not true that $DOR ⊢ \forall w \exists u, v ⟨ u, v ⟩ = w$ , but $DOR + DIV2 + SQRT ⊢ \forall w \exists u, v ⟨ u, v ⟩ = w$ where $DIV2$ is the statement $\forall x \exists y (2 y = x \lor 2 y + 1 = x)$ . and $SQRT$ is the statement $\forall x \exists y (y^{2} ⩽ x \land x < (y + 1)^{2})$ . The injective property of the pairing function is, however, provable in $DOR$ .

Exercise 3.

$DOR ⊢ \forall x, y, u, v ((u + x = v \land u + y = v) \to x = y)$ and $DOR ⊢ \forall u, v \neg (2 u = 2 v + 1)$ . Prove these!

Exercise 4.

Prove in $DOR$ that $\forall u, v, u', v', w (⟨ u, v ⟩ = w \land ⟨ u', v' ⟩ = w \to u = u' \land v = v')$ .

Exercise 5.

Prove $DOR + DIV2 + SQRT ⊢ \forall w \exists u, v ⟨ u, v ⟩ = w$ .

(Hint: Given $w \in M$ , a model of the theory above, first show that there is $r \in M$ such that $r (r +1) ≤ 2 w < (r +1) (r +2)$ ; then find $u$ such that $r (r +1) + 2 u = 2 w$ .)

A formula $ϕ (x_{1}, \dots, x_{m})$ of $L_{A}$ is existential if it is of the form $\exists u_{1} \dots \exists u_{m} θ (u_{1}, \dots u_{n}, x_{1}, \dots, x_{m})$ where $θ (u_{1}, \dots u_{n}, x_{1}, \dots, x_{m})$ is quantifier-free.

Exercise 6.

Prove that every existential formula $ϕ (x_{1}, \dots, x_{m})$ of $L_{A}$ is provably equivalent in $DOR$ to one of the form

\exists v_{1} \dots \exists v_{k} t (v_{1}, \dots, v_{k}, x_{1}, \dots, x_{m}) = s (v_{1}, \dots, v_{k}, x_{1}, \dots, x_{m})

where $t, s$ are terms in the language $L_{A}$ . (Use an induction on the different ways of building a quantifier-free formula $θ$ from atomic and negated atomic ones.)