Exercises on discretely ordered rings

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

Exercise 1.

Show that for $n , m , k ∈ ℕ$ with $n × m = k$ we have $DOR ⊢ ( cterm ( n ) × 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 $¬ σ$ where $σ$ is atomic.

Exercise 2.

Given that $DOR ⊢ σ$ or $DOR ⊢ ¬ σ$ 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 ⊢ ∀ w ∃ u , v ⟨ u , v ⟩ = w$, but $DOR + DIV2 + SQRT ⊢ ∀ w ∃ u , v ⟨ u , v ⟩ = w$ where $DIV2$ is the statement $∀ x ∃ y ( 2 y = x ∨ 2 y + 1 = x )$. and $SQRT$ is the statement $∀ x ∃ y ( y 2 ⩽ x ∧ x < ( y + 1 ) 2 )$. The injective property of the pairing function is, however, provable in $DOR$.

Exercise 3.

$DOR ⊢ ∀ x , y , u , v ( ( u + x = v ∧ u + y = v ) → x = y )$ and $DOR ⊢ ∀ u , v ¬ ( 2 u = 2 v + 1 )$. Prove these!

Exercise 4.

Prove in $DOR$ that $∀ u , v , u ′ , v ′ , w ⟨ u , v ⟩ = w ∧ ⟨ u ′ , v ′ ⟩ = w → u = u ′ ∧ v = v ′$.

Exercise 5.

Prove $DOR + DIV2 + SQRT ⊢ ∀ w ∃ u , v ⟨ u , v ⟩ = w$.

(Hint: Given $w ∈ M$, a model of the theory above, first show that there is $r ∈ 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 , … , x m )$ of $L A$ is existential if it is of the form $∃ u 1 … ∃ u m θ ( u 1 , … u n , x 1 , … , x m )$ where $θ ( u 1 , … u n , x 1 , … , x m )$ is quantifier-free.

Exercise 6.

Prove that every existential formula $ϕ ( x 1 , … , x m )$ of $L A$ is provably equivalent in $DOR$ to one of the form

$∃ v 1 … ∃ v k t ( v 1 , … , v k , x 1 , … , x m ) = s ( v 1 , … , v k , x 1 , … , 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.)