Formulas of first-order logic

This file defines the formulas of first-order Foundation.

p : Semiformula L ξ n is a (semi-)formula of language L with bounded variables of Fin n and free variables of ξ. The quantification is represented by de Bruijn index.

inductive LO.FirstOrder.Semiformula (L : LO.FirstOrder.Language) (ξ : Type u_1) : ℕ → Type (max u_1 u_2)

• verum: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n
• falsum: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n
• rel: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n arity : ℕ} → L.Rel arity → (Fin arity → LO.FirstOrder.Semiterm L ξ n) → LO.FirstOrder.Semiformula L ξ n
• nrel: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n arity : ℕ} → L.Rel arity → (Fin arity → LO.FirstOrder.Semiterm L ξ n) → LO.FirstOrder.Semiformula L ξ n
• and: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n
• or: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n
• all: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ (n + 1) → LO.FirstOrder.Semiformula L ξ n
• ex: {L : LO.FirstOrder.Language} → {ξ : Type u_1} → {n : ℕ} → LO.FirstOrder.Semiformula L ξ (n + 1) → LO.FirstOrder.Semiformula L ξ n

@[reducible, inline]

abbrev LO.FirstOrder.Formula (L : LO.FirstOrder.Language) (ξ : Type u_1) : Type (max u_1 u_2)

Equations

• LO.FirstOrder.Formula L ξ = LO.FirstOrder.Semiformula L ξ 0

@[reducible, inline]

abbrev LO.FirstOrder.Sentence (L : LO.FirstOrder.Language) : Type u_1

Equations

• LO.FirstOrder.Sentence L = LO.FirstOrder.Formula L Empty

@[reducible, inline]

abbrev LO.FirstOrder.Semisentence (L : LO.FirstOrder.Language) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.Semisentence L n = LO.FirstOrder.Semiformula L Empty n

@[reducible, inline]

abbrev LO.FirstOrder.SyntacticSemiformula (L : LO.FirstOrder.Language) (n : ℕ) : Type u_1

Equations

• LO.FirstOrder.SyntacticSemiformula L n = LO.FirstOrder.Semiformula L ℕ n

@[reducible, inline]

abbrev LO.FirstOrder.SyntacticFormula (L : LO.FirstOrder.Language) : Type u_1

Equations

• LO.FirstOrder.SyntacticFormula L = LO.FirstOrder.SyntacticSemiformula L 0

def LO.FirstOrder.Semiformula.neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.verum.neg = LO.FirstOrder.Semiformula.falsum
• LO.FirstOrder.Semiformula.falsum.neg = LO.FirstOrder.Semiformula.verum
• (LO.FirstOrder.Semiformula.rel r v).neg = LO.FirstOrder.Semiformula.nrel r v
• (LO.FirstOrder.Semiformula.nrel r v).neg = LO.FirstOrder.Semiformula.rel r v
• (p.and q).neg = p.neg.or q.neg
• (p.or q).neg = p.neg.and q.neg
• p.all.neg = p.neg.ex
• p.ex.neg = p.neg.all

theorem LO.FirstOrder.Semiformula.neg_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : p.neg.neg = p

