Model-theoretic semantics of first-order classical logic

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

class LO.FirstOrder.Structure (L : 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 : Language} {M : Type w} {x y : Structure L M} (func : func = func) (rel : rel = rel) : x = y

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

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

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

@[reducible, inline]

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

Equations

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

instance LO.FirstOrder.instCoeSortStrucType {L : Language} : CoeSort (Struc L) (Type u_1)

Equations

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

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

def LO.FirstOrder.Structure.lMap {L₁ : Language} {L₂ : Language} (φ : L₁.Hom L₂) {M : Type w} (S : Structure L₂ M) : 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₁ : Language} {L₂ : Language} (φ : L₁.Hom L₂) {M : Type w} (s₂ : Structure L₂ M) {k : ℕ} {f : L₁.Func k} {v : Fin k → M} : func f v = func (φ.func f) v

@[simp]

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

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

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Structure.Decidable (L : Language) (M : Type w) [s : 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 : Language} {M : Type w} [Structure L M] : 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 : Language} {M : Type w} [i : Nonempty M] (s : Structure L M) : Struc L

Equations

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

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

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

Equations

• s.instStructureDom = s.struc

def LO.FirstOrder.Semiterm.val {n : ℕ} {ξ : Type u_1} {L : Language} {M : Type w} (s : Structure L M) (e : Fin n → M) (ε : ξ → M) : 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 : Language} {M : Type w} (s : Structure L M) (e : Fin n → M) (t : ClosedSemiterm L 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 : Language} (M : Type w) [s : Structure L M] {n : ℕ} (e : Fin n → M) (ε : ξ → M) : 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 : Language} (M : Type w) [s : Structure L M] {n : ℕ} (e : Fin n → M) : ClosedSemiterm L n → M

Equations

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

@[reducible, inline]

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

def LO.FirstOrder.Semiformula.EvalAux {ξ : Type u_1} {L : Language} {M : Type w} (s : Structure L M) (ε : ξ → M) {n : ℕ} : (Fin n → M) → 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 : M), LO.FirstOrder.Semiformula.EvalAux s ε (x :> x✝) φ
• LO.FirstOrder.Semiformula.EvalAux s ε x✝ φ.exs = ∃ (x : M), LO.FirstOrder.Semiformula.EvalAux s ε (x :> x✝) φ

@[simp]

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

def LO.FirstOrder.Semiformula.Eval {ξ : Type u_1} {L : Language} {M : Type w} {n : ℕ} (s : Structure L M) (e : Fin n → M) (ε : ξ → M) : 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 : Language} (M : Type w) [s : Structure L M] {n : ℕ} (e : Fin n → M) (ε : ξ → M) : 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 : Language} {M : Type w} (s : Structure L M) (ε : ξ → M) : Formula L ξ →ˡᶜ Prop

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalb {L : Language} {M : Type w} {n : ℕ} (s : Structure L M) (e : Fin n → M) : 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 : Language} (M : Type w) [s : Structure L M] (ε : ξ → M) : Formula L ξ →ˡᶜ Prop

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Evalbm {L : Language} {n : ℕ} (M : Type w) [s : Structure L M] (e : Fin n → M) : 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.Models {L : Language} {M : Type w} (s : Structure L M) : Formula L M →ˡᶜ Prop

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.FirstOrder.Semiformula.eval_rew {ξ₂ : Type u_2} {L : Language} {M : Type w} {s : Structure L M} {ξ₁ : Type u_1} {n₁ n₂ : ℕ} {e₂ : Fin n₂ → M} {ε₂ : ξ₂ → M} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ n₁) : (Eval s e₂ ε₂) ((Rewriting.app ω) φ) ↔ (Eval s (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val s e₂ ε₂ ∘ ⇑ω ∘ Semiterm.fvar)) φ

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

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.eval_enumarateFVar_idxOfFVar_eq_id {L : Language} {M : Type w} {s : Structure L M} {n : ℕ} [DecidableEq M] [Inhabited M] (φ : Semiformula L M n) (v : Fin n → M) : (Evalm M v fun (x : M) => φ.enumarateFVar (φ.idxOfFVar x)) φ ↔ (Evalm M v id) φ

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

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

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

instance LO.FirstOrder.instSemanticsStrucSentence {L : Language} : Semantics (Struc L) (Sentence L)

Equations

• LO.FirstOrder.instSemanticsStrucSentence = { Models := fun (str : LO.FirstOrder.Struc L) => ⇑(LO.FirstOrder.Semiformula.Evalb str.struc ![]) }

instance LO.FirstOrder.instTarskiStrucSentence {L : Language} : Semantics.Tarski (Struc L)

@[reducible, inline]

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

Equations

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

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

Models a sentence

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 : Language} (M : Type u_1) [Nonempty M] [s : Structure L M] (T : Theory L) : Prop

Equations

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

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

Models a set of sentences

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 : Language} (T : Theory L) (σ : Sentence L) : Prop

Equations

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

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

Semantic entailment, also known as logical consequence.

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 : Language} (T : Theory L) : Prop

Equations

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

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

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.models_iff {L : Language} {M : Type u_1} [Nonempty M] [s : Structure L M] {σ : Sentence L} : M ⊧ₘ σ ↔ M ⊧/![] σ

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[reducible, inline]

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

Equations

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

@[simp]

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

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

theorem LO.FirstOrder.Structure.theory_satisfiable {L : Language} {M : Type v} [Nonempty M] [s : Structure L M] : Semantics.Satisfiable (Struc L) (theory L M)