mathlib3 documentation

model_theory.semantics

Basics on First-Order Semantics #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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:

@[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
@[simp]
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} :
@[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} :
@[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} :
@[simp]
@[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) :
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
@[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} :
@[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
@[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)) :
@[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} :
@[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
@[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
@[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
@[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)} :
@[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
@[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
@[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)
@[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)
@[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)
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} :
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) :
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) :
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} :
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))
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) :
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
@[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} :
@[simp]
theorem first_order.language.bounded_formula.realize_relabel_equiv {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {g : α β} {k : } {φ : L.bounded_formula α k} {v : β M} {xs : fin k M} :
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
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
@[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
@[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
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
@[simp]
theorem first_order.language.formula.realize_not {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {φ : L.formula α} {v : α M} :
@[simp]
@[simp]
theorem first_order.language.formula.realize_top {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α M} :
@[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
@[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
@[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 α} :
@[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
@[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)
@[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} :
@[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} :
@[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

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

Equations
@[simp]

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

Equations
Instances for first_order.language.complete_theory

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

Equations
@[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 φ
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 φ
@[simp]
@[protected, instance]
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
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'
@[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'
@[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
@[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
@[simp]
@[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
@[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
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 φ
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
@[protected, instance]