# Documentation

Mathlib.ModelTheory.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 #

• FirstOrder.Language.Term.realize is defined so that t.realize v is the term t evaluated at variables v.
• FirstOrder.Language.BoundedFormula.Realize is defined so that φ.Realize v xs is the bounded formula φ evaluated at tuples of variables v and xs.
• FirstOrder.Language.Formula.Realize is defined so that φ.Realize v is the formula φ evaluated at variables v.
• FirstOrder.Language.Sentence.Realize is defined so that φ.Realize M is the sentence φ evaluated in the structure M. Also denoted M ⊨ φ.
• FirstOrder.Language.Theory.Model is defined so that T.Model M is true if and only if every sentence of T is realized in M. Also denoted T ⊨ φ.

## Main Results #

• FirstOrder.Language.BoundedFormula.realize_toPrenex shows that the prenex normal form of a formula has the same realization as the original formula.
• Several results in this file show that syntactic constructions such as relabel, castLE, liftAt, subst, and the actions of language maps commute with realization of terms, formulas, sentences, and theories.

## Implementation Notes #

• Formulas use a modified version of de Bruijn variables. Specifically, a L.BoundedFormula α n is a formula with some variables indexed by a type α, which cannot be quantified over, and some indexed by Fin n, which can. For any φ : L.BoundedFormula α (n + 1), we define the formula ∀' φ : L.BoundedFormula α n by universally quantifying over the variable indexed by n : Fin (n + 1).

## References #

For the Flypitch project:

