Formulas of first-order logic #

This file defines the formulas of first-order logic.

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

source

inductive LO.FirstOrder.Semiformula (L : LO.FirstOrder.Language) (ξ : Type u_1) :

ℕ → Type (max u_1 u_2)

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

Instances For

source

@[reducible, inline]

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

Type (max u_1 u_2)

Equations

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

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

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

LO.FirstOrder.Semiformula L ξ n → LO.FirstOrder.Semiformula L ξ n

Equations

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

source

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

p.neg.neg = p

source

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

LO.LogicalConnective (LO.FirstOrder.Semiformula L ξ n)

Equations

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

source

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

LO.DeMorgan (LO.FirstOrder.Semiformula L ξ n)

Equations

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

source

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

LO.UnivQuantifier (LO.FirstOrder.Semiformula L ξ)

Equations

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

source

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

LO.ExQuantifier (LO.FirstOrder.Semiformula L ξ)

Equations

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

source

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

LO.FirstOrder.Semiformula L ξ n → String

Equations

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

source

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

Repr (LO.FirstOrder.Semiformula L ξ n)

Equations

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

source

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

ToString (LO.FirstOrder.Semiformula L ξ n)

Equations

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

source

@[simp]

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

∼⊤ = ⊥

source

@[simp]

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

∼⊥ = ⊤

source

@[simp]

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

∼LO.FirstOrder.Semiformula.rel r v = LO.FirstOrder.Semiformula.nrel r v

source

@[simp]

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

∼LO.FirstOrder.Semiformula.nrel r v = LO.FirstOrder.Semiformula.rel r v

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

