Typed Formalized Semiformula/Formula #

theorem LO.Arith.sub_succ_lt_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a b : V} (h : b < a) :

a - (b + 1) < a

theorem LO.Arith.sub_succ_lt_selfs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a b : V} (h : b < a) :

a - (a - (b + 1) + 1) = b

structure LO.Arith.Language.Semiformula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :

Type u_1

val : V
prop : L.IsSemiformula n self.val

Instances For

LO.FirstOrder.Semiformula.goedelQuoteSyntacticSemiformulaToCodedSemiformula

source

@[reducible, inline]

abbrev LO.Arith.Language.Formula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :

Type u_1

Equations

L.Formula = L.Semiformula 0

Instances For

source

@[simp]

theorem LO.Arith.Language.Semiformula.isUFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) :

L.IsUFormula p.val

source

def LO.Arith.instLogicalConnectiveSemiformula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

LogicalConnective (L.Semiformula n)

Equations

LO.Arith.instLogicalConnectiveSemiformula = LO.LogicalConnective.mk

source

def LO.Arith.Language.Semiformula.cast {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n n' : V} (p : L.Semiformula n) (eq : n = n' := by simp) :

L.Semiformula n'

Equations

p.cast eq = eq ▸ p

source

def LO.Arith.verums {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (k : V) :

L.Semiformula n

Equations

LO.Arith.verums k = { val := LO.Arith.qqVerums k, prop := ⋯ }

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_cast {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n n' : V} (p : L.Semiformula n) (eq : n = n') :

(p.cast eq).val = p.val

source

def LO.Arith.Language.Semiformula.all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

L.Semiformula n

Equations

p.all = { val := LO.Arith.qqAll p.val, prop := ⋯ }

source

def LO.Arith.Language.Semiformula.ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

L.Semiformula n

Equations

p.ex = { val := LO.Arith.qqEx p.val, prop := ⋯ }

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

⊤.val = qqVerum

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

⊥.val = qqFalsum

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ⋏ q).val = qqAnd p.val q.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ⋎ q).val = qqOr p.val q.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_neg {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) :

(∼p).val = L.neg p.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_imp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ➝ q).val = p.val ^→[L] q.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

p.all.val = qqAll p.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

p.ex.val = qqEx p.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ⭤ q).val = L.iff p.val q.val

source

theorem LO.Arith.Language.Semiformula.val_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p q : L.Semiformula n} :

p.val = q.val ↔ p = q

source

theorem LO.Arith.Language.Semiformula.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p q : L.Semiformula n} (h : p.val = q.val) :

p = q

source

@[simp]

theorem LO.Arith.Language.Semiformula.and_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p₁ p₂ q₁ q₂ : L.Semiformula n} :

p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

source

@[simp]

theorem LO.Arith.Language.Semiformula.or_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p₁ p₂ q₁ q₂ : L.Semiformula n} :

p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

source

@[simp]

theorem LO.Arith.Language.Semiformula.all_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p q : L.Semiformula (n + 1)} :

p.all = q.all ↔ p = q

source

@[simp]

theorem LO.Arith.Language.Semiformula.ex_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p q : L.Semiformula (n + 1)} :

p.ex = q.ex ↔ p = q

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_verums {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k : V} :

(verums k).val = qqVerums k

source

@[simp]

theorem LO.Arith.Language.Semiformula.verums_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

verums 0 = ⊤

source

@[simp]

theorem LO.Arith.Language.Semiformula.verums_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (k : V) :

verums (k + 1) = ⊤ ⋏ verums k

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

∼⊤ = ⊥

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

∼⊥ = ⊤

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

∼(p ⋏ q) = ∼p ⋎ ∼q

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

∼(p ⋎ q) = ∼p ⋏ ∼q

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

∼p.all = (∼p).ex

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

∼p.ex = (∼p).all

source

theorem LO.Arith.Language.Semiformula.imp_def {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

p ➝ q = ∼p ⋎ q

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_neg {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) :

∼∼p = p

source

def LO.Arith.Language.Semiformula.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) :

L.Semiformula n

Equations

p.shift = { val := L.shift p.val, prop := ⋯ }

source

def LO.Arith.Language.Semiformula.substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (p : L.Semiformula n) (w : L.SemitermVec n m) :

L.Semiformula m

Equations

p^/[w] = { val := L.substs w.val p.val, prop := ⋯ }

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) :

p.shift.val = L.shift p.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.val_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (p : L.Semiformula n) (w : L.SemitermVec n m) :

p^/[w].val = L.substs w.val p.val

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

⊤.shift = ⊤

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} :

