Formulas of first-order logic

This file defines the formulas of first-order logic.

φ : 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 : Language) (ξ : Type u_1) : ℕ → Type (max u_1 u_2)

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

@[reducible, inline]

abbrev LO.FirstOrder.Formula (L : 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 : Language) : Type u_1

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

def LO.FirstOrder.Semiformula.neg {L : Language} {ξ : Type u_1} {n : ℕ} : Semiformula L ξ n → 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
• (φ.and ψ).neg = φ.neg.or ψ.neg
• (φ.or ψ).neg = φ.neg.and ψ.neg
• φ.all.neg = φ.neg.ex
• φ.ex.neg = φ.neg.all

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

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

Equations

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

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

instance LO.FirstOrder.Semiformula.instQuantifier {L : Language} {ξ : Type u_1} : Quantifier (Semiformula L ξ)

Equations

• LO.FirstOrder.Semiformula.instQuantifier = LO.Quantifier.mk

def LO.FirstOrder.Semiformula.toStr {L : Language} {ξ : Type u_1} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] {n : ℕ} : 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 + 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 + 1)) => toString (v i)) ++ "\\right)"
• (φ.and ψ).toStr = "\\left(" ++ φ.toStr ++ " \\land " ++ ψ.toStr ++ "\\right)"
• (φ.or ψ).toStr = "\\left(" ++ φ.toStr ++ " \\lor " ++ ψ.toStr ++ "\\right)"
• φ.all.toStr = "(\\forall x_{" ++ toString n ++ "}) " ++ φ.toStr
• φ.ex.toStr = "(\\exists x_{" ++ toString n ++ "}) " ++ φ.toStr

instance LO.FirstOrder.Semiformula.instRepr {L : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] : Repr (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 : Language} {ξ : Type u_1} {n : ℕ} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] [ToString ξ] : ToString (Semiformula L ξ n)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.rel! {ξ : Type u_1} {n : ℕ} (L : Language) (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : 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 : Language) (k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : Semiformula L ξ n

Equations

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

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

Equations

• LO.FirstOrder.Semiformula.verum.complexity = 0
• LO.FirstOrder.Semiformula.falsum.complexity = 0
• (LO.FirstOrder.Semiformula.rel r v).complexity = 0
• (LO.FirstOrder.Semiformula.nrel r v).complexity = 0
• (φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• (φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• φ.all.complexity = φ.complexity + 1
• φ.ex.complexity = φ.complexity + 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_and {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.verum = hverum
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex LO.FirstOrder.Semiformula.falsum = hfalsum
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.rel r v) = hrel r v
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.nrel r v) = hnrel r v
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (φ.and ψ) = hand φ ψ
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex (φ.or ψ) = hor φ ψ
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex φ.all = hall φ
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hex φ.ex = hex φ

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

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 r v) = hrel r v
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hex (LO.FirstOrder.Semiformula.nrel r v) = hnrel r v

@[simp]

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

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

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

Equations

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

Quantifier Rank

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

Equations

• LO.FirstOrder.Semiformula.verum.qr = 0
• LO.FirstOrder.Semiformula.falsum.qr = 0
• (LO.FirstOrder.Semiformula.rel r v).qr = 0
• (LO.FirstOrder.Semiformula.nrel r v).qr = 0
• (φ.and ψ).qr = φ.qr ⊔ ψ.qr
• (φ.or ψ).qr = φ.qr ⊔ ψ.qr
• φ.all.qr = φ.qr + 1
• φ.ex.qr = φ.qr + 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.qr_and {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).qr = φ.qr ⊔ ψ.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).qr = φ.qr ⊔ ψ.qr

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.qr_imply {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ➝ ψ).qr = φ.qr ⊔ ψ.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⭤ ψ).qr = φ.qr ⊔ ψ.qr

