Semantics of first-order logic

This file defines the structure and the evaluation of terms and formulas by Tarski's truth definition.

theorem LO.FirstOrder.Structure.ext {L : LO.FirstOrder.Language} {M : Type w} (x : LO.FirstOrder.Structure L M) (y : LO.FirstOrder.Structure L M) (func : LO.FirstOrder.Structure.func = LO.FirstOrder.Structure.func) (rel : LO.FirstOrder.Structure.rel = LO.FirstOrder.Structure.rel) : x = y

theorem LO.FirstOrder.Structure.ext_iff {L : LO.FirstOrder.Language} {M : Type w} (x : LO.FirstOrder.Structure L M) (y : LO.FirstOrder.Structure L M) : x = y ↔ LO.FirstOrder.Structure.func = LO.FirstOrder.Structure.func ∧ LO.FirstOrder.Structure.rel = LO.FirstOrder.Structure.rel

class LO.FirstOrder.Structure (L : LO.FirstOrder.Language) (M : Type w) : Type (max u w)

• func : ⦃k : ℕ⦄ → L.Func k → (Fin k → M) → M
• rel : ⦃k : ℕ⦄ → L.Rel k → (Fin k → M) → Prop

structure LO.FirstOrder.Struc (L : LO.FirstOrder.Language) : Type (max (u_1 + 1) u_2)

• Dom : Type u_1
• nonempty : Nonempty self.Dom
• struc : LO.FirstOrder.Structure L self.Dom

theorem LO.FirstOrder.Struc.nonempty {L : LO.FirstOrder.Language} (self : LO.FirstOrder.Struc L) : Nonempty self.Dom

@[reducible, inline]

abbrev LO.FirstOrder.SmallStruc (L : LO.FirstOrder.Language) : Type (u + 1)

Equations

• LO.FirstOrder.SmallStruc L = LO.FirstOrder.Struc L

instance LO.FirstOrder.Structure.instNonempty {L : LO.FirstOrder.Language} {M : Type u_1} [n : Nonempty M] : Nonempty (LO.FirstOrder.Structure L M)

Equations

• ⋯ = ⋯

def LO.FirstOrder.Structure.lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (φ : L₁.Hom L₂) {M : Type w} (S : LO.FirstOrder.Structure L₂ M) : LO.FirstOrder.Structure L₁ M

Equations

• LO.FirstOrder.Structure.lMap φ S = { func := fun (x : ℕ) (f : L₁.Func x) => LO.FirstOrder.Structure.func (φ.func f), rel := fun (x : ℕ) (r : L₁.Rel x) => LO.FirstOrder.Structure.rel (φ.rel r) }

@[simp]

theorem LO.FirstOrder.Structure.lMap_func {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (φ : L₁.Hom L₂) {M : Type w} (s₂ : LO.FirstOrder.Structure L₂ M) {k : ℕ} {f : L₁.Func k} {v : Fin k → M} : LO.FirstOrder.Structure.func f v = LO.FirstOrder.Structure.func (φ.func f) v

@[simp]

theorem LO.FirstOrder.Structure.lMap_rel {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} (φ : L₁.Hom L₂) {M : Type w} (s₂ : LO.FirstOrder.Structure L₂ M) {k : ℕ} {r : L₁.Rel k} {v : Fin k → M} : LO.FirstOrder.Structure.rel r v ↔ LO.FirstOrder.Structure.rel (φ.rel r) v

def LO.FirstOrder.Structure.ofEquiv {L : LO.FirstOrder.Language} {M : Type w} [LO.FirstOrder.Structure L M] {N : Type w'} (φ : M ≃ N) : LO.FirstOrder.Structure L N

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Structure.Decidable (L : LO.FirstOrder.Language) (M : Type w) [s : LO.FirstOrder.Structure L M] : Type (max w u)

Equations

• LO.FirstOrder.Structure.Decidable L M = ({k : ℕ} → (r : L.Rel k) → (v : Fin k → M) → Decidable (LO.FirstOrder.Structure.rel r v))

noncomputable instance LO.FirstOrder.Structure.instDecidable {L : LO.FirstOrder.Language} {M : Type w} [LO.FirstOrder.Structure L M] : LO.FirstOrder.Structure.Decidable L M

Equations

• LO.FirstOrder.Structure.instDecidable r v = Classical.dec (LO.FirstOrder.Structure.rel r v)

@[reducible]

def LO.FirstOrder.Structure.toStruc {L : LO.FirstOrder.Language} {M : Type w} [i : Nonempty M] (s : LO.FirstOrder.Structure L M) : LO.FirstOrder.Struc L

Equations

• s.toStruc = { Dom := M, nonempty := i, struc := s }

instance LO.FirstOrder.Struc.instNonemptyDom {L : LO.FirstOrder.Language} (s : LO.FirstOrder.Struc L) : Nonempty s.Dom

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Struc.instStructureDom {L : LO.FirstOrder.Language} (s : LO.FirstOrder.Struc L) : LO.FirstOrder.Structure L s.Dom

Equations

• s.instStructureDom = s.struc

def LO.FirstOrder.Semiterm.val {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} (s : LO.FirstOrder.Structure L M) (e : Fin n → M) (ε : ξ → M) : LO.FirstOrder.Semiterm L ξ n → M

Equations

• LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.bvar x_1) = e x_1
• LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.fvar x_1) = ε x_1
• LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Structure.func f fun (i : Fin arity) => LO.FirstOrder.Semiterm.val s e ε (v i)

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.valb {n : ℕ} {L : LO.FirstOrder.Language} {M : Type w} (s : LO.FirstOrder.Structure L M) (e : Fin n → M) (t : LO.FirstOrder.Semiterm L Empty n) : M