⊥.shift = ⊥

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ⋏ q).shift = p.shift ⋏ q.shift

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ⋎ q).shift = p.shift ⋎ q.shift

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

p.all.shift = p.shift.all

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula (n + 1)) :

p.ex.shift = p.shift.ex

source

@[simp]

theorem LO.Arith.Language.Semiformula.neg_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p q : L.Semiformula n} :

∼p = ∼q ↔ p = q

source

@[simp]

theorem LO.Arith.Language.Semiformula.imp_inj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p₁ p₂ q₁ q₂ : L.Semiformula n} :

p₁ ➝ p₂ = q₁ ➝ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_neg {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p : L.Semiformula n) :

(∼p).shift = ∼p.shift

source

@[simp]

theorem LO.Arith.Language.Semiformula.shift_imp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (p q : L.Semiformula n) :

(p ➝ q).shift = p.shift ➝ q.shift

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) :

⊤^/[w] = ⊤

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_falsum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) :

⊥^/[w] = ⊥

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p q : L.Semiformula n) :

(p ⋏ q)^/[w] = p^/[w] ⋏ q^/[w]

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p q : L.Semiformula n) :

(p ⋎ q)^/[w] = p^/[w] ⋎ q^/[w]

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p : L.Semiformula (n + 1)) :

p.all^/[w] = p^/[w.q].all

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p : L.Semiformula (n + 1)) :

p.ex^/[w] = p^/[w.q].ex

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_neg {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) :

(∼p)^/[w] = ∼p^/[w]

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_imp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p q : L.Semiformula n) :

(p ➝ q)^/[w] = p^/[w] ➝ q^/[w]

source

@[simp]

theorem LO.Arith.Language.Semiformula.substs_imply {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p q : L.Semiformula n) :

(p ⭤ q)^/[w] = p^/[w] ⭤ q^/[w]

source

def LO.Arith.«term_^/[_]» :

Lean.TrailingParserDescr

Equations

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

source

structure LO.Arith.Language.SemiformulaVec {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n : V) :

Type u_1

val : V
prop (i : V) : i < len self.val → L.IsSemiformula n (Arith.nth self.val i)

source

def LO.Arith.Language.SemiformulaVec.conj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : SemiformulaVec n) :

L.Semiformula n

Equations

ps.conj = { val := LO.Arith.qqConj ps.val, prop := ⋯ }

source

def LO.Arith.Language.SemiformulaVec.disj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : SemiformulaVec n) :

L.Semiformula n

Equations

ps.disj = { val := LO.Arith.qqDisj ps.val, prop := ⋯ }

source

def LO.Arith.Language.SemiformulaVec.nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : SemiformulaVec n) (i : V) (hi : i < len ps.val) :

L.Semiformula n

Equations

ps.nth i hi = { val := LO.Arith.nth ps.val i, prop := ⋯ }

source

@[simp]

theorem LO.Arith.Language.SemiformulaVec.val_conj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : SemiformulaVec n) :

ps.conj.val = qqConj ps.val

source

@[simp]

theorem LO.Arith.Language.SemiformulaVec.val_disj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : SemiformulaVec n) :

ps.disj.val = qqDisj ps.val

source

@[simp]

theorem LO.Arith.Language.SemiformulaVec.val_nth {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (ps : SemiformulaVec n) (i : V) (hi : i < len ps.val) :

(ps.nth i hi).val = Arith.nth ps.val i

source

theorem LO.Arith.Language.TSemifromula.subst_eq_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (w : L.SemitermVec n n) (p : L.Semiformula n) (H : ∀ (i : V) (hi : i < n), w.nth i hi = L.bvar i hi) :

p^/[w] = p

source

@[simp]

theorem LO.Arith.Language.TSemifromula.subst_eq_self₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) :

p^/[(L.bvar 0 ⋯).sing] = p

source

@[simp]

theorem LO.Arith.Language.TSemifromula.subst_nil_eq_self {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : L.Semiformula 0} (w : L.SemitermVec 0 0) :

p^/[w] = p

source

theorem LO.Arith.Language.TSemifromula.shift_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m : V} (w : L.SemitermVec n m) (p : L.Semiformula n) :

p^/[w].shift = p.shift^/[w.shift]

source

theorem LO.Arith.Language.TSemifromula.substs_substs {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n m l : V} (v : L.SemitermVec m l) (w : L.SemitermVec n m) (p : L.Semiformula n) :

(p^/[w])^/[v] = p^/[w.substs v]

source

def LO.Arith.Language.Semiterm.equals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

⌜ℒₒᵣ⌝.Semiformula n

Equations

t.equals u = { val := t.val ^= u.val, prop := ⋯ }

source

def LO.Arith.Language.Semiterm.notEquals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