Open (Semi-)Formula

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Free Variables

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_and {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_or {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_not {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) : (∼φ).freeVariables = φ.freeVariables

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_imp {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ ψ : Semiformula L ξ n) : (φ ➝ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_univClosure {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) : (∀* φ).freeVariables = φ.freeVariables

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_sentence {L : Language} {n : ℕ} {ο : Type u_5} [IsEmpty ο] (φ : Semiformula L ο n) : φ.freeVariables = ∅

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.FVar? {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) (x : ξ) : Prop

Equations

• φ.FVar? x = (x ∈ φ.freeVariables)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_and {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ ψ : Semiformula L ξ n) : (φ ⋏ ψ).FVar? x ↔ φ.FVar? x ∨ ψ.FVar? x

@[simp]

theorem LO.FirstOrder.Semiformula.fvar?_or {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).FVar? x ↔ φ.FVar? x ∨ ψ.FVar? x

@[simp]

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Semiformula.fvSup {L : Language} {n : ℕ} (φ : SyntacticSemiformula L n) : ℕ

Equations

• LO.FirstOrder.Semiformula.fvSup φ = WithBot.recBotCoe 0 Nat.succ (LO.FirstOrder.Semiformula.freeVariables φ).max

theorem LO.FirstOrder.Semiformula.lt_fvSup_of_fvar? {L : Language} {n m : ℕ} {φ : SyntacticSemiformula L n} : FVar? φ m → m < fvSup φ

theorem LO.FirstOrder.Semiformula.not_fvar?_of_lt_fvSup {L : Language} {n m : ℕ} (φ : SyntacticSemiformula L n) (h : fvSup φ ≤ m) : ¬FVar? φ m

@[simp]

theorem LO.FirstOrder.Semiformula.not_fvar?_fvSup {L : Language} {n : ℕ} (φ : SyntacticSemiformula L n) : ¬FVar? φ (fvSup φ)

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

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

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

@[simp]

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

@[simp]

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

def LO.FirstOrder.Semiformula.lMapAux {L₁ : Language} {L₂ : Language} {ξ : Type u_5} (Φ : L₁.Hom L₂) {n : ℕ} : Semiformula L₁ ξ n → 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 r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) (LO.FirstOrder.Semiterm.lMap Φ ∘ v)
• LO.FirstOrder.Semiformula.lMapAux Φ (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) (LO.FirstOrder.Semiterm.lMap Φ ∘ v)
• LO.FirstOrder.Semiformula.lMapAux Φ (φ.and ψ) = LO.FirstOrder.Semiformula.lMapAux Φ φ ⋏ LO.FirstOrder.Semiformula.lMapAux Φ ψ
• LO.FirstOrder.Semiformula.lMapAux Φ (φ.or ψ) = LO.FirstOrder.Semiformula.lMapAux Φ φ ⋎ LO.FirstOrder.Semiformula.lMapAux Φ ψ
• LO.FirstOrder.Semiformula.lMapAux Φ φ.all = ∀' LO.FirstOrder.Semiformula.lMapAux Φ φ
• LO.FirstOrder.Semiformula.lMapAux Φ φ.ex = ∃' LO.FirstOrder.Semiformula.lMapAux Φ φ

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

def LO.FirstOrder.Semiformula.lMap {L₁ : Language} {L₂ : Language} {ξ : Type u_5} (Φ : L₁.Hom L₂) {n : ℕ} : Semiformula L₁ ξ n →ˡᶜ 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₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} {k : ℕ} (r : L₁.Rel k) (v : Fin k → Semiterm L₁ ξ n) : (lMap Φ) (rel r v) = rel (Φ.rel r) fun (i : Fin k) => Semiterm.lMap Φ (v i)

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.freeVariables_lMap {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} [DecidableEq ξ] (Φ : L₁.Hom L₂) (φ : Semiformula L₁ ξ n) : ((lMap Φ) φ).freeVariables = φ.freeVariables

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

• LO.FirstOrder.instCollectionSyntacticFormulaTheory = inferInstance

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

Equations

• LO.FirstOrder.instCollectionSentenceClosedTheory = inferInstance

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

Equations

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

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

Equations

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

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