mathlib documentation

model_theory.semantics

Basics on First-Order Semantics #

This file defines the interpretations of first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.

Main Definitions #

Main Results #

Implementation Notes #

References #

For the Flypitch project:

source
@[simp]
def first_order.language.term.realize {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} (v : α → M) (t : L.term α) :
M

A term t with variables indexed by α can be evaluated by giving a value to each variable.

Equations
source
@[simp]
theorem first_order.language.term.realize_relabel {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.term α} {g : α → β} {v : β → M} :
first_order.language.term.realize v (first_order.language.term.relabel g t) = first_order.language.term.realize (v ∘ g) t
source
@[simp]
theorem first_order.language.term.realize_lift_at {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : ℕ} {t : L.term (α ⊕ fin n)} {v : α ⊕ fin (n + n') → M} :
first_order.language.term.realize v (first_order.language.term.lift_at n' m t) = first_order.language.term.realize (v ∘ sum.map id (λ (i : fin n), ite (↑i < m) (⇑(fin.cast_add n') i) (⇑(fin.add_nat n') i))) t
source
@[simp]
theorem first_order.language.term.realize_constants {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {c : L.constants} {v : α → M} :
first_order.language.term.realize v c.term = ↑c
source
@[simp]
theorem first_order.language.term.realize_functions_apply₁ {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {f : L.functions 1} {t : L.term α} {v : α → M} :
first_order.language.term.realize v (f.apply₁ t) = first_order.language.Structure.fun_map f ![first_order.language.term.realize v t]
source
@[simp]
theorem first_order.language.term.realize_functions_apply₂ {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {f : L.functions 2} {t₁ t₂ : L.term α} {v : α → M} :
first_order.language.term.realize v (f.apply₂ t₁ t₂) = first_order.language.Structure.fun_map f ![first_order.language.term.realize v t₁, first_order.language.term.realize v t₂]
source
theorem first_order.language.term.realize_con {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {A : set M} {a : ↥A} {v : α → M} :
first_order.language.term.realize v (L.con a).term = ↑a
source
@[simp]
theorem first_order.language.term.realize_subst {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.term α} {tf : α → L.term β} {v : β → M} :
first_order.language.term.realize v (t.subst tf) = first_order.language.term.realize (λ (a : α), first_order.language.term.realize v (tf a)) t
source
@[simp]
theorem first_order.language.term.realize_restrict_var {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [decidable_eq α] {t : L.term α} {s : set α} (h : ↑(t.var_finset) ⊆ s) {v : α → M} :
first_order.language.term.realize (v ∘ coe) (t.restrict_var (set.inclusion h)) = first_order.language.term.realize v t
source
@[simp]
theorem first_order.language.term.realize_restrict_var_left {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [decidable_eq α] {γ : Type u_1} {t : L.term (α ⊕ γ)} {s : set α} (h : ↑(t.var_finset_left) ⊆ s) {v : α → M} {xs : γ → M} :
first_order.language.term.realize (sum.elim (v ∘ coe) xs) (t.restrict_var_left (set.inclusion h)) = first_order.language.term.realize (sum.elim v xs) t
source
@[simp]
theorem first_order.language.term.realize_constants_to_vars {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [(L.Lhom_with_constants α).is_expansion_on M] {t : (L.with_constants α).term β} {v : β → M} :
first_order.language.term.realize (sum.elim (λ (a : α), ↑(L.con a)) v) t.constants_to_vars = first_order.language.term.realize v t
source
@[simp]
theorem first_order.language.term.realize_vars_to_constants {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [(L.Lhom_with_constants α).is_expansion_on M] {t : L.term (α ⊕ β)} {v : β → M} :
first_order.language.term.realize v t.vars_to_constants = first_order.language.term.realize (sum.elim (λ (a : α), ↑(L.con a)) v) t
source
theorem first_order.language.term.realize_constants_vars_equiv_left {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [(L.Lhom_with_constants α).is_expansion_on M] {n : ℕ} {t : (L.with_constants α).term (β ⊕ fin n)} {v : β → M} {xs : fin n → M} :
first_order.language.term.realize (sum.elim (sum.elim (λ (a : α), ↑(L.con a)) v) xs) (⇑first_order.language.term.constants_vars_equiv_left t) = first_order.language.term.realize (sum.elim v xs) t
source
@[simp]
theorem first_order.language.Lhom.realize_on_term {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] (t : L.term α) (v : α → M) :
first_order.language.term.realize v (φ.on_term t) = first_order.language.term.realize v t
source
@[simp]
theorem first_order.language.hom.realize_term {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {α : Type u'} (g : L.hom M N) {t : L.term α} {v : α → M} :
first_order.language.term.realize (⇑g ∘ v) t = ⇑g (first_order.language.term.realize v t)
source
@[simp]
theorem first_order.language.embedding.realize_term {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {α : Type u'} {v : α → M} (t : L.term α) (g : L.embedding M N) :
first_order.language.term.realize (⇑g ∘ v) t = ⇑g (first_order.language.term.realize v t)
source
@[simp]
theorem first_order.language.equiv.realize_term {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {α : Type u'} {v : α → M} (t : L.term α) (g : L.equiv M N) :
first_order.language.term.realize (⇑g ∘ v) t = ⇑g (first_order.language.term.realize v t)
source
def first_order.language.bounded_formula.realize {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} (f : L.bounded_formula α l) (v : α → M) (xs : fin l → M) :
Prop

A bounded formula can be evaluated as true or false by giving values to each free variable.

Equations
source
@[simp]
theorem first_order.language.bounded_formula.realize_bot {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : fin l → M} :
⊥.realize v xs ↔ false
source
@[simp]
theorem first_order.language.bounded_formula.realize_not {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ : L.bounded_formula α l} {v : α → M} {xs : fin l → M} :
φ.not.realize v xs ↔ ¬φ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_bd_equal {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : fin l → M} (t₁ t₂ : L.term (α ⊕ fin l)) :
(t₁.bd_equal t₂).realize v xs ↔ first_order.language.term.realize (sum.elim v xs) t₁ = first_order.language.term.realize (sum.elim v xs) t₂
source
@[simp]
theorem first_order.language.bounded_formula.realize_top {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : fin l → M} :
⊤.realize v xs ↔ true
source
@[simp]
theorem first_order.language.bounded_formula.realize_inf {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.bounded_formula α l} {v : α → M} {xs : fin l → M} :
(φ ⊓ ψ).realize v xs ↔ φ.realize v xs ∧ ψ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_foldr_inf {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (l : list (L.bounded_formula α n)) (v : α → M) (xs : fin n → M) :
(list.foldr has_inf.inf ⊤ l).realize v xs ↔ ∀ (φ : L.bounded_formula α n), φ ∈ l → φ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_imp {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.bounded_formula α l} {v : α → M} {xs : fin l → M} :
(φ.imp ψ).realize v xs ↔ φ.realize v xs → ψ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_rel {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : fin l → M} {k : ℕ} {R : L.relations k} {ts : fin k → L.term (α ⊕ fin l)} :
(R.bounded_formula ts).realize v xs ↔ first_order.language.Structure.rel_map R (λ (i : fin k), first_order.language.term.realize (sum.elim v xs) (ts i))
source
@[simp]
theorem first_order.language.bounded_formula.realize_rel₁ {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : fin l → M} {R : L.relations 1} {t : L.term (α ⊕ fin l)} :
(R.bounded_formula₁ t).realize v xs ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize (sum.elim v xs) t]
source
@[simp]
theorem first_order.language.bounded_formula.realize_rel₂ {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : fin l → M} {R : L.relations 2} {t₁ t₂ : L.term (α ⊕ fin l)} :
(R.bounded_formula₂ t₁ t₂).realize v xs ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize (sum.elim v xs) t₁, first_order.language.term.realize (sum.elim v xs) t₂]
source
@[simp]
theorem first_order.language.bounded_formula.realize_sup {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.bounded_formula α l} {v : α → M} {xs : fin l → M} :
(φ ⊔ ψ).realize v xs ↔ φ.realize v xs ∨ ψ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_foldr_sup {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (l : list (L.bounded_formula α n)) (v : α → M) (xs : fin n → M) :
(list.foldr has_sup.sup ⊥ l).realize v xs ↔ ∃ (φ : L.bounded_formula α n) (H : φ ∈ l), φ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_all {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {θ : L.bounded_formula α l.succ} {v : α → M} {xs : fin l → M} :
θ.all.realize v xs ↔ ∀ (a : M), θ.realize v (fin.snoc xs a)
source
@[simp]
theorem first_order.language.bounded_formula.realize_ex {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {θ : L.bounded_formula α l.succ} {v : α → M} {xs : fin l → M} :
θ.ex.realize v xs ↔ ∃ (a : M), θ.realize v (fin.snoc xs a)
source
@[simp]
theorem first_order.language.bounded_formula.realize_iff {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.bounded_formula α l} {v : α → M} {xs : fin l → M} :
(φ.iff ψ).realize v xs ↔ (φ.realize v xs ↔ ψ.realize v xs)
source
theorem first_order.language.bounded_formula.realize_cast_le_of_eq {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {m n : ℕ} (h : m = n) {h' : m ≤ n} {φ : L.bounded_formula α m} {v : α → M} {xs : fin n → M} :
(first_order.language.bounded_formula.cast_le h' φ).realize v xs ↔ φ.realize v (xs ∘ ⇑(fin.cast h))
source
theorem first_order.language.bounded_formula.realize_map_term_rel_id {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [L'.Structure M] {ft : Π (n : ℕ), L.term (α ⊕ fin n) → L'.term (β ⊕ fin n)} {fr : Π (n : ℕ), L.relations n → L'.relations n} {n : ℕ} {φ : L.bounded_formula α n} {v : α → M} {v' : β → M} {xs : fin n → M} (h1 : ∀ (n : ℕ) (t : L.term (α ⊕ fin n)) (xs : fin n → M), first_order.language.term.realize (sum.elim v' xs) (ft n t) = first_order.language.term.realize (sum.elim v xs) t) (h2 : ∀ (n : ℕ) (R : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map (fr n R) x = first_order.language.Structure.rel_map R x) :
(first_order.language.bounded_formula.map_term_rel ft fr (λ (_x : ℕ), id) φ).realize v' xs ↔ φ.realize v xs
source
theorem first_order.language.bounded_formula.realize_map_term_rel_add_cast_le {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [L'.Structure M] {k : ℕ} {ft : Π (n : ℕ), L.term (α ⊕ fin n) → L'.term (β ⊕ fin (k + n))} {fr : Π (n : ℕ), L.relations n → L'.relations n} {n : ℕ} {φ : L.bounded_formula α n} (v : Π {n : ℕ}, (fin (k + n) → M) → α → M) {v' : β → M} (xs : fin (k + n) → M) (h1 : ∀ (n : ℕ) (t : L.term (α ⊕ fin n)) (xs' : fin (k + n) → M), first_order.language.term.realize (sum.elim v' xs') (ft n t) = first_order.language.term.realize (sum.elim (v xs') (xs' ∘ ⇑(fin.nat_add k))) t) (h2 : ∀ (n : ℕ) (R : L.relations n) (x : fin n → M), first_order.language.Structure.rel_map (fr n R) x = first_order.language.Structure.rel_map R x) (hv : ∀ (n : ℕ) (xs : fin (k + n) → M) (x : M), v (fin.snoc xs x) = v xs) :
(first_order.language.bounded_formula.map_term_rel ft fr (λ (n : ℕ), first_order.language.bounded_formula.cast_le _) φ).realize v' xs ↔ φ.realize (v xs) (xs ∘ ⇑(fin.nat_add k))
source
theorem first_order.language.bounded_formula.realize_relabel {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {m n : ℕ} {φ : L.bounded_formula α n} {g : α → β ⊕ fin m} {v : β → M} {xs : fin (m + n) → M} :
(first_order.language.bounded_formula.relabel g φ).realize v xs ↔ φ.realize (sum.elim v (xs ∘ ⇑(fin.cast_add n)) ∘ g) (xs ∘ ⇑(fin.nat_add m))
source
theorem first_order.language.bounded_formula.realize_lift_at {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : ℕ} {φ : L.bounded_formula α n} {v : α → M} {xs : fin (n + n') → M} (hmn : m + n' ≤ n + 1) :
(first_order.language.bounded_formula.lift_at n' m φ).realize v xs ↔ φ.realize v (xs ∘ λ (i : fin n), ite (↑i < m) (⇑(fin.cast_add n') i) (⇑(fin.add_nat n') i))
source
theorem first_order.language.bounded_formula.realize_lift_at_one {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n m : ℕ} {φ : L.bounded_formula α n} {v : α → M} {xs : fin (n + 1) → M} (hmn : m ≤ n) :
(first_order.language.bounded_formula.lift_at 1 m φ).realize v xs ↔ φ.realize v (xs ∘ λ (i : fin n), ite (↑i < m) (⇑fin.cast_succ i) i.succ)
source
@[simp]
theorem first_order.language.bounded_formula.realize_lift_at_one_self {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} {v : α → M} {xs : fin (n + 1) → M} :
(first_order.language.bounded_formula.lift_at 1 n φ).realize v xs ↔ φ.realize v (xs ∘ ⇑fin.cast_succ)
source
theorem first_order.language.bounded_formula.realize_subst {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} {φ : L.bounded_formula α n} {tf : α → L.term β} {v : β → M} {xs : fin n → M} :
(φ.subst tf).realize v xs ↔ φ.realize (λ (a : α), first_order.language.term.realize v (tf a)) xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_restrict_free_var {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [decidable_eq α] {n : ℕ} {φ : L.bounded_formula α n} {s : set α} (h : ↑(φ.free_var_finset) ⊆ s) {v : α → M} {xs : fin n → M} :
(φ.restrict_free_var (set.inclusion h)).realize (v ∘ coe) xs ↔ φ.realize v xs
source
theorem first_order.language.bounded_formula.realize_constants_vars_equiv {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.with_constants α).Structure M] [(L.Lhom_with_constants α).is_expansion_on M] {n : ℕ} {φ : (L.with_constants α).bounded_formula β n} {v : β → M} {xs : fin n → M} :
(⇑first_order.language.bounded_formula.constants_vars_equiv φ).realize (sum.elim (λ (a : α), ↑(L.con a)) v) xs ↔ φ.realize v xs
source
theorem first_order.language.bounded_formula.realize_all_lift_at_one_self {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [nonempty M] {n : ℕ} {φ : L.bounded_formula α n} {v : α → M} {xs : fin n → M} :
(first_order.language.bounded_formula.lift_at 1 n φ).all.realize v xs ↔ φ.realize v xs
source
theorem first_order.language.bounded_formula.realize_to_prenex_imp_right {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [nonempty M] {φ ψ : L.bounded_formula α n} (hφ : φ.is_qf) (hψ : ψ.is_prenex) {v : α → M} {xs : fin n → M} :
(φ.to_prenex_imp_right ψ).realize v xs ↔ (φ.imp ψ).realize v xs
source
theorem first_order.language.bounded_formula.realize_to_prenex_imp {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [nonempty M] {φ ψ : L.bounded_formula α n} (hφ : φ.is_prenex) (hψ : ψ.is_prenex) {v : α → M} {xs : fin n → M} :
(φ.to_prenex_imp ψ).realize v xs ↔ (φ.imp ψ).realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_to_prenex {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} [nonempty M] (φ : L.bounded_formula α n) {v : α → M} {xs : fin n → M} :
φ.to_prenex.realize v xs ↔ φ.realize v xs
source
@[simp]
theorem first_order.language.Lhom.realize_on_bounded_formula {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] {n : ℕ} (ψ : L.bounded_formula α n) {v : α → M} {xs : fin n → M} :
(φ.on_bounded_formula ψ).realize v xs ↔ ψ.realize v xs
source
def first_order.language.formula.realize {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} (φ : L.formula α) (v : α → M) :
Prop

A formula can be evaluated as true or false by giving values to each free variable.

Equations
source
@[simp]
theorem first_order.language.formula.realize_not {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ : L.formula α} {v : α → M} :
φ.not.realize v ↔ ¬φ.realize v
source
@[simp]
theorem first_order.language.formula.realize_bot {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} :
⊥.realize v ↔ false
source
@[simp]
theorem first_order.language.formula.realize_top {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} :
⊤.realize v ↔ true
source
@[simp]
theorem first_order.language.formula.realize_inf {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α → M} :
(φ ⊓ ψ).realize v ↔ φ.realize v ∧ ψ.realize v
source
@[simp]
theorem first_order.language.formula.realize_imp {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α → M} :
(φ.imp ψ).realize v ↔ φ.realize v → ψ.realize v
source
@[simp]
theorem first_order.language.formula.realize_rel {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {k : ℕ} {R : L.relations k} {ts : fin k → L.term α} :
(R.formula ts).realize v ↔ first_order.language.Structure.rel_map R (λ (i : fin k), first_order.language.term.realize v (ts i))
source
@[simp]
theorem first_order.language.formula.realize_rel₁ {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {R : L.relations 1} {t : L.term α} :
(R.formula₁ t).realize v ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize v t]
source
@[simp]
theorem first_order.language.formula.realize_rel₂ {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} {R : L.relations 2} {t₁ t₂ : L.term α} :
(R.formula₂ t₁ t₂).realize v ↔ first_order.language.Structure.rel_map R ![first_order.language.term.realize v t₁, first_order.language.term.realize v t₂]
source
@[simp]
theorem first_order.language.formula.realize_sup {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α → M} :
(φ ⊔ ψ).realize v ↔ φ.realize v ∨ ψ.realize v
source
@[simp]
theorem first_order.language.formula.realize_iff {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.formula α} {v : α → M} :
(φ.iff ψ).realize v ↔ (φ.realize v ↔ ψ.realize v)
source
@[simp]
theorem first_order.language.formula.realize_relabel {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {φ : L.formula α} {g : α → β} {v : β → M} :
(first_order.language.formula.relabel g φ).realize v ↔ φ.realize (v ∘ g)
source
theorem first_order.language.formula.realize_relabel_sum_inr {L : first_order.language} {M : Type w} [L.Structure M] {n : ℕ} (φ : L.formula (fin n)) {v : empty → M} {x : fin n → M} :
(first_order.language.bounded_formula.relabel sum.inr φ).realize v x ↔ φ.realize x
source
@[simp]
theorem first_order.language.formula.realize_equal {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {t₁ t₂ : L.term α} {x : α → M} :
(t₁.equal t₂).realize x ↔ first_order.language.term.realize x t₁ = first_order.language.term.realize x t₂
source
@[simp]
theorem first_order.language.formula.realize_graph {L : first_order.language} {M : Type w} [L.Structure M] {n : ℕ} {f : L.functions n} {x : fin n → M} {y : M} :
(first_order.language.formula.graph f).realize (fin.cons y x) ↔ first_order.language.Structure.fun_map f x = y
source
@[simp]
theorem first_order.language.Lhom.realize_on_formula {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] (ψ : L.formula α) {v : α → M} :
(φ.on_formula ψ).realize v ↔ ψ.realize v
source
@[simp]
theorem first_order.language.Lhom.set_of_realize_on_formula {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] (ψ : L.formula α) :
set_of (φ.on_formula ψ).realize = set_of ψ.realize
source
def first_order.language.sentence.realize {L : first_order.language} (M : Type w) [L.Structure M] (φ : L.sentence) :
Prop

A sentence can be evaluated as true or false in a structure.

Equations
source
@[simp]
theorem first_order.language.sentence.realize_not {L : first_order.language} (M : Type w) [L.Structure M] {φ : L.sentence} :
M ⊨ first_order.language.formula.not φ ↔ ¬M ⊨ φ
source
@[simp]
theorem first_order.language.Lhom.realize_on_sentence {L : first_order.language} {L' : first_order.language} (M : Type w) [L.Structure M] [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] (ψ : L.sentence) :
M ⊨ φ.on_sentence ψ ↔ M ⊨ ψ
source
def first_order.language.complete_theory (L : first_order.language) (M : Type w) [L.Structure M] :
L.Theory

The complete theory of a structure M is the set of all sentences M satisfies.

Equations
Instances for first_order.language.complete_theory
source
def first_order.language.elementarily_equivalent (L : first_order.language) (M : Type w) (N : Type u_3) [L.Structure M] [L.Structure N] :
Prop

Two structures are elementarily equivalent when they satisfy the same sentences.

Equations
source
@[simp]
theorem first_order.language.mem_complete_theory {L : first_order.language} {M : Type w} [L.Structure M] {φ : L.sentence} :
φ ∈ L.complete_theory M ↔ M ⊨ φ
source
theorem first_order.language.elementarily_equivalent_iff {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] :
L.elementarily_equivalent M N ↔ ∀ (φ : L.sentence), M ⊨ φ ↔ N ⊨ φ
source
@[class]
structure first_order.language.Theory.model {L : first_order.language} (M : Type w) [L.Structure M] (T : L.Theory) :
Prop

A model of a theory is a structure in which every sentence is realized as true.

Instances of this typeclass
source
@[simp]
theorem first_order.language.Theory.model_iff {L : first_order.language} {M : Type w} [L.Structure M] (T : L.Theory) :
M ⊨ T ↔ ∀ (φ : L.sentence), φ ∈ T → M ⊨ φ
source
theorem first_order.language.Theory.realize_sentence_of_mem {L : first_order.language} {M : Type w} [L.Structure M] (T : L.Theory) [M ⊨ T] {φ : L.sentence} (h : φ ∈ T) :
M ⊨ φ
source
@[simp]
theorem first_order.language.Lhom.on_Theory_model {L : first_order.language} {L' : first_order.language} {M : Type w} [L.Structure M] [L'.Structure M] (φ : L →ᴸ L') [φ.is_expansion_on M] (T : L.Theory) :
M ⊨ φ.on_Theory T ↔ M ⊨ T
source
@[protected, instance]
def first_order.language.model_empty {L : first_order.language} {M : Type w} [L.Structure M] :
M ⊨ ∅
source
theorem first_order.language.Theory.model.mono {L : first_order.language} {M : Type w} [L.Structure M] {T T' : L.Theory} (h : M ⊨ T') (hs : T ⊆ T') :
M ⊨ T
source
theorem first_order.language.Theory.model.union {L : first_order.language} {M : Type w} [L.Structure M] {T T' : L.Theory} (h : M ⊨ T) (h' : M ⊨ T') :
M ⊨ T ∪ T'
source
@[simp]
theorem first_order.language.Theory.model_union_iff {L : first_order.language} {M : Type w} [L.Structure M] {T T' : L.Theory} :
M ⊨ T ∪ T' ↔ M ⊨ T ∧ M ⊨ T'
source
theorem first_order.language.Theory.model_singleton_iff {L : first_order.language} {M : Type w} [L.Structure M] {φ : L.sentence} :
M ⊨ {φ} ↔ M ⊨ φ
source
theorem first_order.language.Theory.model_iff_subset_complete_theory {L : first_order.language} {M : Type w} [L.Structure M] {T : L.Theory} :
M ⊨ T ↔ T ⊆ L.complete_theory M
source
theorem first_order.language.Theory.complete_theory.subset {L : first_order.language} {M : Type w} [L.Structure M] {T : L.Theory} [MT : M ⊨ T] :
T ⊆ L.complete_theory M
source
@[protected, instance]
def first_order.language.model_complete_theory {L : first_order.language} {M : Type w} [L.Structure M] :
M ⊨ L.complete_theory M
source
theorem first_order.language.realize_iff_of_model_complete_theory {L : first_order.language} (M : Type w) (N : Type u_3) [L.Structure M] [L.Structure N] [N ⊨ L.complete_theory M] (φ : L.sentence) :
N ⊨ φ ↔ M ⊨ φ
source
@[simp]
theorem first_order.language.bounded_formula.realize_alls {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} {v : α → M} :
φ.alls.realize v ↔ ∀ (xs : fin n → M), φ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_exs {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} {φ : L.bounded_formula α n} {v : α → M} :
φ.exs.realize v ↔ ∃ (xs : fin n → M), φ.realize v xs
source
@[simp]
theorem first_order.language.bounded_formula.realize_to_formula {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {n : ℕ} (φ : L.bounded_formula α n) (v : α ⊕ fin n → M) :
φ.to_formula.realize v ↔ φ.realize (v ∘ sum.inl) (v ∘ sum.inr)
source
@[simp]
theorem first_order.language.equiv.realize_bounded_formula {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {α : Type u'} {n : ℕ} (g : L.equiv M N) (φ : L.bounded_formula α n) {v : α → M} {xs : fin n → M} :
φ.realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.realize v xs
source
@[simp]
theorem first_order.language.equiv.realize_formula {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {α : Type u'} (g : L.equiv M N) (φ : L.formula α) {v : α → M} :
φ.realize (⇑g ∘ v) ↔ φ.realize v
source
theorem first_order.language.equiv.realize_sentence {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (g : L.equiv M N) (φ : L.sentence) :
M ⊨ φ ↔ N ⊨ φ
source
theorem first_order.language.equiv.Theory_model {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {T : L.Theory} (g : L.equiv M N) [M ⊨ T] :
N ⊨ T
source
theorem first_order.language.equiv.elementarily_equivalent {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (g : L.equiv M N) :
L.elementarily_equivalent M N
source
@[simp]
theorem first_order.language.relations.realize_reflexive {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M ⊨ r.reflexive ↔ reflexive (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
source
@[simp]
theorem first_order.language.relations.realize_irreflexive {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M ⊨ r.irreflexive ↔ irreflexive (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
source
@[simp]
theorem first_order.language.relations.realize_symmetric {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M ⊨ r.symmetric ↔ symmetric (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
source
@[simp]
theorem first_order.language.relations.realize_antisymmetric {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M ⊨ r.antisymmetric ↔ anti_symmetric (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
source
@[simp]
theorem first_order.language.relations.realize_transitive {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M ⊨ r.transitive ↔ transitive (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
source
@[simp]
theorem first_order.language.relations.realize_total {L : first_order.language} {M : Type w} [L.Structure M] {r : L.relations 2} :
M ⊨ r.total ↔ total (λ (x y : M), first_order.language.Structure.rel_map r ![x, y])
source
@[simp]
theorem first_order.language.sentence.realize_card_ge (L : first_order.language) {M : Type w} [L.Structure M] (n : ℕ) :
M ⊨ first_order.language.sentence.card_ge L n ↔ ↑n ≤ cardinal.mk M
source
@[simp]
theorem first_order.language.model_infinite_theory_iff (L : first_order.language) {M : Type w} [L.Structure M] :
M ⊨ L.infinite_theory ↔ infinite M
source
@[protected, instance]
def first_order.language.model_infinite_theory (L : first_order.language) {M : Type w} [L.Structure M] [h : infinite M] :
M ⊨ L.infinite_theory
source
@[simp]
theorem first_order.language.model_nonempty_theory_iff (L : first_order.language) {M : Type w} [L.Structure M] :
M ⊨ L.nonempty_theory ↔ nonempty M
source
@[protected, instance]
def first_order.language.model_nonempty (L : first_order.language) {M : Type w} [L.Structure M] [h : nonempty M] :
M ⊨ L.nonempty_theory
source
theorem first_order.language.model_distinct_constants_theory (L : first_order.language) {α : Type u'} {M : Type w} [(L.with_constants α).Structure M] (s : set α) :
M ⊨ L.distinct_constants_theory s ↔ set.inj_on (λ (i : α), ↑(L.con i)) s
source
theorem first_order.language.card_le_of_model_distinct_constants_theory (L : first_order.language) {α : Type u'} (s : set α) (M : Type w) [(L.with_constants α).Structure M] [h : M ⊨ L.distinct_constants_theory s] :
(cardinal.mk ↥s).lift ≤ (cardinal.mk M).lift
source
@[symm]
theorem first_order.language.elementarily_equivalent.symm {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (h : L.elementarily_equivalent M N) :
L.elementarily_equivalent N M
source
@[trans]
theorem first_order.language.elementarily_equivalent.trans {L : first_order.language} {M : Type w} {N : Type u_3} {P : Type u_4} [L.Structure M] [L.Structure N] [L.Structure P] (MN : L.elementarily_equivalent M N) (NP : L.elementarily_equivalent N P) :
L.elementarily_equivalent M P
source
theorem first_order.language.elementarily_equivalent.complete_theory_eq {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (h : L.elementarily_equivalent M N) :
L.complete_theory M = L.complete_theory N
source
theorem first_order.language.elementarily_equivalent.realize_sentence {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (h : L.elementarily_equivalent M N) (φ : L.sentence) :
M ⊨ φ ↔ N ⊨ φ
source
theorem first_order.language.elementarily_equivalent.Theory_model_iff {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {T : L.Theory} (h : L.elementarily_equivalent M N) :
M ⊨ T ↔ N ⊨ T
source
theorem first_order.language.elementarily_equivalent.Theory_model {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] {T : L.Theory} [MT : M ⊨ T] (h : L.elementarily_equivalent M N) :
N ⊨ T
source
theorem first_order.language.elementarily_equivalent.nonempty_iff {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (h : L.elementarily_equivalent M N) :
nonempty M ↔ nonempty N
source
theorem first_order.language.elementarily_equivalent.nonempty {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] [Mn : nonempty M] (h : L.elementarily_equivalent M N) :
nonempty N
source
theorem first_order.language.elementarily_equivalent.infinite_iff {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] (h : L.elementarily_equivalent M N) :
infinite M ↔ infinite N
source
theorem first_order.language.elementarily_equivalent.infinite {L : first_order.language} {M : Type w} {N : Type u_3} [L.Structure M] [L.Structure N] [Mi : infinite M] (h : L.elementarily_equivalent M N) :
infinite N