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)

A semiformula of language L. Free variables are of type ξ, and bound variables are implemented as de Bruijn indices, of a type Fin n separate from free variables.

• 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
• exs {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.Semiproposition (L : Language) (n : ℕ) : Type u_1

Equations

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

@[reducible, inline]

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

Equations

• LO.FirstOrder.Proposition L = LO.FirstOrder.Semiproposition 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.exs
• φ.exs.neg = φ.neg.all

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

@[implicit_reducible]

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

Equations

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

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

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

@[implicit_reducible]

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

Equations

• LO.FirstOrder.Semiformula.instQuantifier = { all := fun {n : ℕ} => LO.FirstOrder.Semiformula.all, exs := fun {n : ℕ} => LO.FirstOrder.Semiformula.exs }

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
• φ.exs.toStr = "(\\exists x_{" ++ toString n ++ "}) " ++ φ.toStr

@[implicit_reducible]

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 }

@[implicit_reducible]

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_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_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_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : ∼φ = ∼ψ ↔ φ = ψ

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.neg_exsClosure {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.bexs_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_bexs {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.exs_inj {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) : ∃⁰ φ = ∃⁰ ψ ↔ φ = ψ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.exsItr_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 → ℕ

The complexity of a semiformula, taking max at logical connectives.

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 = max φ.complexity ψ.complexity + 1
• (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1
• φ.all.complexity = φ.complexity + 1
• φ.exs.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 = max φ.complexity ψ.complexity + 1

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_or' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ.or ψ).complexity = max φ.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_exs {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : (∃⁰ φ).complexity = φ.complexity + 1

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_exs' {L : Language} {ξ : Type u_1} {n : ℕ} (φ : Semiformula L ξ (n + 1)) : φ.exs.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 (∀⁰ φ)) (hexs : {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 hexs LO.FirstOrder.Semiformula.verum = hverum
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs LO.FirstOrder.Semiformula.falsum = hfalsum
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (LO.FirstOrder.Semiformula.rel r v) = hrel r v
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (LO.FirstOrder.Semiformula.nrel r v) = hnrel r v
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (φ.and ψ) = hand φ ψ
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs (φ.or ψ) = hor φ ψ
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs φ.all = hall φ
• LO.FirstOrder.Semiformula.cases' hverum hfalsum hrel hnrel hand hor hall hexs φ.exs = hexs φ

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 (∀⁰ φ)) (hexs : {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 hexs LO.FirstOrder.Semiformula.verum = hverum
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs LO.FirstOrder.Semiformula.falsum = hfalsum
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs (LO.FirstOrder.Semiformula.rel r v) = hrel r v
• LO.FirstOrder.Semiformula.rec' hverum hfalsum hrel hnrel hand hor hall hexs (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} [L.DecidableEq] [DecidableEq ξ] {n : ℕ} (φ ψ : Semiformula L ξ n) : Decidable (φ = ψ)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Semiformula.instDecidableEq {L : Language} {ξ : Type u_1} {n : ℕ} [L.DecidableEq] [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 = max φ.qr ψ.qr
• (φ.or ψ).qr = max φ.qr ψ.qr
• φ.all.qr = φ.qr + 1
• φ.exs.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 = max φ.qr ψ.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_or {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ ⋎ ψ).qr = max φ.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_exs {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 = max φ.qr ψ.qr

@[simp]

theorem LO.FirstOrder.Semiformula.qr_iff {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) : (φ 🡘 ψ).qr = max φ.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_exs {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
• φ.exs.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_exs {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_allClosure {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?_exs {L : Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] (x : ξ) (φ : Semiformula L ξ (n + 1)) : (∃⁰ φ).FVar? x ↔ φ.FVar? x

@[simp]

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

def LO.FirstOrder.Semiformula.fvSup {L : Language} {n : ℕ} (φ : Semiproposition 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 : ℕ} {φ : Semiproposition L n} : FVar? φ m → m < fvSup φ

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

@[simp]

theorem LO.FirstOrder.Semiformula.not_fvar?_fvSup {L : Language} {n : ℕ} (φ : Semiproposition 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 α] [Std.LawfulOrderSup α] {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 Φ φ.exs = ∃⁰ 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

The map on semiformulas induced by a homomorphism between languages.

Equations

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

@[simp]

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) (Semiterm.lMap Φ ∘ v)

@[simp]

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) (Semiterm.lMap Φ ∘ v)

@[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_exs {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_bexs {n : ℕ} {L₁ : Language} {L₂ : Language} {ξ : Type u_5} {Φ : L₁.Hom L₂} (φ ψ : Semiformula L₁ ξ (n + 1)) : (lMap Φ) (∃⁰[φ] ψ) = ∃⁰[(lMap Φ) φ] (lMap Φ) ψ

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_allItr {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_exsItr {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

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

Equations

• LO.FirstOrder.Semiformula.verum.fvarList = []
• LO.FirstOrder.Semiformula.falsum.fvarList = []
• (LO.FirstOrder.Semiformula.rel r v).fvarList = (Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten
• (LO.FirstOrder.Semiformula.nrel r v).fvarList = (Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten
• (φ.and ψ).fvarList = φ.fvarList ++ ψ.fvarList
• (φ.or ψ).fvarList = φ.fvarList ++ ψ.fvarList
• φ.all.fvarList = φ.fvarList
• φ.exs.fvarList = φ.fvarList

def LO.FirstOrder.Semiformula.idxOfFVar {n : ℕ} {L : Language} {ξ : Type u_5} [DecidableEq ξ] (φ : Semiformula L ξ n) : ξ → ℕ

Equations

• φ.idxOfFVar a = List.idxOf a φ.fvarList

def LO.FirstOrder.Semiformula.enumarateFVar {n : ℕ} {L : Language} {ξ : Type u_5} [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ

Equations

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

theorem LO.FirstOrder.Semiformula.enumarateFVar_idxOfFVar {n : ℕ} {L : Language} {ξ : Type u_5} [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) : φ.enumarateFVar (φ.idxOfFVar x) = x

theorem LO.FirstOrder.Semiformula.mem_fvarList_iff_fvar? {n : ℕ} {L : Language} {ξ : Type u_5} {x : ξ} [DecidableEq ξ] {φ : Semiformula L ξ n} : x ∈ φ.fvarList ↔ φ.FVar? x

@[reducible, inline]

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

Equations

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

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