Abraham Robinson (6 October 1918 - 11 April 1974)

This paper by EDITORS, Journal of Logic & Analysis, is a reminiscence of Abraham Robinson.

We include here a formalization of the ordering of a countable nonstandard model of Th(N,<), which looks like ℕ ⊕ (ℚ × ℤ).

def N : Type

The underlying set of a countable nonstandard model of Th(N,<).

Equations

• N = (ℕ ⊕ ℚ × ℤ)

def nat_lt (n : ℕ) : N → Prop

Comparing an element of N with a standard element of N.

Equations

• nat_lt n (Sum.inl m) = (n < m)
• nat_lt n (Sum.inr val) = True

def inf_lt (q₁ : ℚ) (z₁ : ℤ) : N → Prop

Comparing an element of N with a nonstandard element of N.

Equations

• inf_lt q₁ z₁ (Sum.inl val) = False
• inf_lt q₁ z₁ (Sum.inr (q₂, z₂)) = (q₁ < q₂ ∨ q₁ = q₂ ∧ z₁ < z₂)

def lt : N → N → Prop

The ordering of a countable nonstandard model of Th(N,<).

Equations

• lt (Sum.inl val) = nat_lt val
• lt (Sum.inr (q₂, z₂)) = inf_lt q₂ z₂

theorem lt_example₁ : lt (Sum.inl 3) (Sum.inr (0, 2))

The natural number 3 is less than the infinite number (0,2).

theorem lt_example₂ : ¬lt (Sum.inr (0, 2)) (Sum.inl 3)

The natural number 3 is not greater than the infinite number (0,2).