Semantics of first-order logic

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

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

theorem LO.FirstOrder.Structure.ext {L : LO.FirstOrder.Language} {M : Type w} {x 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

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

@[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.instCoeSortStrucType {L : LO.FirstOrder.Language} : CoeSort (LO.FirstOrder.Struc L) (Type u_1)

Equations

• LO.FirstOrder.instCoeSortStrucType = { coe := LO.FirstOrder.Struc.Dom }

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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 {ξ : Type u_1} {L : LO.FirstOrder.Language} (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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} (f : L.Func 2) (t 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₂ : ℕ} {μ₁ : Type u_1} {μ₂ : Type u_2} {L : LO.FirstOrder.Language} {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 : ℕ} {μ₁ : Type u_2} {μ₂ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {μ₁ : Type u_1} {μ₂ : Type u_2} {L : LO.FirstOrder.Language} {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₂ : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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₂ : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_3} {L₁ : LO.FirstOrder.Language} {L₂ : LO.FirstOrder.Language} {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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε ε' : ξ → M} [DecidableEq ξ] (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 : ℕ} {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e : Fin n → M} {ε : ξ → M} [DecidableEq ξ] (t : LO.FirstOrder.Semiterm L ξ n) (h : t.freeVariables = ∅) : 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_3} {N : Type u_2} {L : LO.FirstOrder.Language} [s : LO.FirstOrder.Structure L M] (Θ : M ≃ N) {n : ℕ} {ξ : Type u_1} (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 {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 φ v) = LO.FirstOrder.Structure.rel φ fun (i : Fin arity) => LO.FirstOrder.Semiterm.val s x ε (v i)
• LO.FirstOrder.Semiformula.EvalAux s ε x (LO.FirstOrder.Semiformula.nrel φ v) = ¬LO.FirstOrder.Structure.rel φ fun (i : Fin arity) => LO.FirstOrder.Semiterm.val s x ε (v i)
• LO.FirstOrder.Semiformula.EvalAux s ε x (φ.and ψ) = (LO.FirstOrder.Semiformula.EvalAux s ε x φ ∧ LO.FirstOrder.Semiformula.EvalAux s ε x ψ)
• LO.FirstOrder.Semiformula.EvalAux s ε x (φ.or ψ) = (LO.FirstOrder.Semiformula.EvalAux s ε x φ ∨ LO.FirstOrder.Semiformula.EvalAux s ε x ψ)
• LO.FirstOrder.Semiformula.EvalAux s ε x φ.all = ∀ (x_1 : M), LO.FirstOrder.Semiformula.EvalAux s ε (x_1 :> x) φ
• LO.FirstOrder.Semiformula.EvalAux s ε x φ.ex = ∃ (x_1 : M), LO.FirstOrder.Semiformula.EvalAux s ε (x_1 :> x) φ

@[simp]

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

def LO.FirstOrder.Semiformula.Eval {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 {ξ : Type u_1} {L : LO.FirstOrder.Language} (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 {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 {ξ : Type u_1} {L : LO.FirstOrder.Language} (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 {ξ : Type u_1} {L : LO.FirstOrder.Language} {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 {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e e' : Fin n → M} {ε ε' : ξ → M} {φ : LO.FirstOrder.Semiformula L ξ n} (h : (LO.FirstOrder.Semiformula.Eval s e ε) φ) (he : e = e') (hε : ε = ε') : (LO.FirstOrder.Semiformula.Eval s e' ε') φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_rel₀ {ξ : Type u_1} {L : LO.FirstOrder.Language} {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₁ {ξ : Type u_1} {L : LO.FirstOrder.Language} {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₂ {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 2} (t₁ 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 {ξ : Type u_1} {L : LO.FirstOrder.Language} {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₀ {ξ : Type u_1} {L : LO.FirstOrder.Language} {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₁ {ξ : Type u_1} {L : LO.FirstOrder.Language} {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₂ {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {r : L.Rel 2} (t₁ 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 {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : (LO.FirstOrder.Semiformula.Eval s e ε) (∀' φ) ↔ ∀ (x : M), (LO.FirstOrder.Semiformula.Eval s (x :> e) ε) φ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.FirstOrder.Semiformula.eval_rew {n₂ : ℕ} {ξ₂ : Type u_2} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ε₂ : ξ₂ → M} {ξ₁ : Type u_1} {n₁ : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (φ : LO.FirstOrder.Semiformula L ξ₁ n₁) : (LO.FirstOrder.Semiformula.Eval s e₂ ε₂) ((LO.FirstOrder.Rewriting.app ω) φ) ↔ (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)) φ

theorem LO.FirstOrder.Semiformula.eval_rew_q {n₂ : ℕ} {ξ₂ : Type u_2} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {e₂ : Fin n₂ → M} {ξ₁ : Type u_1} {n₁ : ℕ} {x : M} {ε₂ : ξ₂ → M} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) (φ : LO.FirstOrder.Semiformula L ξ₁ (n₁ + 1)) : (LO.FirstOrder.Semiformula.Eval s (x :> e₂) ε₂) ((LO.FirstOrder.Rewriting.app ω.q) φ) ↔ (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)) φ

theorem LO.FirstOrder.Semiformula.eval_map {n₂ : ℕ} {ξ₂ : Type u_2} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n₁ : ℕ} {ξ₁ : Type u_1} (b : Fin n₁ → Fin n₂) (f : ξ₁ → ξ₂) (e : Fin n₂ → M) (ε : ξ₂ → M) (φ : LO.FirstOrder.Semiformula L ξ₁ n₁) : (LO.FirstOrder.Semiformula.Eval s e ε) ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.map b f)) φ) ↔ (LO.FirstOrder.Semiformula.Eval s (e ∘ b) (ε ∘ f)) φ

theorem LO.FirstOrder.Semiformula.eval_rewrite {ξ₂ : Type u_2} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε₂ : ξ₂ → M} {ξ₁ : Type u_1} (f : ξ₁ → LO.FirstOrder.Semiterm L ξ₂ n) (φ : LO.FirstOrder.Semiformula L ξ₁ n) : (LO.FirstOrder.Semiformula.Eval s e ε₂) ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewrite f)) φ) ↔ (LO.FirstOrder.Semiformula.Eval s e fun (x : ξ₁) => LO.FirstOrder.Semiterm.val s e ε₂ (f x)) φ

theorem LO.FirstOrder.Semiformula.eval_rewriteMap {ξ₂ : Type u_2} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε₂ : ξ₂ → M} {ξ₁ : Type u_1} (f : ξ₁ → ξ₂) (φ : LO.FirstOrder.Semiformula L ξ₁ n) : (LO.FirstOrder.Semiformula.Eval s e ε₂) ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.rewriteMap f)) φ) ↔ (LO.FirstOrder.Semiformula.Eval s e fun (x : ξ₁) => ε₂ (f x)) φ

@[simp]

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

@[simp]

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

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

theorem LO.FirstOrder.Semiformula.eval_substs {ξ : Type u_1} {L : LO.FirstOrder.Language} {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.Semiformula L ξ k) : (LO.FirstOrder.Semiformula.Eval s e ε) (φ ⇜ w) ↔ (LO.FirstOrder.Semiformula.Eval s (fun (i : Fin k) => LO.FirstOrder.Semiterm.val s e ε (w i)) ε) φ

@[simp]

theorem LO.FirstOrder.Semiformula.eval_emb {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε : ξ → M} (φ : LO.FirstOrder.Semiformula L Empty n) : (LO.FirstOrder.Semiformula.Eval s e ε) ↑φ ↔ (LO.FirstOrder.Semiformula.Eval s e Empty.elim) φ

@[simp]

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

@[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} (φ : LO.FirstOrder.Formula L (Fin n)) : (LO.FirstOrder.Semiformula.Eval s e ε) ((LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.toS) φ) ↔ (LO.FirstOrder.Semiformula.Eval s ![] e) φ

theorem LO.FirstOrder.Semiformula.eval_embSubsts {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ξ : Type u_1} {ε : ξ → M} {k : ℕ} (w : Fin k → LO.FirstOrder.Semiterm L ξ n) (σ : LO.FirstOrder.Semisentence L k) : (LO.FirstOrder.Semiformula.Eval s e ε) ((LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.embSubsts w)) σ) ↔ (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} (φ : LO.FirstOrder.SyntacticSemiformula L (n + 1)) : (LO.FirstOrder.Semiformula.Eval s e (a :>ₙ ε)) ((LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.free) φ) ↔ (LO.FirstOrder.Semiformula.Eval s (e <: a) ε) φ

@[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} (φ : LO.FirstOrder.SyntacticSemiformula L n) : (LO.FirstOrder.Semiformula.Eval s e (a :>ₙ ε)) ((LO.FirstOrder.Rewriting.app LO.FirstOrder.Rew.shift) φ) ↔ (LO.FirstOrder.Semiformula.Eval s e ε) φ

theorem LO.FirstOrder.Semiformula.eval_iff_of_funEqOn {ξ : Type u_1} {L : LO.FirstOrder.Language} {M : Type w} {s : LO.FirstOrder.Structure L M} {n : ℕ} {e : Fin n → M} {ε ε' : ξ → M} [DecidableEq ξ] (φ : LO.FirstOrder.Semiformula L ξ n) (h : Function.funEqOn φ.FVar? ε ε') : (LO.FirstOrder.Semiformula.Eval s e ε) φ ↔ (LO.FirstOrder.Semiformula.Eval s e ε') φ

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

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

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

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_3} {N : Type u_2} {L : LO.FirstOrder.Language} [s : LO.FirstOrder.Structure L M] (Θ : M ≃ N) {ξ : Type u_1} {n : ℕ} {e : Fin n → N} {ε : ξ → N} {φ : LO.FirstOrder.Semiformula L ξ n} : (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.ofEquiv Θ) e ε) φ ↔ (LO.FirstOrder.Semiformula.Eval s (⇑Θ.symm ∘ e) (⇑Θ.symm ∘ ε)) φ

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

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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[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 ⊧ₘ ↑σ)

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) (φ : LO.FirstOrder.SyntacticFormula L) : Prop

Equations

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

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] {φ : LO.FirstOrder.SyntacticFormula L} : (M ⊧ₘ φ) = ∀ (f : ℕ → M), (LO.FirstOrder.Semiformula.Evalf s f) φ

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

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] {φ : LO.FirstOrder.SyntacticFormula L} : M ⊧ₘ φ ↔ (LO.FirstOrder.Semiformula.Evalb s ![]) (LO.FirstOrder.Semiformula.close₀ φ)

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 ↔ ∀ {φ : LO.FirstOrder.SyntacticFormula L}, φ ∈ T → M ⊧ₘ φ

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] {φ : LO.FirstOrder.SyntacticFormula L} (hp : φ ∈ T) : M ⊧ₘ φ

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

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

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

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

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} {φ : LO.FirstOrder.SyntacticFormula L} : T ⊨[LO.FirstOrder.Struc L] φ ↔ ¬LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) (insert (∼LO.FirstOrder.Semiformula.close φ) T)

theorem LO.FirstOrder.Semiformula.eval_lMap {ξ : Type u_1} {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} [Nonempty M] {φ : LO.FirstOrder.Semiformula L₁ ξ n} : (LO.FirstOrder.Semiformula.Eval s₂ e ε) ((LO.FirstOrder.Semiformula.lMap Φ) φ) ↔ (LO.FirstOrder.Semiformula.Eval (LO.FirstOrder.Structure.lMap Φ s₂) e ε) φ

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

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

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] {φ : LO.FirstOrder.SyntacticFormula L} (h : φ ∈ T) : M ⊧ₘ φ

theorem LO.FirstOrder.ModelsTheory.of_ss {L : LO.FirstOrder.Language} {M : Type u_1} [Nonempty M] [LO.FirstOrder.Structure L M] {T 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 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 U : LO.FirstOrder.Theory L) [M ⊧ₘ* T] [M ⊧ₘ* U] : M ⊧ₘ* T + U

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Theory.modelsTheory_onTheory₁ {L₁ 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