LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted

class BASICModel (num : Type u) extends FirstOrder.Language.peano.Structure num : Type (max u u_1)

Single-sorted models of the BASIC arithmetic axioms.

• funMap {n : ℕ} : peano.Functions n → (Fin n → num) → num
• RelMap {n : ℕ} : peano.Relations n → (Fin n → num) → Prop
• B1 {x : num} : x + 1 ≠ 0
• B2 (x y : num) : x + 1 = y + 1 → x = y
• B3 (x : num) : x + 0 = x
• B4 {x y : num} : x + (y + 1) = x + y + 1
• B5 {x : num} : x * 0 = 0
• B6 {x y : num} : x * (y + 1) = x * y + x
• B7 {x y : num} : x ≤ y → y ≤ x → x = y
• B8 {x y : num} : x ≤ x + y

class BASICModelExt (num : Type u) extends BASICModel num : Type (max u u_1)

BASIC models with the additional axiom (0 : num) + 1 = 1.

• funMap {n : ℕ} : peano.Functions n → (Fin n → num) → num
• RelMap {n : ℕ} : peano.Relations n → (Fin n → num) → Prop
• B1 {x : num} : x + 1 ≠ 0
• B2 (x y : num) : x + 1 = y + 1 → x = y
• B3 (x : num) : x + 0 = x
• B4 {x y : num} : x + (y + 1) = x + y + 1
• B5 {x : num} : x * 0 = 0
• B6 {x y : num} : x * (y + 1) = x * y + x
• B7 {x y : num} : x ≤ y → y ≤ x → x = y
• B8 {x y : num} : x ≤ x + y
• C : 0 + 1 = 1

def natToM {M : Type u_1} [BASICModel M] : ℕ → M

Interpret natural-number literals in a BASIC model by iterating successor.

Equations

• natToM 0 = 0
• natToM 1 = 1
• natToM n.succ = natToM n + 1

@[implicit_reducible]

instance instOfNatLeanPool {M : Type u_1} [BASICModel M] (n : ℕ) : OfNat M n

Equations

• instOfNatLeanPool n = { ofNat := natToM n }

def pair {M : Type u_1} [BASICModel M] (x y : M) : M

Pairing function used to encode two numbers as one number.

Equations

• ⟨x,y⟩ = (x + y) * (x + y + 1) + (1 + 1) * y

def «term⟨_,_⟩» : Lean.ParserDescr

Pairing notation for two numbers.

Equations

• One or more equations did not get rendered due to their size.

def «term⟨_,_,_⟩» : Lean.ParserDescr

Pairing notation for three numbers.

Equations

• One or more equations did not get rendered due to their size.

theorem BASICModel.le_refl {M : Type u} [iopen : BASICModel M] (a : M) : a ≤ a

theorem BASICModel.zero_ne_add_one {M : Type u} [iopen : BASICModel M] (x : M) : x + 1 ≠ 0

theorem BASICModel.one_add_right_regular {M : Type u} [iopen : BASICModel M] : IsAddRightRegular 1