instance LO.FirstOrder.Semiformula.instLogicalConnective {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.LogicalConnective (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.instLogicalConnective = LO.LogicalConnective.mk

instance LO.FirstOrder.Semiformula.instDeMorgan {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.DeMorgan (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.instDeMorgan = { verum := ⋯, falsum := ⋯, imply := ⋯, and := ⋯, or := ⋯, neg := ⋯ }

instance LO.FirstOrder.Semiformula.instUnivQuantifier {L : LO.FirstOrder.Language} {ξ : Type u_1} : LO.UnivQuantifier (LO.FirstOrder.Semiformula L ξ)

Equations

• LO.FirstOrder.Semiformula.instUnivQuantifier = { univ := fun {n : ℕ} => LO.FirstOrder.Semiformula.all }

instance LO.FirstOrder.Semiformula.instExQuantifier {L : LO.FirstOrder.Language} {ξ : Type u_1} : LO.ExQuantifier (LO.FirstOrder.Semiformula L ξ)

Equations

• LO.FirstOrder.Semiformula.instExQuantifier = { ex := fun {n : ℕ} => LO.FirstOrder.Semiformula.ex }

def LO.FirstOrder.Semiformula.toStr {L : LO.FirstOrder.Language} {ξ : Type u_1} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → String

Equations

• LO.FirstOrder.Semiformula.verum.toStr = "\\top"
• LO.FirstOrder.Semiformula.falsum.toStr = "\\bot"
• (LO.FirstOrder.Semiformula.rel r a).toStr = "{" ++ toString r ++ "}"
• (LO.FirstOrder.Semiformula.rel r v).toStr = ("{" ++ toString r ++ "} \\left(" ++ String.vecToStr fun (i : Fin (n + 1)) => toString (v i)) ++ "\\right)"
• (LO.FirstOrder.Semiformula.nrel r a).toStr = "\\lnot {" ++ toString r ++ "}"
• (LO.FirstOrder.Semiformula.nrel r v).toStr = ("\\lnot {" ++ toString r ++ "} \\left(" ++ String.vecToStr fun (i : Fin (n + 1)) => toString (v i)) ++ "\\right)"
• (p.and q).toStr = "\\left(" ++ p.toStr ++ " \\land " ++ q.toStr ++ "\\right)"
• (p.or q).toStr = "\\left(" ++ p.toStr ++ " \\lor " ++ q.toStr ++ "\\right)"
• p.all.toStr = "(\\forall x_{" ++ toString x ++ "}) " ++ p.toStr
• p.ex.toStr = "(\\exists x_{" ++ toString x ++ "}) " ++ p.toStr

instance LO.FirstOrder.Semiformula.instRepr {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] : Repr (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.instRepr = { reprPrec := fun (t : LO.FirstOrder.Semiformula L ξ n) (x : ℕ) => Std.Format.text t.toStr }

instance LO.FirstOrder.Semiformula.instToString {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] : ToString (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.instToString = { toString := LO.FirstOrder.Semiformula.toStr }

@[simp]

theorem LO.FirstOrder.Semiformula.neg_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ∼⊤ = ⊥

@[simp]

theorem LO.FirstOrder.Semiformula.neg_bot {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ∼⊥ = ⊤

@[simp]

theorem LO.FirstOrder.Semiformula.neg_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : ∼LO.FirstOrder.Semiformula.rel r v = LO.FirstOrder.Semiformula.nrel r v

@[simp]

theorem LO.FirstOrder.Semiformula.neg_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : ∼LO.FirstOrder.Semiformula.nrel r v = LO.FirstOrder.Semiformula.rel r v

@[simp]

theorem LO.FirstOrder.Semiformula.neg_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : ∼(p ⋏ q) = ∼p ⋎ ∼q

@[simp]

theorem LO.FirstOrder.Semiformula.neg_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : ∼(p ⋎ q) = ∼p ⋏ ∼q

@[simp]

theorem LO.FirstOrder.Semiformula.neg_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : ∼(∀' p) = ∃' ∼p

@[simp]

theorem LO.FirstOrder.Semiformula.neg_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : ∼(∃' p) = ∀' ∼p

@[simp]

theorem LO.FirstOrder.Semiformula.neg_neg' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : ∼∼p = p

@[simp]

theorem LO.FirstOrder.Semiformula.neg_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : ∼p = ∼q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.neg_univClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : ∼(∀* p) = ∃* ∼p

@[simp]

theorem LO.FirstOrder.Semiformula.neg_exClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : ∼(∃* p) = ∀* ∼p

theorem LO.FirstOrder.Semiformula.neg_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : ∼p = p.neg

theorem LO.FirstOrder.Semiformula.imp_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : p ➝ q = ∼p ⋎ q

theorem LO.FirstOrder.Semiformula.iff_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : p ⭤ q = (∼p ⋎ q) ⋏ (∼q ⋎ p)

theorem LO.FirstOrder.Semiformula.ball_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (q : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀[p] q) = ∀' (p ➝ q)

theorem LO.FirstOrder.Semiformula.bex_eq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (q : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃[p] q) = ∃' p ⋏ q

@[simp]

theorem LO.FirstOrder.Semiformula.neg_ball {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (q : LO.FirstOrder.Semiformula L ξ (n + 1)) : ∼(∀[p] q) = ∃[p] ∼q

@[simp]

theorem LO.FirstOrder.Semiformula.neg_bex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (q : LO.FirstOrder.Semiformula L ξ (n + 1)) : ∼(∃[p] q) = ∀[p] ∼q

@[simp]

theorem LO.FirstOrder.Semiformula.and_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p₁ : LO.FirstOrder.Semiformula L ξ n) (q₁ : LO.FirstOrder.Semiformula L ξ n) (p₂ : LO.FirstOrder.Semiformula L ξ n) (q₂ : LO.FirstOrder.Semiformula L ξ n) : p₁ ⋏ p₂ = q₁ ⋏ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.FirstOrder.Semiformula.or_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p₁ : LO.FirstOrder.Semiformula L ξ n) (q₁ : LO.FirstOrder.Semiformula L ξ n) (p₂ : LO.FirstOrder.Semiformula L ξ n) (q₂ : LO.FirstOrder.Semiformula L ξ n) : p₁ ⋎ p₂ = q₁ ⋎ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[simp]

theorem LO.FirstOrder.Semiformula.all_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (q : LO.FirstOrder.Semiformula L ξ (n + 1)) : ∀' p = ∀' q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.ex_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) (q : LO.FirstOrder.Semiformula L ξ (n + 1)) : ∃' p = ∃' q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.univClosure_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : ∀* p = ∀* q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.exClosure_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : ∃* p = ∃* q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.univItr_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + k)) (q : LO.FirstOrder.Semiformula L ξ (n + k)) : ∀^[k] p = ∀^[k] q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.exItr_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + k)) (q : LO.FirstOrder.Semiformula L ξ (n + k)) : ∃^[k] p = ∃^[k] q ↔ p = q

@[simp]

theorem LO.FirstOrder.Semiformula.imp_inj {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p₁ : LO.FirstOrder.Semiformula L ξ n} {p₂ : LO.FirstOrder.Semiformula L ξ n} {q₁ : LO.FirstOrder.Semiformula L ξ n} {q₂ : LO.FirstOrder.Semiformula L ξ n} : p₁ ➝ p₂ = q₁ ➝ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.rel! {ξ : Type u_1} {n : ℕ} (L : LO.FirstOrder.Language) (k : ℕ) (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.rel! L k r v = LO.FirstOrder.Semiformula.rel r v

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.nrel! {ξ : Type u_1} {n : ℕ} (L : LO.FirstOrder.Language) (k : ℕ) (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.nrel! L k r v = LO.FirstOrder.Semiformula.nrel r v

def LO.FirstOrder.Semiformula.complexity {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → ℕ

Equations

• LO.FirstOrder.Semiformula.verum.complexity = 0
• LO.FirstOrder.Semiformula.falsum.complexity = 0
• (LO.FirstOrder.Semiformula.rel a a_1).complexity = 0
• (LO.FirstOrder.Semiformula.nrel a a_1).complexity = 0
• (p.and q).complexity = max p.complexity q.complexity + 1
• (p.or q).complexity = max p.complexity q.complexity + 1
• p.all.complexity = p.complexity + 1
• p.ex.complexity = p.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊤.complexity = 0

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_bot {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊥.complexity = 0

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.rel r v).complexity = 0

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.nrel r v).complexity = 0

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋏ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_and' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p.and q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋎ q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_or' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p.or q).complexity = max p.complexity q.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀' p).complexity = p.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_all' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : p.all.complexity = p.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃' p).complexity = p.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_ex' {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : p.ex.complexity = p.complexity + 1

def LO.FirstOrder.Semiformula.cases' {L : LO.FirstOrder.Language} {ξ : Type u_1} {C : (n : ℕ) → LO.FirstOrder.Semiformula L ξ n → Sort w} (hverum : {n : ℕ} → C n ⊤) (hfalsum : {n : ℕ} → C n ⊥) (hrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.rel r v)) (hnrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.nrel r v)) (hand : {n : ℕ} → (p q : LO.FirstOrder.Semiformula L ξ n) → C n (p ⋏ q)) (hor : {n : ℕ} → (p q : LO.FirstOrder.Semiformula L ξ n) → C n (p ⋎ q)) (hall : {n : ℕ} → (p : LO.FirstOrder.Semiformula L ξ (n + 1)) → C n (∀' p)) (hex : {n : ℕ} → (p : LO.FirstOrder.Semiformula L ξ (n + 1)) → C n (∃' p)) {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : C n p

Equations

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

def LO.FirstOrder.Semiformula.rec' {L : LO.FirstOrder.Language} {ξ : Type u_1} {C : (n : ℕ) → LO.FirstOrder.Semiformula L ξ n → Sort w} (hverum : {n : ℕ} → C n ⊤) (hfalsum : {n : ℕ} → C n ⊥) (hrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.rel r v)) (hnrel : {n k : ℕ} → (r : L.Rel k) → (v : Fin k → LO.FirstOrder.Semiterm L ξ n) → C n (LO.FirstOrder.Semiformula.nrel r v)) (hand : {n : ℕ} → (p q : LO.FirstOrder.Semiformula L ξ n) → C n p → C n q → C n (p ⋏ q)) (hor : {n : ℕ} → (p q : LO.FirstOrder.Semiformula L ξ n) → C n p → C n q → C n (p ⋎ q)) (hall : {n : ℕ} → (p : LO.FirstOrder.Semiformula L ξ (n + 1)) → C (n + 1) p → C n (∀' p)) (hex : {n : ℕ} → (p : LO.FirstOrder.Semiformula L ξ (n + 1)) → C (n + 1) p → C n (∃' p)) {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : C n p

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.verum = hverum
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.falsum = hfalsum
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.rel a a_1) = hrel a a_1
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.nrel a a_1) = hnrel a a_1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : (∼p).complexity = p.complexity

def LO.FirstOrder.Semiformula.hasDecEq {L : LO.FirstOrder.Language} {ξ : Type u_1} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [DecidableEq ξ] {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : Decidable (p = q)

instance LO.FirstOrder.Semiformula.instDecidableEq {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [DecidableEq ξ] : DecidableEq (LO.FirstOrder.Semiformula L ξ n)

Equations

• LO.FirstOrder.Semiformula.instDecidableEq = LO.FirstOrder.Semiformula.hasDecEq

def LO.FirstOrder.Semiformula.fv {L : LO.FirstOrder.Language} {ξ : Type u_1} [DecidableEq ξ] {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → Finset ξ

Equations

• (LO.FirstOrder.Semiformula.rel a v).fv = Finset.univ.biUnion fun (i : Fin arity) => (v i).fv
• (LO.FirstOrder.Semiformula.nrel a v).fv = Finset.univ.biUnion fun (i : Fin arity) => (v i).fv
• LO.FirstOrder.Semiformula.verum.fv = ∅
• LO.FirstOrder.Semiformula.falsum.fv = ∅
• (p.and q).fv = p.fv ∪ q.fv
• (p.or q).fv = p.fv ∪ q.fv
• p.all.fv = p.fv
• p.ex.fv = p.fv

theorem LO.FirstOrder.Semiformula.fv_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.rel r v).fv = Finset.univ.biUnion fun (i : Fin k) => (v i).fv

theorem LO.FirstOrder.Semiformula.fv_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.nrel r v).fv = Finset.univ.biUnion fun (i : Fin k) => (v i).fv

@[simp]

theorem LO.FirstOrder.Semiformula.fv_verum {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] : ⊤.fv = ∅

@[simp]

theorem LO.FirstOrder.Semiformula.fv_falsum {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] : ⊥.fv = ∅

@[simp]

theorem LO.FirstOrder.Semiformula.fv_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋏ q).fv = p.fv ∪ q.fv

@[simp]

theorem LO.FirstOrder.Semiformula.fv_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋎ q).fv = p.fv ∪ q.fv

@[simp]

theorem LO.FirstOrder.Semiformula.fv_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀' p).fv = p.fv

@[simp]

theorem LO.FirstOrder.Semiformula.fv_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃' p).fv = p.fv

@[simp]

theorem LO.FirstOrder.Semiformula.fv_not {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ n) : (∼p).fv = p.fv

@[simp]

theorem LO.FirstOrder.Semiformula.fv_imp {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ➝ q).fv = p.fv ∪ q.fv

def LO.FirstOrder.Semiformula.qr {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → ℕ

Equations

• LO.FirstOrder.Semiformula.verum.qr = 0
• LO.FirstOrder.Semiformula.falsum.qr = 0
• (LO.FirstOrder.Semiformula.rel a a_1).qr = 0
• (LO.FirstOrder.Semiformula.nrel a a_1).qr = 0
• (p.and q).qr = max p.qr q.qr
• (p.or q).qr = max p.qr q.qr
• p.all.qr = p.qr + 1
• p.ex.qr = p.qr + 1

@[simp]

theorem LO.FirstOrder.Semiformula.qr_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊤.qr = 0

@[simp]

theorem LO.FirstOrder.Semiformula.qr_bot {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊥.qr = 0

@[simp]

theorem LO.FirstOrder.Semiformula.qr_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.rel r v).qr = 0

@[simp]

theorem LO.FirstOrder.Semiformula.qr_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.nrel r v).qr = 0

@[simp]

theorem LO.FirstOrder.Semiformula.qr_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋏ q).qr = max p.qr q.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋎ q).qr = max p.qr q.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀' p).qr = p.qr + 1