• [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [flypitch_cpp]
• [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]
def FirstOrder.Language.Term.realize {L : FirstOrder.Language} {M : Type w} {α : Type u'} (v : αM) (_t : ) :
M

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

Equations
Instances For
@[simp]
theorem FirstOrder.Language.Term.realize_var {L : FirstOrder.Language} {M : Type w} {α : Type u'} (v : αM) (k : α) :
@[simp]
theorem FirstOrder.Language.Term.realize_func {L : FirstOrder.Language} {M : Type w} {α : Type u'} (v : αM) {n : } (f : ) (ts : Fin n) :
@[simp]
theorem FirstOrder.Language.Term.realize_relabel {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {t : } {g : αβ} {v : βM} :
@[simp]
theorem FirstOrder.Language.Term.realize_liftAt {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } {n' : } {m : } {t : FirstOrder.Language.Term L (α Fin n)} {v : α Fin (n + n')M} :
= FirstOrder.Language.Term.realize (v Sum.map id fun i => if i < m then Fin.castAdd n' i else Fin.addNat i n') t
@[simp]
theorem FirstOrder.Language.Term.realize_constants {L : FirstOrder.Language} {M : Type w} {α : Type u'} {v : αM} :
@[simp]
theorem FirstOrder.Language.Term.realize_functions_apply₁ {L : FirstOrder.Language} {M : Type w} {α : Type u'} {f : } {t : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Term.realize_functions_apply₂ {L : FirstOrder.Language} {M : Type w} {α : Type u'} {f : } {t₁ : } {t₂ : } {v : αM} :
theorem FirstOrder.Language.Term.realize_con {L : FirstOrder.Language} {M : Type w} {α : Type u'} {A : Set M} {a : A} {v : αM} :
@[simp]
theorem FirstOrder.Language.Term.realize_subst {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {t : } {tf : α} {v : βM} :
@[simp]
theorem FirstOrder.Language.Term.realize_restrictVar {L : FirstOrder.Language} {M : Type w} {α : Type u'} [] {t : } {s : Set α} (h : ) {v : αM} :
@[simp]
theorem FirstOrder.Language.Term.realize_restrictVarLeft {L : FirstOrder.Language} {M : Type w} {α : Type u'} [] {γ : Type u_4} {t : FirstOrder.Language.Term L (α γ)} {s : Set α} (h : ) {v : αM} {xs : γM} :
@[simp]
theorem FirstOrder.Language.Term.realize_constantsToVars {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {v : βM} :
@[simp]
theorem FirstOrder.Language.Term.realize_varsToConstants {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {t : FirstOrder.Language.Term L (α β)} {v : βM} :
theorem FirstOrder.Language.Term.realize_constantsVarsEquivLeft {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {n : } {t : } {v : βM} {xs : Fin nM} :
FirstOrder.Language.Term.realize (Sum.elim (Sum.elim (fun a => ↑()) v) xs) (FirstOrder.Language.Term.constantsVarsEquivLeft t) =
@[simp]
theorem FirstOrder.Language.LHom.realize_onTerm {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} {α : Type u'} (φ : L →ᴸ L') (t : ) (v : αM) :
@[simp]
theorem FirstOrder.Language.Hom.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {α : Type u'} (g : ) {t : } {v : αM} :
= g ()
@[simp]
theorem FirstOrder.Language.Embedding.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {α : Type u'} {v : αM} (t : ) (g : ) :
= g ()
@[simp]
theorem FirstOrder.Language.Equiv.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {α : Type u'} {v : αM} (t : ) (g : ) :
= g ()
def FirstOrder.Language.BoundedFormula.Realize {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } (_f : ) (_v : αM) (_xs : Fin lM) :

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

Equations
Instances For
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_bot {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_not {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {φ : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_bdEqual {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {v : αM} {xs : Fin lM} (t₁ : FirstOrder.Language.Term L (α Fin l)) (t₂ : FirstOrder.Language.Term L (α Fin l)) :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_top {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_inf {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {φ : } {ψ : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_foldr_inf {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } (l : ) (v : αM) (xs : Fin nM) :
FirstOrder.Language.BoundedFormula.Realize (List.foldr (fun x x_1 => x x_1) l) v xs ∀ (φ : ), φ l
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_imp {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {φ : } {ψ : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_rel {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {v : αM} {xs : Fin lM} {k : } {R : } {ts : Fin kFirstOrder.Language.Term L (α Fin l)} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_rel₁ {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {v : αM} {xs : Fin lM} {R : } {t : FirstOrder.Language.Term L (α Fin l)} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_rel₂ {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {v : αM} {xs : Fin lM} {R : } {t₁ : FirstOrder.Language.Term L (α Fin l)} {t₂ : FirstOrder.Language.Term L (α Fin l)} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_sup {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {φ : } {ψ : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_foldr_sup {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } (l : ) (v : αM) (xs : Fin nM) :
FirstOrder.Language.BoundedFormula.Realize (List.foldr (fun x x_1 => x x_1) l) v xs φ, φ l
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_all {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {θ : } {v : αM} {xs : Fin lM} :
∀ (a : M),
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_ex {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {θ : } {v : αM} {xs : Fin lM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_iff {L : FirstOrder.Language} {M : Type w} {α : Type u'} {l : } {φ : } {ψ : } {v : αM} {xs : Fin lM} :
theorem FirstOrder.Language.BoundedFormula.realize_castLE_of_eq {L : FirstOrder.Language} {M : Type w} {α : Type u'} {m : } {n : } (h : m = n) {h' : m n} {φ : } {v : αM} {xs : Fin nM} :
theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_id {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {ft : (n : ) → FirstOrder.Language.Term L (α Fin n)FirstOrder.Language.Term L' (β Fin n)} {fr : (n : ) → } {n : } {φ : } {v : αM} {v' : βM} {xs : Fin nM} (h1 : ∀ (n : ) (t : FirstOrder.Language.Term L (α Fin n)) (xs : Fin nM), FirstOrder.Language.Term.realize (Sum.elim v' xs) (ft n t) = ) (h2 : ∀ (n : ) (R : ) (x : Fin nM), ) :
theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {k : } {ft : (n : ) → FirstOrder.Language.Term L (α Fin n)FirstOrder.Language.Term L' (β Fin (k + n))} {fr : (n : ) → } {n : } {φ : } (v : {n : } → (Fin (k + n)M) → αM) {v' : βM} (xs : Fin (k + n)M) (h1 : ∀ (n : ) (t : FirstOrder.Language.Term L (α Fin n)) (xs' : Fin (k + n)M), FirstOrder.Language.Term.realize (Sum.elim v' xs') (ft n t) = FirstOrder.Language.Term.realize (Sum.elim (v n xs') (xs' )) t) (h2 : ∀ (n : ) (R : ) (x : Fin nM), ) (hv : ∀ (n : ) (xs : Fin (k + n)M) (x : M), v (n + 1) (Fin.snoc xs x) = v n xs) :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_relabel {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {m : } {n : } {φ : } {g : αβ Fin m} {v : βM} {xs : Fin (m + n)M} :
theorem FirstOrder.Language.BoundedFormula.realize_liftAt {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } {n' : } {m : } {φ : } {v : αM} {xs : Fin (n + n')M} (hmn : m + n' n + 1) :
FirstOrder.Language.BoundedFormula.Realize φ v (xs fun i => if i < m then Fin.castAdd n' i else Fin.addNat i n')
theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } {m : } {φ : } {v : αM} {xs : Fin (n + 1)M} (hmn : m n) :
FirstOrder.Language.BoundedFormula.Realize φ v (xs fun i => if i < m then else )
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one_self {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } {φ : } {v : αM} {xs : Fin (n + 1)M} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_subst {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {n : } {φ : } {tf : α} {v : βM} {xs : Fin nM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar {L : FirstOrder.Language} {M : Type w} {α : Type u'} [] {n : } {φ : } {s : Set α} (h : ) {v : αM} {xs : Fin nM} :
theorem FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {n : } {v : βM} {xs : Fin nM} :
FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.BoundedFormula.constantsVarsEquiv φ) (Sum.elim (fun a => ↑()) v) xs
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_relabelEquiv {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {g : α β} {k : } {φ : } {v : βM} {xs : Fin kM} :
theorem FirstOrder.Language.BoundedFormula.realize_all_liftAt_one_self {L : FirstOrder.Language} {M : Type w} {α : Type u'} [] {n : } {φ : } {v : αM} {xs : Fin nM} :
theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } [] {φ : } {ψ : } {v : αM} {xs : Fin nM} :
theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImp {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } [] {φ : } {ψ : } {v : αM} {xs : Fin nM} :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_toPrenex {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } [] (φ : ) {v : αM} {xs : Fin nM} :
@[simp]
theorem FirstOrder.Language.LHom.realize_onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} {α : Type u'} (φ : L →ᴸ L') {n : } (ψ : ) {v : αM} {xs : Fin nM} :
def FirstOrder.Language.Formula.Realize {L : FirstOrder.Language} {M : Type w} {α : Type u'} (φ : ) (v : αM) :

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

Instances For
@[simp]
theorem FirstOrder.Language.Formula.realize_not {L : FirstOrder.Language} {M : Type w} {α : Type u'} {φ : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_bot {L : FirstOrder.Language} {M : Type w} {α : Type u'} {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_top {L : FirstOrder.Language} {M : Type w} {α : Type u'} {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_inf {L : FirstOrder.Language} {M : Type w} {α : Type u'} {φ : } {ψ : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_imp {L : FirstOrder.Language} {M : Type w} {α : Type u'} {φ : } {ψ : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_rel {L : FirstOrder.Language} {M : Type w} {α : Type u'} {v : αM} {k : } {R : } {ts : Fin k} :
@[simp]
theorem FirstOrder.Language.Formula.realize_rel₁ {L : FirstOrder.Language} {M : Type w} {α : Type u'} {v : αM} {R : } {t : } :
@[simp]
theorem FirstOrder.Language.Formula.realize_rel₂ {L : FirstOrder.Language} {M : Type w} {α : Type u'} {v : αM} {R : } {t₁ : } {t₂ : } :
@[simp]
theorem FirstOrder.Language.Formula.realize_sup {L : FirstOrder.Language} {M : Type w} {α : Type u'} {φ : } {ψ : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_iff {L : FirstOrder.Language} {M : Type w} {α : Type u'} {φ : } {ψ : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_relabel {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {φ : } {g : αβ} {v : βM} :
theorem FirstOrder.Language.Formula.realize_relabel_sum_inr {L : FirstOrder.Language} {M : Type w} {n : } (φ : ) {v : EmptyM} {x : Fin nM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_equal {L : FirstOrder.Language} {M : Type w} {α : Type u'} {t₁ : } {t₂ : } {x : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_graph {L : FirstOrder.Language} {M : Type w} {n : } {f : } {x : Fin nM} {y : M} :
@[simp]
theorem FirstOrder.Language.LHom.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} {α : Type u'} (φ : L →ᴸ L') (ψ : ) {v : αM} :
@[simp]

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

Instances For

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

Instances For
@[simp]
theorem FirstOrder.Language.Formula.realize_equivSentence_symm_con {L : FirstOrder.Language} (M : Type w) {α : Type u'} :
(FirstOrder.Language.Formula.Realize (FirstOrder.Language.Formula.equivSentence.symm φ) fun a => ↑()) M φ
@[simp]
theorem FirstOrder.Language.Formula.realize_equivSentence {L : FirstOrder.Language} (M : Type w) {α : Type u'} (φ : ) :
M FirstOrder.Language.Formula.equivSentence φ FirstOrder.Language.Formula.Realize φ fun a => ↑()
theorem FirstOrder.Language.Formula.realize_equivSentence_symm {L : FirstOrder.Language} (M : Type w) {α : Type u'} (v : αM) :
FirstOrder.Language.Formula.Realize (FirstOrder.Language.Formula.equivSentence.symm φ) v M φ
@[simp]

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

Instances For

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

Instances For

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

Instances For
@[simp]
theorem FirstOrder.Language.elementarilyEquivalent_iff {L : FirstOrder.Language} {M : Type w} {N : Type u_1} :
∀ (φ : ), M φ N φ
• realize_of_mem : ∀ (φ : ), φ TM φ

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

Instances

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

Instances For
@[simp]
theorem FirstOrder.Language.Theory.model_iff {L : FirstOrder.Language} {M : Type w} (T : ) :
M T ∀ (φ : ), φ TM φ
theorem FirstOrder.Language.Theory.realize_sentence_of_mem {L : FirstOrder.Language} {M : Type w} (T : ) [M T] {φ : } (h : φ T) :
M φ
@[simp]
theorem FirstOrder.Language.Theory.Model.mono {L : FirstOrder.Language} {M : Type w} {T : } {T' : } (_h : M T') (hs : T T') :
M T
theorem FirstOrder.Language.Theory.Model.union {L : FirstOrder.Language} {M : Type w} {T : } {T' : } (h : M T) (h' : M T') :
M T T'
@[simp]
theorem FirstOrder.Language.Theory.model_union_iff {L : FirstOrder.Language} {M : Type w} {T : } {T' : } :
M T T' M T M T'
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_alls {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } {φ : } {v : αM} :
∀ (xs : Fin nM),
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_exs {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } {φ : } {v : αM} :
@[simp]
theorem FirstOrder.Language.Formula.realize_iAlls {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {γ : Type u_3} [] {f : αβ γ} {φ : } {v : βM} :
∀ (i : γM), FirstOrder.Language.Formula.Realize φ fun a => Sum.elim v i (f a)
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_iAlls {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {γ : Type u_3} [] {f : αβ γ} {φ : } {v : βM} {v' : Fin 0M} :
∀ (i : γM), FirstOrder.Language.Formula.Realize φ fun a => Sum.elim v i (f a)
@[simp]
theorem FirstOrder.Language.Formula.realize_iExs {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {γ : Type u_3} [] {f : αβ γ} {φ : } {v : βM} :
i, FirstOrder.Language.Formula.Realize φ fun a => Sum.elim v i (f a)
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_iExs {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {γ : Type u_3} [] {f : αβ γ} {φ : } {v : βM} {v' : Fin 0M} :
i, FirstOrder.Language.Formula.Realize φ fun a => Sum.elim v i (f a)
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_toFormula {L : FirstOrder.Language} {M : Type w} {α : Type u'} {n : } (φ : ) (v : α Fin nM) :
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_iSup {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {n : } (s : ) (f : ) (v : αM) (v' : Fin nM) :
b, b s
@[simp]
theorem FirstOrder.Language.BoundedFormula.realize_iInf {L : FirstOrder.Language} {M : Type w} {α : Type u'} {β : Type v'} {n : } (s : ) (f : ) (v : αM) (v' : Fin nM) :
∀ (b : β), b s
@[simp]
theorem FirstOrder.Language.Equiv.realize_boundedFormula {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {α : Type u'} {n : } (g : ) (φ : ) {v : αM} {xs : Fin nM} :
@[simp]
theorem FirstOrder.Language.Equiv.realize_formula {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {α : Type u'} (g : ) (φ : ) {v : αM} :
theorem FirstOrder.Language.Equiv.realize_sentence {L : FirstOrder.Language} {M : Type w} {N : Type u_1} (g : ) (φ : ) :
M φ N φ
theorem FirstOrder.Language.Equiv.theory_model {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {T : } (g : ) [M T] :
N T
@[simp]
theorem FirstOrder.Language.model_distinctConstantsTheory (L : FirstOrder.Language) {α : Type u'} {M : Type w} (s : Set α) :
Set.InjOn (fun i => ↑()) s
theorem FirstOrder.Language.ElementarilyEquivalent.trans {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} (MN : ) (NP : ) :
theorem FirstOrder.Language.ElementarilyEquivalent.theory_model {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {T : } [MT : M T] (h : ) :
N T