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.

source

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

Instances For

source

@[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

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

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

source

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

φ.neg.neg = φ

source

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

LogicalConnective (Semiformula L ξ n)

Equations

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

source

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

DeMorgan (Semiformula L ξ n)

source

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

Quantifier (Semiformula L ξ)

Equations

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

source

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

source

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 }

source

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 }

source

@[simp]

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

∼⊤ = ⊥

source

@[simp]

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

∼⊥ = ⊤

source

@[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

source

@[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

source

@[simp]

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

∼(φ ⋏ ψ) = ∼φ ⋎ ∼ψ

source

@[simp]

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

∼(φ ⋎ ψ) = ∼φ ⋏ ∼ψ

source

@[simp]

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

∼(∀' φ) = ∃' ∼φ

source

@[simp]

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

∼(∃' φ) = ∀' ∼φ

source

@[simp]

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

∼∼φ = φ

source

@[simp]

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

∼φ = ∼ψ ↔ φ = ψ

source

@[simp]

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

∼(∀* φ) = ∃* ∼φ

source

@[simp]

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

∼(∃* φ) = ∀* ∼φ

source

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

∼φ = φ.neg

source

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

φ ➝ ψ = ∼φ ⋎ ψ

source

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

φ ⭤ ψ = (∼φ ⋎ ψ) ⋏ (∼ψ ⋎ φ)

source

theorem LO.FirstOrder.Semiformula.ball_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) :

(∀[φ] ψ) = ∀' (φ ➝ ψ)

source

theorem LO.FirstOrder.Semiformula.bex_eq {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) :

(∃[φ] ψ) = ∃' φ ⋏ ψ

source

@[simp]

theorem LO.FirstOrder.Semiformula.neg_ball {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) :

∼(∀[φ] ψ) = ∃[φ] ∼ψ

source

@[simp]

theorem LO.FirstOrder.Semiformula.neg_bex {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ (n + 1)) :

∼(∃[φ] ψ) = ∀[φ] ∼ψ

source

@[simp]

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

φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

source

@[simp]

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

φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

source

@[simp]

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

∀' φ = ∀' ψ ↔ φ = ψ

source

@[simp]

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

∃' φ = ∃' ψ ↔ φ = ψ

source

@[simp]

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

∀* φ = ∀* ψ ↔ φ = ψ

source

@[simp]

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

∃* φ = ∃* ψ ↔ φ = ψ

source

@[simp]

theorem LO.FirstOrder.Semiformula.univItr_inj {L : Language} {ξ : Type u_1} {n k : ℕ} (φ ψ : Semiformula L ξ (n + k)) :

∀^[k] φ = ∀^[k] ψ ↔ φ = ψ

source

@[simp]

theorem LO.FirstOrder.Semiformula.exItr_inj {L : Language} {ξ : Type u_1} {n k : ℕ} (φ ψ : Semiformula L ξ (n + k)) :

∃^[k] φ = ∃^[k] ψ ↔ φ = ψ

source

@[simp]

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

φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

source

@[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

source

@[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

source

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

source

@[simp]

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

⊤.complexity = 0

source

@[simp]

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

⊥.complexity = 0

source

@[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

source

@[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

source

@[simp]

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

(φ ⋏ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_and' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ.and ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

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

(φ ⋎ ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

theorem LO.FirstOrder.Semiformula.complexity_or' {L : Language} {ξ : Type u_1} {n : ℕ} (φ ψ : Semiformula L ξ n) :

(φ.or ψ).complexity = φ.complexity ⊔ ψ.complexity + 1

source

@[simp]

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

(∀' φ).complexity = φ.complexity + 1

source

@[simp]

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

φ.all.complexity = φ.complexity + 1

source

@[simp]

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

(∃' φ).complexity = φ.complexity + 1

source

@[simp]

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

φ.ex.complexity = φ.complexity + 1

source

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 φ

source

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

source

@[simp]

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

(∼φ).complexity = φ.complexity

source

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 (φ = ψ)

source

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

source

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

source

@[simp]

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

⊤.qr = 0

source

@[simp]

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

⊥.qr = 0

source

@[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

source

@[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

source

@[simp]

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

(φ ⋏ ψ).qr = φ.qr ⊔ ψ.qr

source

@[simp]

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

(φ ⋎ ψ).qr = φ.qr ⊔ ψ.qr

source

@[simp]

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

(∀' φ).qr = φ.qr + 1

source

@[simp]

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

(∃' φ).qr = φ.qr + 1

source

@[simp]

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

(∼φ).qr = φ.qr

source

@[simp]

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

(φ ➝ ψ).qr = φ.qr ⊔ ψ.qr

source

@[simp]

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

(φ ⭤ ψ).qr = φ.qr ⊔ ψ.qr

Open (Semi-)Formula

source

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

Prop

Equations

φ.Open = (φ.qr = 0)

source

@[simp]

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

⊤.Open

source

@[simp]

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

⊥.Open

source

@[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

source

@[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

source

@[simp]

theorem LO.FirstOrder.Semiformula.open_and {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} :

(φ ⋏ ψ).Open ↔ φ.Open ∧ ψ.Open

source

@[simp]

theorem LO.FirstOrder.Semiformula.open_or {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} :

(φ ⋎ ψ).Open ↔ φ.Open ∧ ψ.Open

source

@[simp]

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

¬(∀' φ).Open

source

@[simp]

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

¬(∃' φ).Open

source

@[simp]

theorem LO.FirstOrder.Semiformula.open_neg {L : Language} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} :

(∼φ).Open ↔ φ.Open

source

@[simp]

theorem LO.FirstOrder.Semiformula.open_imply {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} :

(φ ➝ ψ).Open ↔ φ.Open ∧ ψ.Open

source

@[simp]

theorem LO.FirstOrder.Semiformula.open_iff {L : Language} {ξ : Type u_1} {n : ℕ} {φ ψ : Semiformula L ξ n} :

(φ ⭤ ψ).Open ↔ φ.Open ∧ ψ.Open

Free Variables

source

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

source

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

source

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

source

@[simp]

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

⊤.freeVariables = ∅

source

@[simp]

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

⊥.freeVariables = ∅

source

@[simp]

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

(φ ⋏ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

source

@[simp]

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

(φ ⋎ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

source

@[simp]

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

(∀' φ).freeVariables = φ.freeVariables

source

@[simp]

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

(∃' φ).freeVariables = φ.freeVariables

source

@[simp]

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

(∼φ).freeVariables = φ.freeVariables

source

@[simp]

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

(φ ➝ ψ).freeVariables = φ.freeVariables ∪ ψ.freeVariables

source

@[simp]

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

(∀* φ).freeVariables = φ.freeVariables

source

@[simp]

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

φ.freeVariables = ∅

source

@[reducible, inline]

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

Prop

Equations

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

source

@[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

source

@[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

source

@[simp]

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

¬⊤.FVar? x

source

@[simp]

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

¬⊥.FVar? x

source

@[simp]

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

(φ ⋏ ψ).FVar? x ↔ φ.FVar? x ∨ ψ.FVar? x

source

@[simp]

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

(φ ⋎ ψ).FVar? x ↔ φ.FVar? x ∨ ψ.FVar? x

source

@[simp]

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

(∀' φ).FVar? x ↔ φ.FVar? x

source

@[simp]

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

(∃' φ).FVar? x ↔ φ.FVar? x

source

@[simp]

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

(∀* φ).FVar? x ↔ φ.FVar? x

source

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

source

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

FVar? φ m → m < fvSup φ

source

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

¬FVar? φ m

source

@[simp]

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

¬FVar? φ (fvSup φ)

source

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

l.max?.isSome = true

source

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

source

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

φ ≠ ψ

source

@[simp]

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

φ ≠ φ ⋎ ψ

source

@[simp]

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

ψ ≠ φ ⋎ ψ

source

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 Φ φ

source

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

lMapAux Φ (∼φ) = ∼lMapAux Φ φ

source

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' := ⋯ }

source

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)

source

@[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) ![]

source

@[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]

source

@[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₂]

source

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)

source

@[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) ![]

source

@[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]

source

@[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₂]

source

@[simp]

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

(lMap Φ) (∀' φ) = ∀' (lMap Φ) φ

source

@[simp]

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

(lMap Φ) (∃' φ) = ∃' (lMap Φ) φ

source

@[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 Φ) ψ

source

@[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 Φ) ψ

source

@[simp]

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

(lMap Φ) (∀* φ) = ∀* (lMap Φ) φ

source

@[simp]

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

(lMap Φ) (∃* φ) = ∃* (lMap Φ) φ

source

@[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 Φ) φ

source

@[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 Φ) φ

source

@[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

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

LO.FirstOrder.instCollectionSentenceClosedTheory

source

instance LO.FirstOrder.instCollectionSyntacticFormulaTheory {L : Language} :

Collection (SyntacticFormula L) (Theory L)

Equations

LO.FirstOrder.instCollectionSyntacticFormulaTheory = inferInstance

source

instance LO.FirstOrder.instCollectionSentenceClosedTheory {L : Language} :

Collection (Sentence L) (ClosedTheory L)

Equations

LO.FirstOrder.instCollectionSentenceClosedTheory = inferInstance

source

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

source

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 }

source

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

T + U = T ∪ U

Documentation

Foundation.FirstOrder.Basic.Syntax.Formula

Formulas of first-order logic #