⌜ℒₒᵣ⌝.Semiformula n

Equations

t.notEquals u = { val := t.val ^≠ u.val, prop := ⋯ }

source

def LO.Arith.Language.Semiterm.lessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

⌜ℒₒᵣ⌝.Semiformula n

Equations

t.lessThan u = { val := t.val ^< u.val, prop := ⋯ }

source

def LO.Arith.Language.Semiterm.notLessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

⌜ℒₒᵣ⌝.Semiformula n

Equations

t.notLessThan u = { val := t.val ^≮ u.val, prop := ⋯ }

source

def LO.Arith.«term_='_» :

Lean.TrailingParserDescr

Equations

LO.Arith.«term_='_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_='_» 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =' ") (Lean.ParserDescr.cat `term 76))

source

def LO.Arith.«term_≠'_» :

Lean.TrailingParserDescr

Equations

LO.Arith.«term_≠'_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_≠'_» 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≠' ") (Lean.ParserDescr.cat `term 76))

source

def LO.Arith.«term_<'_» :

Lean.TrailingParserDescr

Equations

LO.Arith.«term_<'_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_<'_» 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <' ") (Lean.ParserDescr.cat `term 76))

source

def LO.Arith.«term_≮'_» :

Lean.TrailingParserDescr

Equations

LO.Arith.«term_≮'_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_≮'_» 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≮' ") (Lean.ParserDescr.cat `term 76))

source

def LO.Arith.Language.Semiformula.ball {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

⌜ℒₒᵣ⌝.Semiformula n

Equations

LO.Arith.Language.Semiformula.ball t p = ((⌜ℒₒᵣ⌝.bvar 0 ⋯).notLessThan t.bShift ⋎ p).all

source

def LO.Arith.Language.Semiformula.bex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

⌜ℒₒᵣ⌝.Semiformula n

Equations

LO.Arith.Language.Semiformula.bex t p = ((⌜ℒₒᵣ⌝.bvar 0 ⋯).lessThan t.bShift ⋏ p).ex

source

@[simp]

theorem LO.Arith.Formalized.val_equals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

(t.equals u).val = t.val ^= u.val

source

@[simp]

theorem LO.Arith.Formalized.val_notEquals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

(t.notEquals u).val = t.val ^≠ u.val

source

@[simp]

theorem LO.Arith.Formalized.val_lessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

(t.lessThan u).val = t.val ^< u.val

source

@[simp]

theorem LO.Arith.Formalized.val_notLessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t u : ⌜ℒₒᵣ⌝.Semiterm n) :

(t.notLessThan u).val = t.val ^≮ u.val

source

@[simp]

theorem LO.Arith.Formalized.equals_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :

t₁.equals u₁ = t₂.equals u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

source

@[simp]

theorem LO.Arith.Formalized.notequals_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :

t₁.notEquals u₁ = t₂.notEquals u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

source

@[simp]

theorem LO.Arith.Formalized.lessThan_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :

t₁.lessThan u₁ = t₂.lessThan u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

source

@[simp]

theorem LO.Arith.Formalized.notLessThan_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} {t₁ t₂ u₁ u₂ : ⌜ℒₒᵣ⌝.Semiterm n} :

t₁.notLessThan u₁ = t₂.notLessThan u₂ ↔ t₁ = t₂ ∧ u₁ = u₂

source

@[simp]

theorem LO.Arith.Formalized.neg_equals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

∼t₁.equals t₂ = t₁.notEquals t₂

source

@[simp]

theorem LO.Arith.Formalized.neg_notEquals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

∼t₁.notEquals t₂ = t₁.equals t₂

source

@[simp]

theorem LO.Arith.Formalized.neg_lessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

∼t₁.lessThan t₂ = t₁.notLessThan t₂

source

@[simp]

theorem LO.Arith.Formalized.neg_notLessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

∼t₁.notLessThan t₂ = t₁.lessThan t₂

source

@[simp]

theorem LO.Arith.Formalized.shift_equals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.equals t₂).shift = t₁.shift.equals t₂.shift

source

@[simp]

theorem LO.Arith.Formalized.shift_notEquals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.notEquals t₂).shift = t₁.shift.notEquals t₂.shift

source

@[simp]

theorem LO.Arith.Formalized.shift_lessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.lessThan t₂).shift = t₁.shift.lessThan t₂.shift

source

@[simp]

theorem LO.Arith.Formalized.shift_notLessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.notLessThan t₂).shift = t₁.shift.notLessThan t₂.shift

source

@[simp]

theorem LO.Arith.Formalized.substs_equals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.equals t₂)^/[w] = t₁^ᵗ/[w].equals (t₂^ᵗ/[w])

