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)

A first-order L-structure associates domain M with interpretations of function and relation symbols.

• 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)

An auxiliary structure that corresponds to a first-order L-structure with a nonempty domain.

• 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

@[implicit_reducible]

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)

@[implicit_reducible]

instance LO.FirstOrder.Structure.unit {L : Language} : Structure L Unit

Equations

• LO.FirstOrder.Structure.unit = { func := fun (x : ℕ) (x_1 : L.Func x) (x_2 : Fin x → Unit) => (), rel := fun (x : ℕ) (x_1 : L.Rel x) (x_2 : Fin x → Unit) => True }

@[reducible, inline]

abbrev 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

@[reducible, inline]

abbrev 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))

@[implicit_reducible]

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

@[implicit_reducible]

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] (b : Fin n → M) (f : ξ → M) : Semiterm L ξ n → M

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.valb {n : ℕ} {L : Language} {M : Type w} [s : Structure L M] (b : Fin n → M) (t : ClosedSemiterm L n) : M

Equations

• LO.FirstOrder.Semiterm.valb b t = LO.FirstOrder.Semiterm.val b Empty.elim t

@[reducible, inline]

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

Equations

• LO.FirstOrder.Semiterm.valf b = LO.FirstOrder.Semiterm.val b Empty.elim

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiterm.val_func {n : ℕ} {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {b : Fin n → M} {f : ξ → M} {k : ℕ} (F : L.Func k) (v : Fin k → Semiterm L ξ n) : val b f (func F v) = Structure.func F (val b f ∘ v)

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

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

theorem LO.FirstOrder.Semiterm.val_rewrite {n : ℕ} {ξ₁ : Type u_2} {ξ₂ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {b : Fin n → M} {f₂ : ξ₂ → M} (f : ξ₁ → Semiterm L ξ₂ n) (t : Semiterm L ξ₁ n) : val b f₂ ((Rew.rewrite f) t) = val b (val b f₂ ∘ f) t

theorem LO.FirstOrder.Semiterm.val_rewriteMap {n : ℕ} {ξ₁ : Type u_1} {ξ₂ : Type u_2} {L : Language} {M : Type w} {s : Structure L M} {b : Fin n → M} {f₂ : ξ₂ → M} (f : ξ₁ → ξ₂) (t : Semiterm L ξ₁ n) : val b f₂ ((Rew.rewriteMap f) t) = val b (f₂ ∘ f) t

theorem LO.FirstOrder.Semiterm.val_substs {n₁ n₂ : ℕ} {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {b₂ : Fin n₂ → M} {f : ξ → M} (w : Fin n₁ → Semiterm L ξ n₂) (t : Semiterm L ξ n₁) : val b₂ f ((Rew.subst w) t) = val (val b₂ f ∘ w) f t

@[simp]

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

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

@[simp]

theorem LO.FirstOrder.Semiterm.val_emb {n : ℕ} {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {b : Fin n → M} {f : ξ → M} {o : Type v'} [i : IsEmpty o] (t : Semiterm L o n) : val b f (Rew.emb t) = val b (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} {b₂ : Fin n₂ → M} {f : ξ → M} (h : n₁ ≤ n₂) (t : Semiterm L ξ n₁) : val b₂ f ((Rew.castLE h) t) = val (fun (x : Fin n₁) => b₂ (Fin.castLE h x)) f t

theorem LO.FirstOrder.Semiterm.val_embSubsts {n : ℕ} {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {b : Fin n → M} {f : ξ → M} {k : ℕ} (w : Fin k → Semiterm L ξ n) (t : Semiterm L Empty k) : val b f ((Rew.embSubsts w) t) = valb (val b f ∘ w) 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) (b : Fin n → M) (f : ξ → M) {t : Semiterm L₁ ξ n} : val b f (lMap φ t) = val b f t

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

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

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

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

theorem LO.FirstOrder.Semiterm.val_toEmpty {n : ℕ} {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {b : Fin n → M} {f : ξ → M} [DecidableEq ξ] (t : Semiterm L ξ n) (h : t.freeVariables = ∅) : val b f t = valb b (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} (b : Fin n → N) (f : ξ → N) (t : Semiterm L ξ n) : Semiterm.val b f t = Θ (Semiterm.val (⇑Θ.symm ∘ b) (⇑Θ.symm ∘ f) t)

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

Equations

• LO.FirstOrder.Semiformula.EvalAux s f b (LO.FirstOrder.Semiformula.rel φ v) = LO.FirstOrder.Structure.rel φ fun (i : Fin arity) => LO.FirstOrder.Semiterm.val b f (v i)
• LO.FirstOrder.Semiformula.EvalAux s f b (LO.FirstOrder.Semiformula.nrel φ v) = ¬LO.FirstOrder.Structure.rel φ fun (i : Fin arity) => LO.FirstOrder.Semiterm.val b f (v i)
• LO.FirstOrder.Semiformula.EvalAux s f b LO.FirstOrder.Semiformula.verum = True
• LO.FirstOrder.Semiformula.EvalAux s f b LO.FirstOrder.Semiformula.falsum = False
• LO.FirstOrder.Semiformula.EvalAux s f b (φ.and ψ) = (LO.FirstOrder.Semiformula.EvalAux s f b φ ∧ LO.FirstOrder.Semiformula.EvalAux s f b ψ)
• LO.FirstOrder.Semiformula.EvalAux s f b (φ.or ψ) = (LO.FirstOrder.Semiformula.EvalAux s f b φ ∨ LO.FirstOrder.Semiformula.EvalAux s f b ψ)
• LO.FirstOrder.Semiformula.EvalAux s f b φ.all = ∀ (x : M), LO.FirstOrder.Semiformula.EvalAux s f (x :> b) φ
• LO.FirstOrder.Semiformula.EvalAux s f b φ.exs = ∃ (x : M), LO.FirstOrder.Semiformula.EvalAux s f (x :> b) φ

@[simp]

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

def LO.FirstOrder.Semiformula.Eval {ξ : Type u_1} {L : Language} {M : Type w} {n : ℕ} [s : Structure L M] (b : Fin n → M) (f : ξ → M) : Semiformula L ξ n →ˡᶜ Prop

Evaluation of semiformula with variation of free-variables f and bounded-variables b

Equations

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

@[reducible, inline]

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

Equations

• LO.FirstOrder.Semiformula.Evalf f = LO.FirstOrder.Semiformula.Eval ![] f

@[reducible, inline]

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

Equations

• LO.FirstOrder.Semiformula.Evalb b = LO.FirstOrder.Semiformula.Eval b Empty.elim

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 : Language} (M : Type u_1) [s : Structure L M] : Sentence L →ˡᶜ Prop

Equations

• LO.FirstOrder.Semiformula.Realize M = LO.FirstOrder.Semiformula.Eval ![] Empty.elim

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

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

@[simp]

theorem LO.FirstOrder.Semiformula.eval_rel {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {n : ℕ} {b : Fin n → M} {f : ξ → M} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ n} : (Eval b f) (rel r v) ↔ Structure.rel r (Semiterm.val b f ∘ v)

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

@[simp]

theorem LO.FirstOrder.Semiformula.eval_nrel {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {n : ℕ} {b : Fin n → M} {f : ξ → M} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ξ n} : (Eval b f) (nrel r v) ↔ ¬Structure.rel r (Semiterm.val b f ∘ v)

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem LO.FirstOrder.Semiformula.eval_rew_q {n₂ : ℕ} {ξ₂ : Type u_2} {L : Language} {M : Type w} {s : Structure L M} {b₂ : Fin n₂ → M} {ξ₁ : Type u_1} {n₁ : ℕ} {x : M} {f₂ : ξ₂ → M} (ω : Rew L ξ₁ n₁ ξ₂ n₂) (φ : Semiformula L ξ₁ (n₁ + 1)) : (Eval (x :> b₂) f₂) ((Rewriting.app ω.q) φ) ↔ (Eval (x :> Semiterm.val b₂ f₂ ∘ ⇑ω ∘ Semiterm.bvar) (Semiterm.val b₂ f₂ ∘ ⇑ω ∘ 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} (θ : Fin n₁ → Fin n₂) (η : ξ₁ → ξ₂) (b : Fin n₂ → M) (f : ξ₂ → M) (φ : Semiformula L ξ₁ n₁) : (Eval b f) ((Rewriting.app (Rew.map θ η)) φ) ↔ (Eval (b ∘ θ) (f ∘ η)) φ

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

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem LO.FirstOrder.Semiformula.eval_substs {ξ : Type u_1} {L : Language} {M : Type w} {s : Structure L M} {n : ℕ} {b : Fin n → M} {f : ξ → M} {k : ℕ} (w : Fin k → Semiterm L ξ n) (φ : Semiformula L ξ k) : (Eval b f) (φ ⇜ w) ↔ (Eval (Semiterm.val b f ∘ w) f) φ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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 = ∅) {b : Fin n → M} : (Eval b f) φ ↔ (Evalb b) (φ.toEmpty hp)

@[simp]

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

@[simp]

theorem LO.FirstOrder.Semiformula.eval_univCl {L : Language} {M : Type w} {s : Structure L M} [Nonempty M] (φ : Proposition L) : (Realize M) (univCl φ) ↔ ∀ (f : ℕ → M), (Evalf 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) : (Eval v fun (x : M) => φ.enumarateFVar (φ.idxOfFVar x)) φ ↔ (Eval 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} {b : Fin n → N} {f : ξ → N} {φ : Semiformula L ξ n} : (Semiformula.Eval b f) φ ↔ (Semiformula.Eval (⇑Θ.symm ∘ b) (⇑Θ.symm ∘ f)) φ

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} {f : ξ → N} {φ : Formula L ξ} : (Semiformula.Evalf f) φ ↔ (Semiformula.Evalf (⇑Θ.symm ∘ f)) φ

@[implicit_reducible]

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.Realize str.Dom) }

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

@[reducible, inline]

abbrev LO.FirstOrder.Language.str (M : Type u_2) [Nonempty M] (L : Language) [s : Structure L M] : Struc L

Standard structure inferred from a given domain

Equations

• M↓[L] = s.toStruc

def LO.FirstOrder.«term_↓[_]» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Consequence {L : Language} (T : Theory L) (σ : Sentence L) : Prop

Equations

• LO.FirstOrder.Consequence 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

theorem LO.FirstOrder.struc_models_iff_models {L : Language} {σ : Sentence L} {s : Struc L} : s ⊧ σ ↔ s.Dom↓[L] ⊧ σ

theorem LO.FirstOrder.models_iff {L : Language} {M : Type u_1} [Nonempty M] [s : Structure L M] {σ : Sentence L} : M↓[L] ⊧ σ ↔ (Semiformula.Realize M) σ

theorem LO.FirstOrder.notModels_iff {L : Language} {M : Type u_1} [Nonempty M] [s : Structure L M] {σ : Sentence L} : M↓[L] ⊭ σ ↔ ¬(Semiformula.Realize M) σ

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

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

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

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

theorem LO.FirstOrder.models_iff_models {L : Language} {M : Type u_1} [Nonempty M] [s : Structure L M] {φ : Sentence L} : M↓[L] ⊧ φ ↔ 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↓[L] ⊧* T → M↓[L] ⊧ φ

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↓[L] ⊧* T], M↓[L] ⊧ φ

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↓[L] ⊧ φ

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↓[L] ⊧* 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↓[L] ⊧* T

theorem LO.FirstOrder.satisfiable_intro {L : Language} {T : Theory L} (M : Type v) [Nonempty M] [s : Structure L M] (h : M↓[L] ⊧* 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)↓[L] ⊧* T }

Equations

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

@[implicit_reducible]

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)↓[L] ⊧* 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 : ℕ} {b : Fin n → M} {f : ξ → M} [Nonempty M] {φ : Semiformula L₁ ξ n} : (Eval b f) ((lMap Φ) φ) ↔ (Eval b f) φ

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.models_of_ss {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] {T U : Theory L} (h : M↓[L] ⊧* U) (ss : T ⊆ U) : M↓[L] ⊧* T

theorem LO.FirstOrder.models_of_le {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] {T₁ T₂ : Theory L} (h : M↓[L] ⊧* T₂) (le : T₁ ⊆ T₂) : M↓[L] ⊧* T₁

instance LO.FirstOrder.models_theory_sup {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (T₁ T₂ : Theory L) [M↓[L] ⊧* T₁] [M↓[L] ⊧* T₂] : M↓[L] ⊧* T₁ ∪ T₂

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

@[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↓[L] ⊧ σ

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↓[L] ⊧* 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)