LeanPool.FormalizationOfBoundedArithmetic.IDelta0 #

source

class IDelta0Model (num : Type u_1) extends IOPENModel num :

Type (max u_1 u_2)

Models of open induction extended with induction for delta-zero formulas.

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
open_induction {n : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n ⊕ a) 0) : phi.IsOpen → num ⊨ mkInductionSentence phi
delta0_induction {n1 : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n1 ⊕ a) 0) : phi.IsDelta0 → num ⊨ mkInductionSentence phi

Instances

source

theorem IDelta0Model.pred_exists {M : Type u_1} [idelta0 : IDelta0Model M] {x : M} :

x ≠ 0 → ∃ y ≤ x, x = y + 1

source

theorem IDelta0Model.ex_of_bdEx {a : Type u_2} [LE a] {t : a} {P : a → Prop} :

(∃ x ≤ t, P x) → ∃ (x : a), P x

source

theorem IDelta0Model.zero_add {M : Type u_1} [idelta0 : IDelta0Model M] (x : M) :

0 + x = x

source

@[implicit_reducible]

instance IDelta0Model.instAddZeroClass {M : Type u_1} [idelta0 : IDelta0Model M] :

AddZeroClass M

Equations

IDelta0Model.instAddZeroClass = { toZero := FirstOrder.Language.peano.instZeroOfStructure, toAdd := FirstOrder.Language.peano.instAddOfStructure, zero_add := ⋯, add_zero := ⋯ }

source

theorem IDelta0Model.add_diff_exists {M : Type u_1} [idelta0 : IDelta0Model M] (x y : M) :

∃ (z : M), x + z = y ∨ y + z = x

source

theorem IDelta0Model.le_iff_exists_add {M : Type u_1} [idelta0 : IDelta0Model M] (x y : M) :

x ≤ y ↔ ∃ (z : M), x + z = y

source

theorem IDelta0Model.le_trans {M : Type u_1} [idelta0 : IDelta0Model M] {x y z : M} :

x ≤ y → y ≤ z → x ≤ z

source

@[implicit_reducible]

instance IDelta0Model.instPreorder {M : Type u_1} [idelta0 : IDelta0Model M] :

Preorder M

Equations

IDelta0Model.instPreorder = { toLE := FirstOrder.Language.peano.instLEOfStructure, toLT := FirstOrder.Language.peano.instLTOfStructure, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

source

theorem IDelta0Model.le_total {M : Type u_1} [idelta0 : IDelta0Model M] (x y : M) :

x ≤ y ∨ y ≤ x

source

theorem IDelta0Model.add_rotate {M : Type u_1} [idelta0 : IDelta0Model M] {a b c : M} :

a + b + c = b + c + a

source

theorem IDelta0Model.add_le_add_right {M : Type u_1} [idelta0 : IDelta0Model M] {x y z : M} :

x ≤ y ↔ x + z ≤ y + z

source

theorem IDelta0Model.le_cancel_left {M : Type u_1} [idelta0 : IDelta0Model M] {x y z : M} :

x ≤ y → z + x ≤ z + y

source

theorem IDelta0Model.le_mul_right {M : Type u_1} [idelta0 : IDelta0Model M] {x y z : M} :

x ≤ y → x * z ≤ y * z

source

theorem IDelta0Model.le_succ_iff {M : Type u_1} [idelta0 : IDelta0Model M] {x y : M} :

x ≤ y + 1 ↔ x ≤ y ∨ x = y + 1

source

@[implicit_reducible]

instance IDelta0Model.instPartialOrder {M : Type u_1} [idelta0 : IDelta0Model M] :

PartialOrder M

Equations

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

source

instance IDelta0Model.instCanonicallyOrderedAdd {M : Type u_1} [idelta0 : IDelta0Model M] :

CanonicallyOrderedAdd M

source

@[implicit_reducible]

noncomputable instance IDelta0Model.instLinearOrder {M : Type u_1} [idelta0 : IDelta0Model M] :

LinearOrder M

Equations

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

source

theorem IDelta0Model.le_of_eq {M : Type u_1} [idelta0 : IDelta0Model M] {x y : M} :

x = y → x ≤ y

source

theorem IDelta0Model.zero_if_sum_zero {M : Type u_1} [idelta0 : IDelta0Model M] {x y : M} :

x + y = 0 → x = 0 ∧ y = 0

source

theorem IDelta0Model.lt_one_eq_zero {M : Type u_1} [idelta0 : IDelta0Model M] {x : M} :

x < 1 → x = 0

source

theorem IDelta0Model.lt_iff_succ_le {M : Type u_1} [idelta0 : IDelta0Model M] {x y : M} :

x < y ↔ x + 1 ≤ y

source

theorem IDelta0Model.mul_eq_zero_iff_left {M : Type u_1} [idelta0 : IDelta0Model M] {x y : M} :

x ≠ 0 → (x * y = 0 ↔ y = 0)

source

theorem IDelta0Model.mul_cancel_right {M : Type u_1} [idelta0 : IDelta0Model M] (x y z : M) :

x * z = y * z ∧ z ≠ 0 → x = y