Equations

• LO.FirstOrder.Semiterm.valb s e t = LO.FirstOrder.Semiterm.val s e Empty.elim t

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.valm {L : LO.FirstOrder.Language} {ξ : Type v} (M : Type w) [s : LO.FirstOrder.Structure L M] {n : ℕ} (e : Fin n → M) (ε : ξ → M) : LO.FirstOrder.Semiterm L ξ n → M

Equations

• LO.FirstOrder.Semiterm.valm M e ε = LO.FirstOrder.Semiterm.val s e ε

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.valbm {L : LO.FirstOrder.Language} (M : Type w) [s : LO.FirstOrder.Structure L M] {n : ℕ} (e : Fin n → M) : LO.FirstOrder.Semiterm L Empty n → M

Equations

• LO.FirstOrder.Semiterm.valbm M e = LO.FirstOrder.Semiterm.valb s e

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.realize {L : LO.FirstOrder.Language} {M : Type w} (s : LO.FirstOrder.Structure L M) (t : LO.FirstOrder.Term L M) : M

Equations

• LO.FirstOrder.Semiterm.realize s t = LO.FirstOrder.Semiterm.val s ![] id t

@[simp]

theorem LO.FirstOrder.Semiterm.val_bvar {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (x : Fin n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.bvar x) = e x

@[simp]

theorem LO.FirstOrder.Semiterm.val_fvar {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (x : ξ) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.fvar x) = ε x

theorem LO.FirstOrder.Semiterm.val_func {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} {k : ℕ} (f : L.Func k) (v : Fin k → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Structure.func f fun (i : Fin k) => LO.FirstOrder.Semiterm.val s e ε (v i)

@[simp]

theorem LO.FirstOrder.Semiterm.val_func₀ {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (f : L.Func 0) (v : Fin 0 → LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.func f v) = LO.FirstOrder.Structure.func f ![]

@[simp]

theorem LO.FirstOrder.Semiterm.val_func₁ {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (f : L.Func 1) (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.func f ![t]) = LO.FirstOrder.Structure.func f ![LO.FirstOrder.Semiterm.val s e ε t]

@[simp]

theorem LO.FirstOrder.Semiterm.val_func₂ {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (f : L.Func 2) (t : LO.FirstOrder.Semiterm L ξ n) (u : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Semiterm.func f ![t, u]) = LO.FirstOrder.Structure.func f ![LO.FirstOrder.Semiterm.val s e ε t, LO.FirstOrder.Semiterm.val s e ε u]

theorem LO.FirstOrder.Semiterm.val_rew {n₁ : ℕ} {n₂ : ℕ} {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ε₂ : μ₂ → M} (ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂) (t : LO.FirstOrder.Semiterm L μ₁ n₁) : LO.FirstOrder.Semiterm.val s e₂ ε₂ (ω t) = LO.FirstOrder.Semiterm.val s (LO.FirstOrder.Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.bvar) (LO.FirstOrder.Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.fvar) t

theorem LO.FirstOrder.Semiterm.val_rewrite {n : ℕ} {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε₂ : μ₂ → M} (f : μ₁ → LO.FirstOrder.Semiterm L μ₂ n) (t : LO.FirstOrder.Semiterm L μ₁ n) : LO.FirstOrder.Semiterm.val s e ε₂ ((LO.FirstOrder.Rew.rewrite f) t) = LO.FirstOrder.Semiterm.val s e (fun (x : μ₁) => LO.FirstOrder.Semiterm.val s e ε₂ (f x)) t

theorem LO.FirstOrder.Semiterm.val_rewriteMap {n : ℕ} {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε₂ : μ₂ → M} (f : μ₁ → μ₂) (t : LO.FirstOrder.Semiterm L μ₁ n) : LO.FirstOrder.Semiterm.val s e ε₂ ((LO.FirstOrder.Rew.rewriteMap f) t) = LO.FirstOrder.Semiterm.val s e (fun (x : μ₁) => ε₂ (f x)) t

theorem LO.FirstOrder.Semiterm.val_substs {n₁ : ℕ} {n₂ : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ε : ξ → M} (w : Fin n₁ → LO.FirstOrder.Semiterm L ξ n₂) (t : LO.FirstOrder.Semiterm L ξ n₁) : LO.FirstOrder.Semiterm.val s e₂ ε ((LO.FirstOrder.Rew.substs w) t) = LO.FirstOrder.Semiterm.val s (fun (x : Fin n₁) => LO.FirstOrder.Semiterm.val s e₂ ε (w x)) ε t

@[simp]

theorem LO.FirstOrder.Semiterm.val_bShift {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (a : M) (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val s (a :> e) ε (LO.FirstOrder.Rew.bShift t) = LO.FirstOrder.Semiterm.val s e ε t

theorem LO.FirstOrder.Semiterm.val_bShift' {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {ε : ξ → M} (e : Fin (n + 1) → M) (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Rew.bShift t) = LO.FirstOrder.Semiterm.val s (fun (x : Fin n) => e x.succ) ε t

@[simp]

theorem LO.FirstOrder.Semiterm.val_emb {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} {o : Type v'} [i : IsEmpty o] (t : LO.FirstOrder.Semiterm L o n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Rew.emb t) = LO.FirstOrder.Semiterm.val s e (fun (a : o) => i.elim a) t

@[simp]

theorem LO.FirstOrder.Semiterm.val_castLE {n₁ : ℕ} {n₂ : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ε : ξ → M} (h : n₁ ≤ n₂) (t : LO.FirstOrder.Semiterm L ξ n₁) : LO.FirstOrder.Semiterm.val s e₂ ε ((LO.FirstOrder.Rew.castLE h) t) = LO.FirstOrder.Semiterm.val s (fun (x : Fin n₁) => e₂ (Fin.castLE h x)) ε t

theorem LO.FirstOrder.Semiterm.val_embSubsts {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L ξ n) (t : LO.FirstOrder.Semiterm L Empty k) : LO.FirstOrder.Semiterm.val s e ε ((LO.FirstOrder.Rew.embSubsts w) t) = LO.FirstOrder.Semiterm.valb s (fun (x : Fin k) => LO.FirstOrder.Semiterm.val s e ε (w x)) t

@[simp]

theorem LO.FirstOrder.Semiterm.val_toS {n : ℕ} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} (t : LO.FirstOrder.Semiterm L (Fin n) 0) : LO.FirstOrder.Semiterm.valb s e (LO.FirstOrder.Rew.toS t) = LO.FirstOrder.Semiterm.val s ![] e t

@[simp]

theorem LO.FirstOrder.Semiterm.val_toF {n : ℕ} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} (t : LO.FirstOrder.Semiterm L Empty n) : LO.FirstOrder.Semiterm.val s ![] e (LO.FirstOrder.Rew.toF t) = LO.FirstOrder.Semiterm.valb s e t

theorem LO.FirstOrder.Semiterm.val_lMap {n : ℕ} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} (φ : L₁.Hom L₂) (s₂ : LO.FirstOrder.Structure L₂ M) (e : Fin n → M) (ε : ξ → M) {t : LO.FirstOrder.Semiterm L₁ ξ n} : LO.FirstOrder.Semiterm.val s₂ e ε (LO.FirstOrder.Semiterm.lMap φ t) = LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.lMap φ s₂) e ε t

theorem LO.FirstOrder.Semiterm.val_shift {n : ℕ} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} (ε : ℕ → M) (t : LO.FirstOrder.SyntacticSemiterm L n) : LO.FirstOrder.Semiterm.val s e ε (LO.FirstOrder.Rew.shift t) = LO.FirstOrder.Semiterm.val s e (ε ∘ Nat.succ) t

theorem LO.FirstOrder.Semiterm.val_free {n : ℕ} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} (ε : ℕ → M) (a : M) (t : LO.FirstOrder.SyntacticSemiterm L (n + 1)) : LO.FirstOrder.Semiterm.val s e (a :>ₙ ε) (LO.FirstOrder.Rew.free t) = LO.FirstOrder.Semiterm.val s (e <: a) ε t

theorem LO.FirstOrder.Semiterm.val_fix {n : ℕ} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} (ε : ℕ → M) (a : M) (t : LO.FirstOrder.SyntacticSemiterm L n) : LO.FirstOrder.Semiterm.val s (e <: a) ε (LO.FirstOrder.Rew.fix t) = LO.FirstOrder.Semiterm.val s e (a :>ₙ ε) t

theorem LO.FirstOrder.Semiterm.val_eq_of_funEqOn {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} {ε' : ξ → M} (t : LO.FirstOrder.Semiterm L ξ n) (h : Function.funEqOn t.fvar? ε ε') : LO.FirstOrder.Semiterm.val s e ε t = LO.FirstOrder.Semiterm.val s e ε' t

theorem LO.FirstOrder.Semiterm.val_toEmpty {n : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (t : LO.FirstOrder.Semiterm L ξ n) (h : t.fvarList = []) : LO.FirstOrder.Semiterm.val s e ε t = LO.FirstOrder.Semiterm.valb s e (t.toEmpty h)

theorem LO.FirstOrder.Structure.ofEquiv_func {M : Type u_2} {N : Type u_1} {L : LO.FirstOrder.Language} [s : LO.FirstOrder.Structure L M] (φ : M ≃ N) {k : ℕ} (f : L.Func k) (v : Fin k → N) : LO.FirstOrder.Structure.func f v = φ (LO.FirstOrder.Structure.func f (⇑φ.symm ∘ v))

theorem LO.FirstOrder.Structure.ofEquiv_val {M : Type u_2} {N : Type u_1} {L : LO.FirstOrder.Language} {ξ : Type v} [s : LO.FirstOrder.Structure L M] (φ : M ≃ N) {n : ℕ} (e : Fin n → N) (ε : ξ → N) (t : LO.FirstOrder.Semiterm L ξ n) : LO.FirstOrder.Semiterm.val (LO.FirstOrder.Structure.ofEquiv φ) e ε t = φ (LO.FirstOrder.Semiterm.val s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε) t)

def LO.FirstOrder.Semiformula.EvalAux {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} (s : LO.FirstOrder.Structure L M) (ε : ξ → M) {n : ℕ} : (Fin n → M) → LO.FirstOrder.Semiformula L ξ n → Prop

Equations

• LO.FirstOrder.Semiformula.EvalAux s ε x LO.FirstOrder.Semiformula.verum = True
• LO.FirstOrder.Semiformula.EvalAux s ε x LO.FirstOrder.Semiformula.falsum = False
• LO.FirstOrder.Semiformula.EvalAux s ε x (LO.FirstOrder.Semiformula.rel p v) = LO.FirstOrder.Structure.rel p fun (i : Fin arity) => LO.FirstOrder.Semiterm.val s x ε (v i)
• LO.FirstOrder.Semiformula.EvalAux s ε x (LO.FirstOrder.Semiformula.nrel p v) = ¬LO.FirstOrder.Structure.rel p fun (i : Fin arity) => LO.FirstOrder.Semiterm.val s x ε (v i)
• LO.FirstOrder.Semiformula.EvalAux s ε x (p.and q) = (LO.FirstOrder.Semiformula.EvalAux s ε x p ∧ LO.FirstOrder.Semiformula.EvalAux s ε x q)
• LO.FirstOrder.Semiformula.EvalAux s ε x (p.or q) = (LO.FirstOrder.Semiformula.EvalAux s ε x p ∨ LO.FirstOrder.Semiformula.EvalAux s ε x q)
• LO.FirstOrder.Semiformula.EvalAux s ε x p.all = ∀ (x_1 : M), LO.FirstOrder.Semiformula.EvalAux s ε (x_1 :> x) p
• LO.FirstOrder.Semiformula.EvalAux s ε x p.ex = ∃ (x_1 : M), LO.FirstOrder.Semiformula.EvalAux s ε (x_1 :> x) p

@[simp]

theorem LO.FirstOrder.Semiformula.EvalAux_neg {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} (p : LO.FirstOrder.Semiformula L ξ n) : LO.FirstOrder.Semiformula.EvalAux s ε e (∼p) = ¬LO.FirstOrder.Semiformula.EvalAux s ε e p

def LO.FirstOrder.Semiformula.Eval {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {n : ℕ} (s : LO.FirstOrder.Structure L M) (e : Fin n → M) (ε : ξ → M) : LO.FirstOrder.Semiformula L ξ n →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Eval s e ε = { toTr := LO.FirstOrder.Semiformula.EvalAux s ε e, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalm {L : LO.FirstOrder.Language} {ξ : Type v} (M : Type w) [s : LO.FirstOrder.Structure L M] {n : ℕ} (e : Fin n → M) (ε : ξ → M) : LO.FirstOrder.Semiformula L ξ n →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Evalm M e ε = LO.FirstOrder.Semiformula.Eval s e ε

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalf {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} (s : LO.FirstOrder.Structure L M) (ε : ξ → M) : LO.FirstOrder.Formula L ξ →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Evalf s ε = LO.FirstOrder.Semiformula.Eval s ![] ε

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalb {L : LO.FirstOrder.Language} {M : Type w} {n : ℕ} (s : LO.FirstOrder.Structure L M) (e : Fin n → M) : LO.FirstOrder.Semisentence L n →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Evalb s e = LO.FirstOrder.Semiformula.Eval s e Empty.elim

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalfm {L : LO.FirstOrder.Language} {ξ : Type v} (M : Type w) [s : LO.FirstOrder.Structure L M] (ε : ξ → M) : LO.FirstOrder.Formula L ξ →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Evalfm M ε = LO.FirstOrder.Semiformula.Evalf s ε

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalbm {L : LO.FirstOrder.Language} {n : ℕ} (M : Type w) [s : LO.FirstOrder.Structure L M] (e : Fin n → M) : LO.FirstOrder.Semiformula L Empty n →ˡᶜ Prop

Equations

• M ⊧/e = LO.FirstOrder.Semiformula.Evalb s e

def LO.FirstOrder.Semiformula.«term_⊧/_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Realize {L : LO.FirstOrder.Language} {M : Type w} (s : LO.FirstOrder.Structure L M) : LO.FirstOrder.Formula L M →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Realize s = LO.FirstOrder.Semiformula.Eval s ![] id

theorem LO.FirstOrder.Semiformula.eval_rel {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.rel r v) ↔ LO.FirstOrder.Structure.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.val s e ε (v i)

theorem LO.FirstOrder.Semiformula.Eval.of_eq {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {e' : Fin n → M} {ε : ξ → M} {ε' : ξ → M} {p : LO.FirstOrder.Semiformula L ξ n} (h : (LO.FirstOrder.Semiformula.Eval s e ε) p) (he : e = e') (hε : ε = ε') : (LO.FirstOrder.Semiformula.Eval s e' ε') p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_rel₀ {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 0} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.rel r ![]) ↔ LO.FirstOrder.Structure.rel r ![]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_rel₁ {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 1} (t : LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.rel r ![t]) ↔ LO.FirstOrder.Structure.rel r ![LO.FirstOrder.Semiterm.val s e ε t]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_rel₂ {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 2} (t₁ : LO.FirstOrder.Semiterm L ξ n) (t₂ : LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.rel r ![t₁, t₂]) ↔ LO.FirstOrder.Structure.rel r ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂]

theorem LO.FirstOrder.Semiformula.eval_nrel {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {k : ℕ} {r : L.Rel k} {v : Fin k → LO.FirstOrder.Semiterm L ξ n} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.nrel r v) ↔ ¬LO.FirstOrder.Structure.rel r fun (i : Fin k) => LO.FirstOrder.Semiterm.val s e ε (v i)

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nrel₀ {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 0} : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.nrel r ![]) ↔ ¬LO.FirstOrder.Structure.rel r ![]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nrel₁ {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 1} (t : LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.nrel r ![t]) ↔ ¬LO.FirstOrder.Structure.rel r ![LO.FirstOrder.Semiterm.val s e ε t]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nrel₂ {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 2} (t₁ : LO.FirstOrder.Semiterm L ξ n) (t₂ : LO.FirstOrder.Semiterm L ξ n) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Semiformula.nrel r ![t₁, t₂]) ↔ ¬LO.FirstOrder.Structure.rel r ![LO.FirstOrder.Semiterm.val s e ε t₁, LO.FirstOrder.Semiterm.val s e ε t₂]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_all {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∀' p) ↔ ∀ (x : M), (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_ex {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∃' p) ↔ ∃ (x : M), (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_ball {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {q : LO.FirstOrder.Semiformula L ξ (n + 1)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∀[p] q) ↔ ∀ (x : M), (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p → (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) q

@[simp]

theorem LO.FirstOrder.Semiformula.eval_bex {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {q : LO.FirstOrder.Semiformula L ξ (n + 1)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∃[p] q) ↔ ∃ (x : M), (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) p ⋏ (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) q

@[simp]

theorem LO.FirstOrder.Semiformula.eval_univClosure {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {ε : ξ → M} {n' : ℕ} {e' : Fin 0 → M} {p : LO.FirstOrder.Semiformula L ξ n'} : (LO.FirstOrder.Semiformula.Eval s e' ε) (∀* p) ↔ ∀ (e : Fin n' → M), (LO.FirstOrder.Semiformula.Eval s e ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_exClosure {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {ε : ξ → M} {n' : ℕ} {e' : Fin 0 → M} {p : LO.FirstOrder.Semiformula L ξ n'} : (LO.FirstOrder.Semiformula.Eval s e' ε) (∃* p) ↔ ∃ (e : Fin n' → M), (LO.FirstOrder.Semiformula.Eval s e ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_univItr {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {ε : ξ → M} {k : ℕ} {e : Fin n → M} {p : LO.FirstOrder.Semiformula L ξ (n + k)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∀^[k] p) ↔ ∀ (e' : Fin k → M), (LO.FirstOrder.Semiformula.Eval s (Matrix.appendr e' e) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_exItr {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {ε : ξ → M} {k : ℕ} {e : Fin n → M} {p : LO.FirstOrder.Semiformula L ξ (n + k)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∃^[k] p) ↔ ∃ (e' : Fin k → M), (LO.FirstOrder.Semiformula.Eval s (Matrix.appendr e' e) ε) p

theorem LO.FirstOrder.Semiformula.eval_rew {n₂ : ℕ} {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ε₂ : μ₂ → M} {n₁ : ℕ} (ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂) (p : LO.FirstOrder.Semiformula L μ₁ n₁) : (LO.FirstOrder.Semiformula.Eval s e₂ ε₂) (ω.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s (LO.FirstOrder.Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.bvar) (LO.FirstOrder.Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.fvar)) p

theorem LO.FirstOrder.Semiformula.eval_rew_q {n₂ : ℕ} {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {n₁ : ℕ} {x : M} {e₂ : Fin n₂ → M} {ε₂ : μ₂ → M} (ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂) (p : LO.FirstOrder.Semiformula L μ₁ (n₁ + 1)) : (LO.FirstOrder.Semiformula.Eval s (x :> e₂) ε₂) (ω.q.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s (x :> LO.FirstOrder.Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.bvar) (LO.FirstOrder.Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ LO.FirstOrder.Semiterm.fvar)) p

theorem LO.FirstOrder.Semiformula.eval_map {n₂ : ℕ} {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {n₁ : ℕ} (b : Fin n₁ → Fin n₂) (f : μ₁ → μ₂) (e : Fin n₂ → M) (ε : μ₂ → M) (p : LO.FirstOrder.Semiformula L μ₁ n₁) : (LO.FirstOrder.Semiformula.Eval s e ε) ((LO.FirstOrder.Rew.map b f).hom p) ↔ (LO.FirstOrder.Semiformula.Eval s (e ∘ b) (ε ∘ f)) p

theorem LO.FirstOrder.Semiformula.eval_rewrite {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε₂ : μ₂ → M} (f : μ₁ → LO.FirstOrder.Semiterm L μ₂ n) (p : LO.FirstOrder.Semiformula L μ₁ n) : (LO.FirstOrder.Semiformula.Eval s e ε₂) ((LO.FirstOrder.Rew.rewrite f).hom p) ↔ (LO.FirstOrder.Semiformula.Eval s e fun (x : μ₁) => LO.FirstOrder.Semiterm.val s e ε₂ (f x)) p

theorem LO.FirstOrder.Semiformula.eval_rewriteMap {L : LO.FirstOrder.Language} {μ₁ : Type v₁} {μ₂ : Type v₂} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε₂ : μ₂ → M} (f : μ₁ → μ₂) (p : LO.FirstOrder.Semiformula L μ₁ n) : (LO.FirstOrder.Semiformula.Eval s e ε₂) ((LO.FirstOrder.Rew.rewriteMap f).hom p) ↔ (LO.FirstOrder.Semiformula.Eval s e fun (x : μ₁) => ε₂ (f x)) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_castLE {n₂ : ℕ} {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ε : ξ → M} {n₁ : ℕ} (h : n₁ ≤ n₂) (p : LO.FirstOrder.Semiformula L ξ n₁) : (LO.FirstOrder.Semiformula.Eval s e₂ ε) ((LO.FirstOrder.Rew.castLE h).hom p) ↔ (LO.FirstOrder.Semiformula.Eval s (fun (x : Fin n₁) => e₂ (Fin.castLE h x)) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_bShift {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {x : M} (p : LO.FirstOrder.Semiformula L ξ n) : (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) (LO.FirstOrder.Rew.bShift.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s e ε) p

theorem LO.FirstOrder.Semiformula.eval_bShift' {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {ε : ξ → M} {e' : Fin (n + 1) → M} (p : LO.FirstOrder.Semiformula L ξ n) : (LO.FirstOrder.Semiformula.Eval s e' ε) (LO.FirstOrder.Rew.bShift.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s (fun (x : Fin n) => e' x.succ) ε) p

theorem LO.FirstOrder.Semiformula.eval_substs {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L ξ n) (p : LO.FirstOrder.Semiformula L ξ k) : (LO.FirstOrder.Semiformula.Eval s e ε) ((LO.FirstOrder.Rew.substs w).hom p) ↔ (LO.FirstOrder.Semiformula.Eval s (fun (i : Fin k) => LO.FirstOrder.Semiterm.val s e ε (w i)) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_emb {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} (p : LO.FirstOrder.Semiformula L Empty n) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Rew.emb.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s e Empty.elim) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_empty {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {o : Type u_1} [h : IsEmpty o] (p : LO.FirstOrder.Formula L o) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Rew.empty.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s ![] fun (a : o) => h.elim a) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_toS {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : Empty → M} (p : LO.FirstOrder.Formula L (Fin n)) : (LO.FirstOrder.Semiformula.Eval s e ε) (LO.FirstOrder.Rew.toS.hom p) ↔ (LO.FirstOrder.Semiformula.Eval s ![] e) p

theorem LO.FirstOrder.Semiformula.eval_embSubsts {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L ξ n) (σ : LO.FirstOrder.Semisentence L k) : (LO.FirstOrder.Semiformula.Eval s e ε) ((LO.FirstOrder.Rew.embSubsts w).hom σ) ↔ (LO.FirstOrder.Semiformula.Evalb s fun (x : Fin k) => LO.FirstOrder.Semiterm.val s e ε (w x)) σ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_free {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} (ε : ℕ → M) {a : M} (p : LO.FirstOrder.SyntacticSemiformula L (n + 1)) : (LO.FirstOrder.Semiformula.Eval s e (a :>ₙ ε)) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.free) p) ↔ (LO.FirstOrder.Semiformula.Eval s (e <: a) ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.eval_shift {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} (ε : ℕ → M) {a : M} (p : LO.FirstOrder.SyntacticSemiformula L n) : (LO.FirstOrder.Semiformula.Eval s e (a :>ₙ ε)) ((LO.FirstOrder.Rew.hom LO.FirstOrder.Rew.shift) p) ↔ (LO.FirstOrder.Semiformula.Eval s e ε) p

theorem LO.FirstOrder.Semiformula.eval_iff_of_funEqOn {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {ε' : ξ → M} (p : LO.FirstOrder.Semiformula L ξ n) (h : Function.funEqOn p.fvar? ε ε') : (LO.FirstOrder.Semiformula.Eval s e ε) p ↔ (LO.FirstOrder.Semiformula.Eval s e ε') p

theorem LO.FirstOrder.Semiformula.val_fvUnivClosure_inhabited {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} [h : Nonempty ξ] [DecidableEq ξ] {p : LO.FirstOrder.Formula L ξ} : (LO.FirstOrder.Semiformula.Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : ξ → M), (LO.FirstOrder.Semiformula.Evalf s ε) p

@[simp]

theorem LO.FirstOrder.Semiformula.val_fvUnivClosure {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} [Nonempty M] [DecidableEq ξ] {p : LO.FirstOrder.Formula L ξ} : (LO.FirstOrder.Semiformula.Evalf s Empty.elim) (∀ᶠ* p) ↔ ∀ (ε : ξ → M), (LO.FirstOrder.Semiformula.Evalf s ε) p

theorem LO.FirstOrder.Semiformula.eval_toEmpty {L : LO.FirstOrder.Language} {ξ : Type v} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {f : ξ → M} {p : LO.FirstOrder.Semiformula L ξ n} (hp : p.fvarList = []) : (LO.FirstOrder.Semiformula.Eval s e f) p ↔ (LO.FirstOrder.Semiformula.Evalb s e) (p.toEmpty hp)

theorem LO.FirstOrder.Semiformula.eval_close {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {ε : ℕ → M} (p : LO.FirstOrder.SyntacticFormula L) : (LO.FirstOrder.Semiformula.Evalf s ε) (LO.FirstOrder.Semiformula.close p) ↔ ∀ (f : ℕ → M), (LO.FirstOrder.Semiformula.Evalf s f) p

theorem LO.FirstOrder.Semiformula.eval_close₀ {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} [Nonempty M] (p : LO.FirstOrder.SyntacticFormula L) : (LO.FirstOrder.Semiformula.Evalb s ![]) (LO.FirstOrder.Semiformula.close₀ p) ↔ ∀ (f : ℕ → M), (LO.FirstOrder.Semiformula.Evalf s f) p

theorem LO.FirstOrder.Structure.ofEquiv_rel {M : Type u_2} {N : Type u_1} {L : LO.FirstOrder.Language} [s : LO.FirstOrder.Structure L M] (φ : M ≃ N) {k : ℕ} (r : L.Rel k) (v : Fin k → N) : LO.FirstOrder.Structure.rel r v ↔ LO.FirstOrder.Structure.rel r (⇑φ.symm ∘ v)

theorem LO.FirstOrder.Structure.eval_ofEquiv_iff {M : Type u_2} {N : Type u_1} {L : LO.FirstOrder.Language} {ξ : Type v} [s : LO.FirstOrder.Structure L M] (φ : M ≃ N) {n : ℕ} {e : Fin n → N} {ε : ξ → N} {p : LO.FirstOrder.Semiformula L ξ n} : (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.ofEquiv φ) e ε) p ↔ (LO.FirstOrder.Semiformula.Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p

theorem LO.FirstOrder.Structure.evalf_ofEquiv_iff {M : Type u_2} {N : Type u_1} {L : LO.FirstOrder.Language} {ξ : Type v} [s : LO.FirstOrder.Structure L M] (φ : M ≃ N) {ε : ξ → N} {p : LO.FirstOrder.Formula L ξ} : (LO.FirstOrder.Semiformula.Evalf (LO.FirstOrder.Structure.ofEquiv φ) ε) p ↔ (LO.FirstOrder.Semiformula.Evalf s (⇑φ.symm ∘ ε)) p

instance LO.FirstOrder.instSemanticsSyntacticFormulaStruc {L : LO.FirstOrder.Language} : LO.Semantics (LO.FirstOrder.SyntacticFormula L) (LO.FirstOrder.Struc L)

Equations

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

instance LO.FirstOrder.instTopStrucSyntacticFormula {L : LO.FirstOrder.Language} : LO.Semantics.Top (LO.FirstOrder.Struc L)

Equations

• LO.FirstOrder.instTopStrucSyntacticFormula = { realize_top := ⋯ }

instance LO.FirstOrder.instBotStrucSyntacticFormula {L : LO.FirstOrder.Language} : LO.Semantics.Bot (LO.FirstOrder.Struc L)

Equations

• LO.FirstOrder.instBotStrucSyntacticFormula = { realize_bot := ⋯ }

instance LO.FirstOrder.instAndStrucSyntacticFormula {L : LO.FirstOrder.Language} : LO.Semantics.And (LO.FirstOrder.Struc L)

Equations

• LO.FirstOrder.instAndStrucSyntacticFormula = { realize_and := ⋯ }

@[reducible, inline]

abbrev LO.FirstOrder.Models {L : LO.FirstOrder.Language} (M : Type u_1) [Nonempty M] [s : LO.FirstOrder.Structure L M] : LO.FirstOrder.SyntacticFormula L → Prop

Equations

• LO.FirstOrder.Models M = LO.Semantics.Realize s.toStruc

def LO.FirstOrder.«term_⊧ₘ_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊧ₘ_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊧ₘ_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ₘ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Models₀ {L : LO.FirstOrder.Language} (M : Type u_1) [Nonempty M] [s : LO.FirstOrder.Structure L M] (σ : LO.FirstOrder.Sentence L) : Prop

Equations

• (M ⊧ₘ₀ σ) = (M ⊧ₘ LO.FirstOrder.Rew.emb.hom σ)

def LO.FirstOrder.«term_⊧ₘ₀_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊧ₘ₀_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊧ₘ₀_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ₘ₀ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.ModelsTheory {L : LO.FirstOrder.Language} (M : Type u_1) [Nonempty M] [s : LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) : Prop

Equations

• (M ⊧ₘ* T) = (s.toStruc ⊧* T)

def LO.FirstOrder.«term_⊧ₘ*_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊧ₘ*_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊧ₘ*_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ₘ* ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Realize {L : LO.FirstOrder.Language} (M : Type u_2) [s : LO.FirstOrder.Structure L M] : LO.FirstOrder.Formula L M → Prop

Equations

• LO.FirstOrder.Realize M = ⇑(LO.FirstOrder.Semiformula.Evalf s id)

def LO.FirstOrder.«term_⊧ₘᵣ_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊧ₘᵣ_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊧ₘᵣ_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊧ₘᵣ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Consequence {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) (p : LO.FirstOrder.SyntacticFormula L) : Prop

Equations

• (T ⊨ p) = T ⊨[LO.FirstOrder.SmallStruc L] p

def LO.FirstOrder.«term_⊨_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⊨_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.term_⊨_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ ") (Lean.ParserDescr.cat `term 46))

@[reducible, inline]

abbrev LO.FirstOrder.Satisfiable {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : Prop

Equations

• LO.FirstOrder.Satisfiable T = LO.Semantics.Satisfiable (LO.FirstOrder.SmallStruc L) T

def LO.FirstOrder.modelsTheory_iff_modelsTheory_s {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {T : LO.FirstOrder.Theory L} : M ⊧ₘ* T ↔ s.toStruc ⊧* T

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.models_def {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {p : LO.FirstOrder.SyntacticFormula L} : (M ⊧ₘ p) = ∀ (f : ℕ → M), (LO.FirstOrder.Semiformula.Evalf s f) p

theorem LO.FirstOrder.models_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {p : LO.FirstOrder.SyntacticFormula L} : M ⊧ₘ p ↔ ∀ (f : ℕ → M), (LO.FirstOrder.Semiformula.Evalf s f) p

theorem LO.FirstOrder.models₀_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {σ : LO.FirstOrder.Sentence L} : M ⊧ₘ₀ σ ↔ (LO.FirstOrder.Semiformula.Evalb s ![]) σ

theorem LO.FirstOrder.models_iff₀ {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {p : LO.FirstOrder.SyntacticFormula L} : M ⊧ₘ p ↔ (LO.FirstOrder.Semiformula.Evalb s ![]) (LO.FirstOrder.Semiformula.close₀ p)

theorem LO.FirstOrder.modelsTheory_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {T : LO.FirstOrder.Theory L} : M ⊧ₘ* T ↔ ∀ {p : LO.FirstOrder.SyntacticFormula L}, p ∈ T → M ⊧ₘ p

theorem LO.FirstOrder.Theory.models {L : LO.FirstOrder.Language} (M : Type u_1) [Nonempty M] [s : LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) [M ⊧ₘ* T] {p : LO.FirstOrder.SyntacticFormula L} (hp : p ∈ T) : M ⊧ₘ p

theorem LO.FirstOrder.models_iff_models {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [s : LO.FirstOrder.Structure L M] {p : LO.FirstOrder.SyntacticFormula L} : M ⊧ₘ p ↔ s.toStruc ⊧ p

theorem LO.FirstOrder.consequence_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} : T ⊨[LO.FirstOrder.Struc L] p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M], M ⊧ₘ* T → M ⊧ₘ p

theorem LO.FirstOrder.consequence_iff' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} : T ⊨[LO.FirstOrder.Struc L] p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : M ⊧ₘ* T], M ⊧ₘ p

theorem LO.FirstOrder.valid_iff {L : LO.FirstOrder.Language} {p : LO.FirstOrder.SyntacticFormula L} : LO.Semantics.Valid (LO.FirstOrder.Struc L) p ↔ ∀ (M : Type v) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M], M ⊧ₘ p

theorem LO.FirstOrder.satisfiable_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T ↔ ∃ (M : Type v) (x : Nonempty M) (x_1 : LO.FirstOrder.Structure L M), M ⊧ₘ* T

theorem LO.FirstOrder.unsatisfiable_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : ¬LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T ↔ ∀ (M : Type v) (x : Nonempty M) (x_1 : LO.FirstOrder.Structure L M), ¬M ⊧ₘ* T

theorem LO.FirstOrder.satisfiable_intro {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (M : Type v) [Nonempty M] [s : LO.FirstOrder.Structure L M] (h : M ⊧ₘ* T) : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T

noncomputable def LO.FirstOrder.ModelOfSat {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (h : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) : Type v

Equations

• LO.FirstOrder.ModelOfSat h = Classical.choose ⋯

noncomputable instance LO.FirstOrder.nonemptyModelOfSat {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (h : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) : Nonempty (LO.FirstOrder.ModelOfSat h)

Equations

• ⋯ = ⋯

noncomputable def LO.FirstOrder.StructureModelOfSatAux {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (h : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) : { s : LO.FirstOrder.Structure L (LO.FirstOrder.ModelOfSat h) // LO.FirstOrder.ModelOfSat h ⊧ₘ* T }

Equations

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

noncomputable instance LO.FirstOrder.StructureModelOfSat {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (h : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) : LO.FirstOrder.Structure L (LO.FirstOrder.ModelOfSat h)

Equations

• LO.FirstOrder.StructureModelOfSat h = ↑(LO.FirstOrder.StructureModelOfSatAux h)

theorem LO.FirstOrder.ModelOfSat.models {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (h : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T) : LO.FirstOrder.ModelOfSat h ⊧ₘ* T

theorem LO.FirstOrder.consequence_iff_unsatisfiable {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} : T ⊨[LO.FirstOrder.Struc L] p ↔ ¬LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) (insert (∼LO.FirstOrder.Semiformula.close p) T)

theorem LO.FirstOrder.Semiformula.eval_lMap {ξ : Type v} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {M : Type u} {s₂ : LO.FirstOrder.Structure L₂ M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {p : LO.FirstOrder.Semiformula L₁ ξ n} : (LO.FirstOrder.Semiformula.Eval s₂ e ε) ((LO.FirstOrder.Semiformula.lMap Φ) p) ↔ (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.lMap Φ s₂) e ε) p

theorem LO.FirstOrder.Semiformula.models_lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {M : Type u} [Nonempty M] {s₂ : LO.FirstOrder.Structure L₂ M} {p : LO.FirstOrder.SyntacticFormula L₁} : s₂.toStruc ⊧ (LO.FirstOrder.Semiformula.lMap Φ) p ↔ (LO.FirstOrder.Structure.lMap Φ s₂).toStruc ⊧ p

theorem LO.FirstOrder.lMap_models_lMap {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {T : LO.FirstOrder.Theory L₁} {p : LO.FirstOrder.SyntacticFormula L₁} (h : T ⊨[LO.FirstOrder.Struc L₁] p) : LO.FirstOrder.Theory.lMap Φ T ⊨[LO.FirstOrder.Struc L₂] (LO.FirstOrder.Semiformula.lMap Φ) p

theorem LO.FirstOrder.ModelsTheory.models {L : LO.FirstOrder.Language} (M : Type u_1) [Nonempty M] [LO.FirstOrder.Structure L M] {T : LO.FirstOrder.Theory L} [M ⊧ₘ* T] {p : LO.FirstOrder.SyntacticFormula L} (h : p ∈ T) : M ⊧ₘ p

theorem LO.FirstOrder.ModelsTheory.of_ss {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.Theory L} (h : M ⊧ₘ* U) (ss : T ⊆ U) : M ⊧ₘ* T

@[simp]

theorem LO.FirstOrder.ModelsTheory.add_iff {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.Theory L} : M ⊧ₘ* T + U ↔ M ⊧ₘ* T ∧ M ⊧ₘ* U

instance LO.FirstOrder.ModelsTheory.add {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) [M ⊧ₘ* T] [M ⊧ₘ* U] : M ⊧ₘ* T + U

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Theory.modelsTheory_onTheory₁ {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {Φ : L₁.Hom L₂} {M : Type u} [Nonempty M] [s₂ : LO.FirstOrder.Structure L₂ M] {T₁ : LO.FirstOrder.Theory L₁} : M ⊧ₘ* LO.FirstOrder.Theory.lMap Φ T₁ ↔ M ⊧ₘ* T₁

@[reducible, inline]

abbrev LO.FirstOrder.Structure.theory (L : LO.FirstOrder.Language) (M : Type u) [Nonempty M] [s : LO.FirstOrder.Structure L M] : LO.FirstOrder.Theory L

Equations

• LO.FirstOrder.Structure.theory L M = LO.Semantics.theory s.toStruc

@[simp]

theorem LO.FirstOrder.Structure.mem_theory_iff {L : LO.FirstOrder.Language} {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {σ : LO.FirstOrder.SyntacticFormula L} : σ ∈ LO.FirstOrder.Structure.theory L M ↔ M ⊧ₘ σ

theorem LO.FirstOrder.Structure.subset_of_models {L : LO.FirstOrder.Language} {M : Type u} [Nonempty M] [LO.FirstOrder.Structure L M] {T : LO.FirstOrder.Theory L} : T ⊆ LO.FirstOrder.Structure.theory L M ↔ M ⊧ₘ* T