∼(∀' p) = ∃' ∼p

source

@[simp]

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

∼(∃' p) = ∀' ∼p

source

@[simp]

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

∼∼p = p

source

@[simp]

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

∼p = ∼q ↔ p = q

source

@[simp]

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

∼(∀* p) = ∃* ∼p

source

@[simp]

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

∼(∃* p) = ∀* ∼p

source

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

∼p = p.neg

source

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

p ➝ q = ∼p ⋎ q

source

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

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

source

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

(∀[p] q) = ∀' (p ➝ q)

source

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

(∃[p] q) = ∃' p ⋏ q

source

@[simp]

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

∼(∀[p] q) = ∃[p] ∼q

source

@[simp]

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

∼(∃[p] q) = ∀[p] ∼q

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

∀' p = ∀' q ↔ p = q

source

@[simp]

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

∃' p = ∃' q ↔ p = q

source

@[simp]

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

∀* p = ∀* q ↔ p = q

source

@[simp]

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

∃* p = ∃* q ↔ p = q

source

@[simp]

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

∀^[k] p = ∀^[k] q ↔ p = q

source

@[simp]

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

∃^[k] p = ∃^[k] q ↔ p = q

source

@[simp]

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

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

source

@[reducible, inline]

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

LO.FirstOrder.Semiformula L ξ n

Equations

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

source

@[reducible, inline]

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

LO.FirstOrder.Semiformula L ξ n

Equations

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

source

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

LO.FirstOrder.Semiformula L ξ n → ℕ

Equations

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

source

@[simp]

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

⊤.complexity = 0

source

@[simp]

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

⊥.complexity = 0

source

@[simp]

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

(LO.FirstOrder.Semiformula.rel r v).complexity = 0

source

@[simp]

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

(LO.FirstOrder.Semiformula.nrel r v).complexity = 0

source

@[simp]

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

(p ⋏ q).complexity = max p.complexity q.complexity + 1

source

@[simp]

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

(p.and q).complexity = max p.complexity q.complexity + 1

source

@[simp]

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

(p ⋎ q).complexity = max p.complexity q.complexity + 1

source

@[simp]

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

(p.or q).complexity = max p.complexity q.complexity + 1

source

@[simp]

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

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

source

@[simp]

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

p.all.complexity = p.complexity + 1

source

@[simp]

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

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

source

@[simp]

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

p.ex.complexity = p.complexity + 1

source

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

C n p

Equations

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

source

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

C n p

Equations

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

source

@[simp]

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

(∼p).complexity = p.complexity

source

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

Decidable (p = q)

source

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

DecidableEq (LO.FirstOrder.Semiformula L ξ n)

Equations

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

source

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

LO.FirstOrder.Semiformula L ξ n → Finset ξ

Equations

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

source

theorem LO.FirstOrder.Semiformula.fv_rel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) :

(LO.FirstOrder.Semiformula.rel r v).fv = Finset.univ.biUnion fun (i : Fin k) => (v i).fv

source

theorem LO.FirstOrder.Semiformula.fv_nrel {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} [DecidableEq ξ] {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) :

(LO.FirstOrder.Semiformula.nrel r v).fv = Finset.univ.biUnion fun (i : Fin k) => (v i).fv

source

@[simp]

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

⊤.fv = ∅

source

@[simp]

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

⊥.fv = ∅

source

@[simp]

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

(p ⋏ q).fv = p.fv ∪ q.fv

source

@[simp]

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

(p ⋎ q).fv = p.fv ∪ q.fv

source

@[simp]

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

(∀' p).fv = p.fv

source

@[simp]

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

(∃' p).fv = p.fv

source

@[simp]

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

(∼p).fv = p.fv

source

@[simp]

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

(p ➝ q).fv = p.fv ∪ q.fv

source

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

LO.FirstOrder.Semiformula L ξ n → ℕ

Equations

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

source

@[simp]

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

⊤.qr = 0

source

@[simp]

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

⊥.qr = 0

source

@[simp]

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

(LO.FirstOrder.Semiformula.rel r v).qr = 0

source

@[simp]

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

(LO.FirstOrder.Semiformula.nrel r v).qr = 0

source

@[simp]

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

(p ⋏ q).qr = max p.qr q.qr

source

@[simp]

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

(p ⋎ q).qr = max p.qr q.qr

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(∼p).qr = p.qr

source

@[simp]

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

(p ➝ q).qr = max p.qr q.qr

source

@[simp]

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

(p ⭤ q).qr = max p.qr q.qr

source

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

Prop

Equations

p.Open = (p.qr = 0)

source

@[simp]

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

⊤.Open

source

@[simp]

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

⊥.Open

source

@[simp]

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

(LO.FirstOrder.Semiformula.rel r v).Open

source

@[simp]

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

(LO.FirstOrder.Semiformula.nrel r v).Open

source

@[simp]

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

(p ⋏ q).Open ↔ p.Open ∧ q.Open

source

@[simp]

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

(p ⋎ q).Open ↔ p.Open ∧ q.Open

source

@[simp]

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

¬(∀' p).Open

source

@[simp]

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

¬(∃' p).Open

source

@[simp]

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

(∼p).Open ↔ p.Open

source

@[simp]

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

(p ➝ q).Open ↔ p.Open ∧ q.Open

source

@[simp]

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

(p ⭤ q).Open ↔ p.Open ∧ q.Open

source

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

LO.FirstOrder.Semiformula L ξ n → List ξ

Equations

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

source

@[reducible, inline]

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

Prop

Equations

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

source

@[simp]

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

⊤.fvarList = []

source

@[simp]

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

⊥.fvarList = []

source

@[simp]

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

(p ⋏ q).fvarList = p.fvarList ++ q.fvarList

source

@[simp]

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

(p ⋎ q).fvarList = p.fvarList ++ q.fvarList

source

@[simp]

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

(∀' p).fvarList = p.fvarList

source

@[simp]

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

(∃' p).fvarList = p.fvarList

source

@[simp]

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

(∀* p).fvarList = p.fvarList

source

@[simp]

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

(∼p).fvarList = p.fvarList

source

@[simp]

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

p.fvarList = []

source

@[simp]

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

(LO.FirstOrder.Semiformula.rel R v).fvar? x ↔ ∃ (i : Fin k), (v i).fvar? x

source

@[simp]

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

(LO.FirstOrder.Semiformula.nrel R v).fvar? x ↔ ∃ (i : Fin k), (v i).fvar? x

source

@[simp]

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

¬⊤.fvar? x

source

@[simp]

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

¬⊥.fvar? x

source

@[simp]

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

(p ⋏ q).fvar? x ↔ p.fvar? x ∨ q.fvar? x

source

@[simp]

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

(p ⋎ q).fvar? x ↔ p.fvar? x ∨ q.fvar? x

source

@[simp]

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

(∀' p).fvar? x ↔ p.fvar? x

source

@[simp]

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

(∃' p).fvar? x ↔ p.fvar? x

source

@[simp]

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

(∀* p).fvar? x ↔ p.fvar? x

source

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

ℕ

Equations

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

source

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

l.maximum?.isSome = true

source

@[simp]

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

x ≤ List.foldl max x l

source

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

y ∈ l → y ≤ List.foldl max x l

source

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

x ∈ l → x ≤ a

source

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

LO.FirstOrder.Semiformula.fvar? p m → m < LO.FirstOrder.Semiformula.upper p

source

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

¬LO.FirstOrder.Semiformula.fvar? p m

source

@[simp]

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

¬LO.FirstOrder.Semiformula.fvar? p (LO.FirstOrder.Semiformula.upper p)

source

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

p ≠ q

source

@[simp]

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

p ≠ p ⋎ q

source

@[simp]

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

q ≠ p ⋎ q

source

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

LO.FirstOrder.Semiformula L₁ ξ n → LO.FirstOrder.Semiformula L₂ ξ n

Equations

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

source

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

LO.FirstOrder.Semiformula.lMapAux Φ (∼p) = ∼LO.FirstOrder.Semiformula.lMapAux Φ p

source

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

LO.FirstOrder.Semiformula L₁ ξ n →ˡᶜ LO.FirstOrder.Semiformula L₂ ξ n

Equations

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

source

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

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) fun (i : Fin k) => LO.FirstOrder.Semiterm.lMap Φ (v i)

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r v) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![]

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r ![t]) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t]

source

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_rel₂ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 2) (t₁ : LO.FirstOrder.Semiterm L₁ ξ n) (t₂ : LO.FirstOrder.Semiterm L₁ ξ n) :

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.rel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.rel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t₁, LO.FirstOrder.Semiterm.lMap Φ t₂]

source

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

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) fun (i : Fin k) => LO.FirstOrder.Semiterm.lMap Φ (v i)

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r v) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![]

source

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_nrel₁ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 1) (t : LO.FirstOrder.Semiterm L₁ ξ n) :

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r ![t]) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t]