@[simp]

theorem LO.FirstOrder.Semiformula.qr_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃' p).qr = p.qr + 1

@[simp]

theorem LO.FirstOrder.Semiformula.qr_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : (∼p).qr = p.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_imply {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ➝ q).qr = max p.qr q.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⭤ q).qr = max p.qr q.qr

def LO.FirstOrder.Semiformula.Open {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : Prop

Equations

• p.Open = (p.qr = 0)

@[simp]

theorem LO.FirstOrder.Semiformula.open_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊤.Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_bot {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊥.Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.rel r v).Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.nrel r v).Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ n} {q : LO.FirstOrder.Semiformula L ξ n} : (p ⋏ q).Open ↔ p.Open ∧ q.Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ n} {q : LO.FirstOrder.Semiformula L ξ n} : (p ⋎ q).Open ↔ p.Open ∧ q.Open

@[simp]

theorem LO.FirstOrder.Semiformula.not_open_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} : ¬(∀' p).Open

@[simp]

theorem LO.FirstOrder.Semiformula.not_open_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} : ¬(∃' p).Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ n} : (∼p).Open ↔ p.Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_imply {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ n} {q : LO.FirstOrder.Semiformula L ξ n} : (p ➝ q).Open ↔ p.Open ∧ q.Open

@[simp]

theorem LO.FirstOrder.Semiformula.open_iff {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ n} {q : LO.FirstOrder.Semiformula L ξ n} : (p ⭤ q).Open ↔ p.Open ∧ q.Open

def LO.FirstOrder.Semiformula.fvarList {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : LO.FirstOrder.Semiformula L ξ n → List ξ

Equations

• LO.FirstOrder.Semiformula.verum.fvarList = []
• LO.FirstOrder.Semiformula.falsum.fvarList = []
• (LO.FirstOrder.Semiformula.rel a a_1).fvarList = (Matrix.toList fun (i : Fin arity) => (a_1 i).fvarList).join
• (LO.FirstOrder.Semiformula.nrel a a_1).fvarList = (Matrix.toList fun (i : Fin arity) => (a_1 i).fvarList).join
• (p.and q).fvarList = p.fvarList ++ q.fvarList
• (p.or q).fvarList = p.fvarList ++ q.fvarList
• p.all.fvarList = p.fvarList
• p.ex.fvarList = p.fvarList

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.fvar? {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (x : ξ) : Prop

Equations

• p.fvar? x = (x ∈ p.fvarList)

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊤.fvarList = []

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_bot {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} : ⊥.fvarList = []

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋏ q).fvarList = p.fvarList ++ q.fvarList

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋎ q).fvarList = p.fvarList ++ q.fvarList

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀' p).fvarList = p.fvarList

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃' p).fvarList = p.fvarList

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_univClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : (∀* p).fvarList = p.fvarList

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_neg {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : (∼p).fvarList = p.fvarList

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_sentence {L : LO.FirstOrder.Language} {n : ℕ} {o : Type u_2} [IsEmpty o] (p : LO.FirstOrder.Semiformula L o n) : p.fvarList = []

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) {k : ℕ} (R : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.rel R v).fvar? x ↔ ∃ (i : Fin k), (v i).fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) {k : ℕ} (R : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.nrel R v).fvar? x ↔ ∃ (i : Fin k), (v i).fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_top {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) : ¬⊤.fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_falsum {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) : ¬⊥.fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_and {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋏ q).fvar? x ↔ p.fvar? x ∨ q.fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_or {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : (p ⋎ q).fvar? x ↔ p.fvar? x ∨ q.fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_all {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∀' p).fvar? x ↔ p.fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_ex {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) (p : LO.FirstOrder.Semiformula L ξ (n + 1)) : (∃' p).fvar? x ↔ p.fvar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_univClosure {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (x : ξ) (p : LO.FirstOrder.Semiformula L ξ n) : (∀* p).fvar? x ↔ p.fvar? x

def LO.FirstOrder.Semiformula.upper {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) : ℕ

Equations

• LO.FirstOrder.Semiformula.upper p = Option.rec 0 Nat.succ (LO.FirstOrder.Semiformula.fvarList p).maximum?

theorem LO.FirstOrder.Semiformula.List.maximam?_some_of_not_nil {α : Type u_2} [LinearOrder α] {l : List α} (h : l ≠ []) : l.maximum?.isSome = true

@[simp]

theorem LO.FirstOrder.Semiformula.le_foldl_max_self {α : Type u_2} [LinearOrder α] (x : α) (l : List α) : x ≤ List.foldl max x l

theorem LO.FirstOrder.Semiformula.le_foldl_max {α : Type u_2} [LinearOrder α] (x : α) (l : List α) {y : α} : y ∈ l → y ≤ List.foldl max x l

theorem LO.FirstOrder.Semiformula.List.maximam?_eq_some {α : Type u_2} [LinearOrder α] {l : List α} {a : α} (h : l.maximum? = some a) (x : α) : x ∈ l → x ≤ a

theorem LO.FirstOrder.Semiformula.lt_upper_of_fvar? {L : LO.FirstOrder.Language} {n : ℕ} {m : ℕ} {p : LO.FirstOrder.SyntacticSemiformula L n} : LO.FirstOrder.Semiformula.fvar? p m → m < LO.FirstOrder.Semiformula.upper p

theorem LO.FirstOrder.Semiformula.not_fvar?_of_lt_upper {L : LO.FirstOrder.Language} {n : ℕ} {m : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) (h : LO.FirstOrder.Semiformula.upper p ≤ m) : ¬LO.FirstOrder.Semiformula.fvar? p m

@[simp]

theorem LO.FirstOrder.Semiformula.not_fvar?_upper {L : LO.FirstOrder.Language} {n : ℕ} (p : LO.FirstOrder.SyntacticSemiformula L n) : ¬LO.FirstOrder.Semiformula.fvar? p (LO.FirstOrder.Semiformula.upper p)

theorem LO.FirstOrder.Semiformula.ne_of_ne_complexity {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {p : LO.FirstOrder.Semiformula L ξ n} {q : LO.FirstOrder.Semiformula L ξ n} (h : p.complexity ≠ q.complexity) : p ≠ q

@[simp]

theorem LO.FirstOrder.Semiformula.ne_or_left {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : p ≠ p ⋎ q

@[simp]

theorem LO.FirstOrder.Semiformula.ne_or_right {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (q : LO.FirstOrder.Semiformula L ξ n) : q ≠ p ⋎ q

def LO.FirstOrder.Semiformula.lMapAux {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} (Φ : L₁.Hom L₂) {n : ℕ} : LO.FirstOrder.Semiformula L₁ ξ n → LO.FirstOrder.Semiformula L₂ ξ n

Equations

• LO.FirstOrder.Semiformula.lMapAux Φ LO.FirstOrder.Semiformula.verum = ⊤
• LO.FirstOrder.Semiformula.lMapAux Φ LO.FirstOrder.Semiformula.falsum = ⊥
• LO.FirstOrder.Semiformula.lMapAux Φ (LO.FirstOrder.Semiformula.rel a a_1) = LO.FirstOrder.Semiformula.rel (Φ.rel a) (LO.FirstOrder.Semiterm.lMap Φ ∘ a_1)
• LO.FirstOrder.Semiformula.lMapAux Φ (LO.FirstOrder.Semiformula.nrel a a_1) = LO.FirstOrder.Semiformula.nrel (Φ.rel a) (LO.FirstOrder.Semiterm.lMap Φ ∘ a_1)
• LO.FirstOrder.Semiformula.lMapAux Φ (p.and q) = LO.FirstOrder.Semiformula.lMapAux Φ p ⋏ LO.FirstOrder.Semiformula.lMapAux Φ q
• LO.FirstOrder.Semiformula.lMapAux Φ (p.or q) = LO.FirstOrder.Semiformula.lMapAux Φ p ⋎ LO.FirstOrder.Semiformula.lMapAux Φ q
• LO.FirstOrder.Semiformula.lMapAux Φ p.all = ∀' LO.FirstOrder.Semiformula.lMapAux Φ p
• LO.FirstOrder.Semiformula.lMapAux Φ p.ex = ∃' LO.FirstOrder.Semiformula.lMapAux Φ p

theorem LO.FirstOrder.Semiformula.lMapAux_neg {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {n : ℕ} (p : LO.FirstOrder.Semiformula L₁ ξ n) : LO.FirstOrder.Semiformula.lMapAux Φ (∼p) = ∼LO.FirstOrder.Semiformula.lMapAux Φ p

def LO.FirstOrder.Semiformula.lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} (Φ : L₁.Hom L₂) {n : ℕ} : LO.FirstOrder.Semiformula L₁ ξ n →ˡᶜ LO.FirstOrder.Semiformula L₂ ξ n

Equations

• LO.FirstOrder.Semiformula.lMap Φ = { toTr := LO.FirstOrder.Semiformula.lMapAux Φ, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

theorem LO.FirstOrder.Semiformula.lMap_rel {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {k : ℕ} (r : L₁.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) fun (i : Fin k) => LO.FirstOrder.Semiterm.lMap Φ (v i)

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_rel₀ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 0) (v : Fin 0 → LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![]

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_rel₁ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 1) (t : LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r ![t]) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t]

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_rel₂ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 2) (t₁ : LO.FirstOrder.Semiterm L₁ ξ n) (t₂ : LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t₁, LO.FirstOrder.Semiterm.lMap Φ t₂]

theorem LO.FirstOrder.Semiformula.lMap_nrel {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {k : ℕ} (r : L₁.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) fun (i : Fin k) => LO.FirstOrder.Semiterm.lMap Φ (v i)

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_nrel₀ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 0) (v : Fin 0 → LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![]

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_nrel₁ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 1) (t : LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r ![t]) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t]

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_nrel₂ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 2) (t₁ : LO.FirstOrder.Semiterm L₁ ξ n) (t₂ : LO.FirstOrder.Semiterm L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t₁, LO.FirstOrder.Semiterm.lMap Φ t₂]

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_all {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ ξ (n + 1)) : (LO.FirstOrder.Semiformula.lMap Φ) (∀' p) = ∀' (LO.FirstOrder.Semiformula.lMap Φ) p

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_ex {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ ξ (n + 1)) : (LO.FirstOrder.Semiformula.lMap Φ) (∃' p) = ∃' (LO.FirstOrder.Semiformula.lMap Φ) p

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_ball {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ ξ (n + 1)) (q : LO.FirstOrder.Semiformula L₁ ξ (n + 1)) : (LO.FirstOrder.Semiformula.lMap Φ) (∀[p] q) = ∀[(LO.FirstOrder.Semiformula.lMap Φ) p] (LO.FirstOrder.Semiformula.lMap Φ) q

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_bex {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ ξ (n + 1)) (q : LO.FirstOrder.Semiformula L₁ ξ (n + 1)) : (LO.FirstOrder.Semiformula.lMap Φ) (∃[p] q) = ∃[(LO.FirstOrder.Semiformula.lMap Φ) p] (LO.FirstOrder.Semiformula.lMap Φ) q

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_univClosure {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (∀* p) = ∀* (LO.FirstOrder.Semiformula.lMap Φ) p

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_exClosure {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (p : LO.FirstOrder.Semiformula L₁ ξ n) : (LO.FirstOrder.Semiformula.lMap Φ) (∃* p) = ∃* (LO.FirstOrder.Semiformula.lMap Φ) p

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_univItr {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {k : ℕ} (p : LO.FirstOrder.Semiformula L₁ ξ (n + k)) : (LO.FirstOrder.Semiformula.lMap Φ) (∀^[k] p) = ∀^[k] (LO.FirstOrder.Semiformula.lMap Φ) p

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_exItr {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} {k : ℕ} (p : LO.FirstOrder.Semiformula L₁ ξ (n + k)) : (LO.FirstOrder.Semiformula.lMap Φ) (∃^[k] p) = ∃^[k] (LO.FirstOrder.Semiformula.lMap Φ) p

@[simp]

theorem LO.FirstOrder.Semiformula.fvarList_lMap {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} (Φ : L₁.Hom L₂) (p : LO.FirstOrder.Semiformula L₁ ξ n) : ((LO.FirstOrder.Semiformula.lMap Φ) p).fvarList = p.fvarList

def LO.FirstOrder.Semiformula.fvEnum {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type u_2} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ n) : ξ → ℕ

Equations

• p.fvEnum a = List.indexOf a p.fvarList

def LO.FirstOrder.Semiformula.fvEnumInv {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type u_2} [Inhabited ξ] (p : LO.FirstOrder.Semiformula L ξ n) : ℕ → ξ

Equations

• p.fvEnumInv i = if hi : i < p.fvarList.length then p.fvarList.get ⟨i, hi⟩ else default

theorem LO.FirstOrder.Semiformula.fvEnumInv_fvEnum {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type u_2} [DecidableEq ξ] [Inhabited ξ] {p : LO.FirstOrder.Semiformula L ξ n} {x : ξ} (hx : x ∈ p.fvarList) : p.fvEnumInv (p.fvEnum x) = x

def LO.FirstOrder.Semiformula.fvListing {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type u_2} [DecidableEq ξ] (p : LO.FirstOrder.Semiformula L ξ n) : ξ → Fin (p.fvarList.length + 1)

Equations

• p.fvListing x = ⟨List.indexOf x p.fvarList, ⋯⟩

def LO.FirstOrder.Semiformula.fvListingInv {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type u_2} [Inhabited ξ] (p : LO.FirstOrder.Semiformula L ξ n) : Fin (p.fvarList.length + 1) → ξ

Equations

• p.fvListingInv i = if hi : ↑i < p.fvarList.length then p.fvarList.get ⟨↑i, hi⟩ else default

theorem LO.FirstOrder.Semiformula.fvListingInv_fvListing {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type u_2} [DecidableEq ξ] [Inhabited ξ] {p : LO.FirstOrder.Semiformula L ξ n} {x : ξ} (hx : x ∈ p.fvarList) : p.fvListingInv (p.fvListing x) = x

@[reducible, inline]

abbrev LO.FirstOrder.Theory (L : LO.FirstOrder.Language) : Type u_1

Equations

• LO.FirstOrder.Theory L = Set (LO.FirstOrder.SyntacticFormula L)

@[reducible, inline]

abbrev LO.FirstOrder.ClosedTheory (L : LO.FirstOrder.Language) : Type u_1

Equations

• LO.FirstOrder.ClosedTheory L = Set (LO.FirstOrder.Sentence L)

instance LO.FirstOrder.instCollectionSyntacticFormulaTheory {L : LO.FirstOrder.Language} : Collection (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Theory L)

Equations

• LO.FirstOrder.instCollectionSyntacticFormulaTheory = inferInstance

instance LO.FirstOrder.instCollectionSentenceClosedTheory {L : LO.FirstOrder.Language} : Collection (LO.FirstOrder.Sentence L) (LO.FirstOrder.ClosedTheory L)

Equations

• LO.FirstOrder.instCollectionSentenceClosedTheory = inferInstance

def LO.FirstOrder.Theory.lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (Φ : L₁.Hom L₂) (T : LO.FirstOrder.Theory L₁) : LO.FirstOrder.Theory L₂

Equations

• LO.FirstOrder.Theory.lMap Φ T = ⇑(LO.FirstOrder.Semiformula.lMap Φ) '' T

instance LO.FirstOrder.Theory.instAdd {L : LO.FirstOrder.Language} : Add (LO.FirstOrder.Theory L)

Equations

• LO.FirstOrder.Theory.instAdd = { add := fun (x x_1 : LO.FirstOrder.Theory L) => x ∪ x_1 }

theorem LO.FirstOrder.Theory.add_def {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) : T + U = T ∪ U