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:

@[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_relabel {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.term α} {g : α → β} {v : β → M} :
@[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} :
@[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} :
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]
@[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} :
@[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) :
@[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]
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) :
@[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 kL.term fin l)} :
@[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)} :
@[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)} :
@[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 nL'.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 nL'.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) :
@[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} :
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} :
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} :
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]
theorem first_order.language.formula.realize_bot {L : first_order.language} {M : Type w} [L.Structure M] {α : Type u'} {v : α → M} :
@[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 kL.term α} :
@[simp]
@[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 α} :
@[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
@[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 α) :
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
@[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 ψ

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

Equations
Instances for first_order.language.complete_theory
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
@[simp]
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 φ
@[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), φ TM φ
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]
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
@[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'
theorem first_order.language.Theory.model_singleton_iff {L : first_order.language} {M : Type w} [L.Structure M] {φ : L.sentence} :
M {φ} M φ
@[protected, instance]
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 φ
@[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]
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) :
@[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
@[simp]
@[protected, instance]
@[protected, instance]
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