source

@[simp]

theorem LO.FirstOrder.Semiformula.lMap_nrel₂ {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type u_2} {Φ : L₁.Hom L₂} (r : L₁.Rel 2) (t₁ : LO.FirstOrder.Semiterm L₁ ξ n) (t₂ : LO.FirstOrder.Semiterm L₁ ξ n) :

(LO.FirstOrder.Semiformula.lMap Φ) (LO.FirstOrder.Semiformula.nrel r ![t₁, t₂]) = LO.FirstOrder.Semiformula.nrel (Φ.rel r) ![LO.FirstOrder.Semiterm.lMap Φ t₁, LO.FirstOrder.Semiterm.lMap Φ t₂]

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∀' p) = ∀' (LO.FirstOrder.Semiformula.lMap Φ) p

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∃' p) = ∃' (LO.FirstOrder.Semiformula.lMap Φ) p

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∀[p] q) = ∀[(LO.FirstOrder.Semiformula.lMap Φ) p] (LO.FirstOrder.Semiformula.lMap Φ) q

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∃[p] q) = ∃[(LO.FirstOrder.Semiformula.lMap Φ) p] (LO.FirstOrder.Semiformula.lMap Φ) q

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∀* p) = ∀* (LO.FirstOrder.Semiformula.lMap Φ) p

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∃* p) = ∃* (LO.FirstOrder.Semiformula.lMap Φ) p

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∀^[k] p) = ∀^[k] (LO.FirstOrder.Semiformula.lMap Φ) p

source

@[simp]

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

(LO.FirstOrder.Semiformula.lMap Φ) (∃^[k] p) = ∃^[k] (LO.FirstOrder.Semiformula.lMap Φ) p

source

@[simp]

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

((LO.FirstOrder.Semiformula.lMap Φ) p).fvarList = p.fvarList

source

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

ξ → ℕ

Equations

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

source

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

ℕ → ξ

Equations

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

source

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

p.fvEnumInv (p.fvEnum x) = x

source

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

ξ → Fin (p.fvarList.length + 1)

Equations

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

source

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

Fin (p.fvarList.length + 1) → ξ

Equations

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

source

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

p.fvListingInv (p.fvListing x) = x

source

@[reducible, inline]

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

Type u_1

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.ClosedTheory (L : LO.FirstOrder.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 : LO.FirstOrder.Language} :

Collection (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Theory L)

Equations

LO.FirstOrder.instCollectionSyntacticFormulaTheory = inferInstance

source

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

Collection (LO.FirstOrder.Sentence L) (LO.FirstOrder.ClosedTheory L)

Equations

LO.FirstOrder.instCollectionSentenceClosedTheory = inferInstance

source

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

LO.FirstOrder.Theory L₂

Equations

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

source

instance LO.FirstOrder.Theory.instAdd {L : LO.FirstOrder.Language} :

Add (LO.FirstOrder.Theory L)

Equations

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

source

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

T + U = T ∪ U

Documentation

Logic.FirstOrder.Basic.Syntax.Formula

Formulas of first-order logic #