source

@[simp]

theorem LO.Arith.Formalized.substs_notEquals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.notEquals t₂)^/[w] = t₁^ᵗ/[w].notEquals (t₂^ᵗ/[w])

source

@[simp]

theorem LO.Arith.Formalized.substs_lessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.lessThan t₂)^/[w] = t₁^ᵗ/[w].lessThan (t₂^ᵗ/[w])

source

@[simp]

theorem LO.Arith.Formalized.substs_notLessThan {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t₁ t₂ : ⌜ℒₒᵣ⌝.Semiterm n) :

(t₁.notLessThan t₂)^/[w] = t₁^ᵗ/[w].notLessThan (t₂^ᵗ/[w])

source

@[simp]

theorem LO.Arith.Formalized.val_ball {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

(Language.Semiformula.ball t p).val = qqAll (qqOr (qqBvar 0 ^≮ ⌜ℒₒᵣ⌝.termBShift t.val) p.val)

source

@[simp]

theorem LO.Arith.Formalized.val_bex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

(Language.Semiformula.bex t p).val = qqEx (qqAnd (qqBvar 0 ^< ⌜ℒₒᵣ⌝.termBShift t.val) p.val)

source

theorem LO.Arith.Formalized.neg_ball {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

∼Language.Semiformula.ball t p = Language.Semiformula.bex t (∼p)

source

theorem LO.Arith.Formalized.neg_bex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

∼Language.Semiformula.bex t p = Language.Semiformula.ball t (∼p)

source

@[simp]

theorem LO.Arith.Formalized.shifts_ball {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

(Language.Semiformula.ball t p).shift = Language.Semiformula.ball t.shift p.shift

source

@[simp]

theorem LO.Arith.Formalized.shifts_bex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

(Language.Semiformula.bex t p).shift = Language.Semiformula.bex t.shift p.shift

source

@[simp]

theorem LO.Arith.Formalized.substs_ball {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

(Language.Semiformula.ball t p)^/[w] = Language.Semiformula.ball (t^ᵗ/[w]) (p^/[w.q])

source

@[simp]

theorem LO.Arith.Formalized.substs_bex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

(Language.Semiformula.bex t p)^/[w] = Language.Semiformula.bex (t^ᵗ/[w]) (p^/[w.q])

source

def LO.Arith.Formalized.tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

Language.SemiformulaVec m

Equations

LO.Arith.Formalized.tSubstItr w p k = { val := LO.Arith.Formalized.substItr w.val p.val k, prop := ⋯ }

source

@[simp]

theorem LO.Arith.Formalized.val_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

(tSubstItr w p k).val = substItr w.val p.val k

source

@[simp]

theorem LO.Arith.Formalized.len_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

len (tSubstItr w p k).val = k

source

theorem LO.Arith.Formalized.nth_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) {i : V} (hi : i < k) :

(tSubstItr w p k).nth i ⋯ = p^/[(typedNumeral m (k - (i + 1))).cons w]

source

theorem LO.Arith.Formalized.nth_tSubstItr' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) {i : V} (hi : i < k) :

(tSubstItr w p k).nth (k - (i + 1)) ⋯ = p^/[(typedNumeral m i).cons w]

source

@[simp]

theorem LO.Arith.Formalized.neg_conj_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

∼(tSubstItr w p k).conj = (tSubstItr w (∼p) k).disj

source

@[simp]

theorem LO.Arith.Formalized.neg_disj_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

∼(tSubstItr w p k).disj = (tSubstItr w (∼p) k).conj

source

@[simp]

theorem LO.Arith.Formalized.substs_conj_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m l : V} (v : ⌜ℒₒᵣ⌝.SemitermVec m l) (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

(tSubstItr w p k).conj^/[v] = (tSubstItr (w.substs v) p k).conj

source

@[simp]

theorem LO.Arith.Formalized.substs_disj_tSubstItr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m l : V} (v : ⌜ℒₒᵣ⌝.SemitermVec m l) (w : ⌜ℒₒᵣ⌝.SemitermVec n m) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) (k : V) :

(tSubstItr w p k).disj^/[v] = (tSubstItr (w.substs v) p k).disj

source

theorem LO.Arith.Language.Semiformula.ball_eq_imp {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n : V} (t : ⌜ℒₒᵣ⌝.Semiterm n) (p : ⌜ℒₒᵣ⌝.Semiformula (n + 1)) :

ball t p = ((⌜ℒₒᵣ⌝.bvar 0 ⋯).lessThan t.bShift ➝ p).all

Documentation

Arithmetization.ISigmaOne.Metamath.Formula.Typed

Typed Formalized Semiformula/Formula #