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 #

Main Results #

Implementation Notes #

References #

For the Flypitch project:

def FirstOrder.Language.Term.realize {L : FirstOrder.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
Instances For
    @[simp]
    theorem FirstOrder.Language.Term.realize_var {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} (v : αM) (k : α) :
    @[simp]
    theorem FirstOrder.Language.Term.realize_func {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} (v : αM) {n : } (f : L.Functions n) (ts : Fin nL.Term α) :
    @[simp]
    theorem FirstOrder.Language.Term.realize_relabel {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α} {g : αβ} {v : βM} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_liftAt {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : } {t : L.Term (α Fin n)} {v : α Fin (n + n')M} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_constants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {c : L.Constants} {v : αM} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_functions_apply₁ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {f : L.Functions 1} {t : L.Term α} {v : αM} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_functions_apply₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {f : L.Functions 2} {t₁ t₂ : L.Term α} {v : αM} :
    theorem FirstOrder.Language.Term.realize_con {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {A : Set M} {a : A} {v : αM} :
    FirstOrder.Language.Term.realize v (L.con a).term = a
    @[simp]
    theorem FirstOrder.Language.Term.realize_subst {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {t : L.Term α} {tf : αL.Term β} {v : βM} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_restrictVar {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [DecidableEq α] {t : L.Term α} {s : Set α} (h : t.varFinset s) {v : αM} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_restrictVarLeft {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [DecidableEq α] {γ : Type u_4} {t : L.Term (α γ)} {s : Set α} (h : t.varFinsetLeft s) {v : αM} {xs : γM} :
    @[simp]
    theorem FirstOrder.Language.Term.realize_constantsToVars {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {t : (L.withConstants α).Term β} {v : βM} :
    FirstOrder.Language.Term.realize (Sum.elim (fun (a : α) => (L.con a)) v) t.constantsToVars = FirstOrder.Language.Term.realize v t
    @[simp]
    theorem FirstOrder.Language.Term.realize_varsToConstants {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {t : L.Term (α β)} {v : βM} :
    FirstOrder.Language.Term.realize v t.varsToConstants = FirstOrder.Language.Term.realize (Sum.elim (fun (a : α) => (L.con a)) v) t
    theorem FirstOrder.Language.Term.realize_constantsVarsEquivLeft {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : } {t : (L.withConstants α).Term (β Fin n)} {v : βM} {xs : Fin nM} :
    FirstOrder.Language.Term.realize (Sum.elim (Sum.elim (fun (a : α) => (L.con a)) v) xs) (FirstOrder.Language.Term.constantsVarsEquivLeft t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t
    @[simp]
    theorem FirstOrder.Language.LHom.realize_onTerm {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (t : L.Term α) (v : αM) :
    @[simp]
    theorem FirstOrder.Language.HomClass.realize_term {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {F : Type u_4} [FunLike F M N] [L.HomClass F M N] (g : F) {t : L.Term α} {v : αM} :
    def FirstOrder.Language.BoundedFormula.Realize {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } (_f : L.BoundedFormula α l) (_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} [L.Structure M] {α : Type u'} {l : } {v : αM} {xs : Fin lM} :
      .Realize v xs False
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_not {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ : L.BoundedFormula α l} {v : αM} {xs : Fin lM} :
      φ.not.Realize v xs ¬φ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_bdEqual {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {v : αM} {xs : Fin lM} (t₁ t₂ : L.Term (α Fin l)) :
      (t₁.bdEqual t₂).Realize v xs FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ = FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {v : αM} {xs : Fin lM} :
      .Realize v xs True
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ ψ : L.BoundedFormula α l} {v : αM} {xs : Fin lM} :
      (φ ψ).Realize v xs φ.Realize v xs ψ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_foldr_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } (l : List (L.BoundedFormula α n)) (v : αM) (xs : Fin nM) :
      (List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 x2) l).Realize v xs φl, φ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_imp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ ψ : L.BoundedFormula α l} {v : αM} {xs : Fin lM} :
      (φ.imp ψ).Realize v xs φ.Realize v xsψ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_rel {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {v : αM} {xs : Fin lM} {k : } {R : L.Relations k} {ts : Fin kL.Term (α Fin l)} :
      (R.boundedFormula ts).Realize v xs FirstOrder.Language.Structure.RelMap R fun (i : Fin k) => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_rel₁ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {v : αM} {xs : Fin lM} {R : L.Relations 1} {t : L.Term (α Fin l)} :
      (R.boundedFormula₁ t).Realize v xs FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t]
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_rel₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {v : αM} {xs : Fin lM} {R : L.Relations 2} {t₁ t₂ : L.Term (α Fin l)} :
      (R.boundedFormula₂ t₁ t₂).Realize v xs FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize (Sum.elim v xs) t₁, FirstOrder.Language.Term.realize (Sum.elim v xs) t₂]
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ ψ : L.BoundedFormula α l} {v : αM} {xs : Fin lM} :
      (φ ψ).Realize v xs φ.Realize v xs ψ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_foldr_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } (l : List (L.BoundedFormula α n)) (v : αM) (xs : Fin nM) :
      (List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 x2) l).Realize v xs φl, φ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_all {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {θ : L.BoundedFormula α l.succ} {v : αM} {xs : Fin lM} :
      θ.all.Realize v xs ∀ (a : M), θ.Realize v (Fin.snoc xs a)
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_ex {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {θ : L.BoundedFormula α l.succ} {v : αM} {xs : Fin lM} :
      θ.ex.Realize v xs ∃ (a : M), θ.Realize v (Fin.snoc xs a)
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {l : } {φ ψ : L.BoundedFormula α l} {v : αM} {xs : Fin lM} :
      (φ.iff ψ).Realize v xs (φ.Realize v xs ψ.Realize v xs)
      theorem FirstOrder.Language.BoundedFormula.realize_castLE_of_eq {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {m n : } (h : m = n) {h' : m n} {φ : L.BoundedFormula α m} {v : αM} {xs : Fin nM} :
      (FirstOrder.Language.BoundedFormula.castLE h' φ).Realize v xs φ.Realize v (xs Fin.cast h)
      theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_id {L : FirstOrder.Language} {L' : FirstOrder.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.BoundedFormula α n} {v : αM} {v' : βM} {xs : Fin nM} (h1 : ∀ (n : ) (t : L.Term (α Fin n)) (xs : Fin nM), FirstOrder.Language.Term.realize (Sum.elim v' xs) (ft n t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t) (h2 : ∀ (n : ) (R : L.Relations n) (x : Fin nM), FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) :
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun (x : ) => id) φ).Realize v' xs φ.Realize v xs
      theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe {L : FirstOrder.Language} {L' : FirstOrder.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.BoundedFormula α 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), FirstOrder.Language.Term.realize (Sum.elim v' xs') (ft n t) = FirstOrder.Language.Term.realize (Sum.elim (v xs') (xs' Fin.natAdd k)) t) (h2 : ∀ (n : ) (R : L.Relations n) (x : Fin nM), FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) (hv : ∀ (n : ) (xs : Fin (k + n)M) (x : M), v (Fin.snoc xs x) = v xs) :
      (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun (x : ) => FirstOrder.Language.BoundedFormula.castLE ) φ).Realize v' xs φ.Realize (v xs) (xs Fin.natAdd k)
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_relabel {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {m n : } {φ : L.BoundedFormula α n} {g : αβ Fin m} {v : βM} {xs : Fin (m + n)M} :
      (FirstOrder.Language.BoundedFormula.relabel g φ).Realize v xs φ.Realize (Sum.elim v (xs Fin.castAdd n) g) (xs Fin.natAdd m)
      theorem FirstOrder.Language.BoundedFormula.realize_liftAt {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n n' m : } {φ : L.BoundedFormula α n} {v : αM} {xs : Fin (n + n')M} (hmn : m + n' n + 1) :
      (FirstOrder.Language.BoundedFormula.liftAt n' m φ).Realize v xs φ.Realize v (xs fun (i : Fin n) => if i < m then Fin.castAdd n' i else i.addNat n')
      theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n m : } {φ : L.BoundedFormula α n} {v : αM} {xs : Fin (n + 1)M} (hmn : m n) :
      (FirstOrder.Language.BoundedFormula.liftAt 1 m φ).Realize v xs φ.Realize v (xs fun (i : Fin n) => if i < m then i.castSucc else i.succ)
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one_self {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } {φ : L.BoundedFormula α n} {v : αM} {xs : Fin (n + 1)M} :
      (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).Realize v xs φ.Realize v (xs Fin.castSucc)
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_subst {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : } {φ : L.BoundedFormula α n} {tf : αL.Term β} {v : βM} {xs : Fin nM} :
      (φ.subst tf).Realize v xs φ.Realize (fun (a : α) => FirstOrder.Language.Term.realize v (tf a)) xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [DecidableEq α] {n : } {φ : L.BoundedFormula α n} {s : Set α} (h : φ.freeVarFinset s) {v : αM} {xs : Fin nM} :
      (φ.restrictFreeVar (Set.inclusion h)).Realize (v Subtype.val) xs φ.Realize v xs
      theorem FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {n : } {φ : (L.withConstants α).BoundedFormula β n} {v : βM} {xs : Fin nM} :
      (FirstOrder.Language.BoundedFormula.constantsVarsEquiv φ).Realize (Sum.elim (fun (a : α) => (L.con a)) v) xs φ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.BoundedFormula.realize_relabelEquiv {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {g : α β} {k : } {φ : L.BoundedFormula α k} {v : βM} {xs : Fin kM} :
      ((FirstOrder.Language.BoundedFormula.relabelEquiv g) φ).Realize v xs φ.Realize (v g) xs
      theorem FirstOrder.Language.BoundedFormula.realize_all_liftAt_one_self {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [Nonempty M] {n : } {φ : L.BoundedFormula α n} {v : αM} {xs : Fin nM} :
      (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all.Realize v xs φ.Realize v xs
      @[simp]
      theorem FirstOrder.Language.LHom.realize_onBoundedFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] {n : } (ψ : L.BoundedFormula α n) {v : αM} {xs : Fin nM} :
      (φ.onBoundedFormula ψ).Realize v xs ψ.Realize v xs
      def FirstOrder.Language.Formula.Realize {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} (φ : L.Formula α) (v : αM) :

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

      Equations
      Instances For
        @[simp]
        theorem FirstOrder.Language.Formula.realize_not {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {φ : L.Formula α} {v : αM} :
        φ.not.Realize v ¬φ.Realize v
        @[simp]
        theorem FirstOrder.Language.Formula.realize_bot {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : αM} :
        .Realize v False
        @[simp]
        theorem FirstOrder.Language.Formula.realize_top {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : αM} :
        .Realize v True
        @[simp]
        theorem FirstOrder.Language.Formula.realize_inf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : αM} :
        (φ ψ).Realize v φ.Realize v ψ.Realize v
        @[simp]
        theorem FirstOrder.Language.Formula.realize_imp {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : αM} :
        (φ.imp ψ).Realize v φ.Realize vψ.Realize v
        @[simp]
        theorem FirstOrder.Language.Formula.realize_rel {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : αM} {k : } {R : L.Relations k} {ts : Fin kL.Term α} :
        (R.formula ts).Realize v FirstOrder.Language.Structure.RelMap R fun (i : Fin k) => FirstOrder.Language.Term.realize v (ts i)
        @[simp]
        theorem FirstOrder.Language.Formula.realize_rel₁ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : αM} {R : L.Relations 1} {t : L.Term α} :
        @[simp]
        theorem FirstOrder.Language.Formula.realize_rel₂ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {v : αM} {R : L.Relations 2} {t₁ t₂ : L.Term α} :
        @[simp]
        theorem FirstOrder.Language.Formula.realize_sup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : αM} :
        (φ ψ).Realize v φ.Realize v ψ.Realize v
        @[simp]
        theorem FirstOrder.Language.Formula.realize_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {φ ψ : L.Formula α} {v : αM} :
        (φ.iff ψ).Realize v (φ.Realize v ψ.Realize v)
        @[simp]
        theorem FirstOrder.Language.Formula.realize_relabel {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {φ : L.Formula α} {g : αβ} {v : βM} :
        (FirstOrder.Language.Formula.relabel g φ).Realize v φ.Realize (v g)
        theorem FirstOrder.Language.Formula.realize_relabel_sum_inr {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n : } (φ : L.Formula (Fin n)) {v : EmptyM} {x : Fin nM} :
        (FirstOrder.Language.BoundedFormula.relabel Sum.inr φ).Realize v x φ.Realize x
        @[simp]
        theorem FirstOrder.Language.Formula.realize_equal {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {t₁ t₂ : L.Term α} {x : αM} :
        @[simp]
        theorem FirstOrder.Language.Formula.realize_graph {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n : } {f : L.Functions n} {x : Fin nM} {y : M} :
        @[simp]
        theorem FirstOrder.Language.LHom.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) {v : αM} :
        (φ.onFormula ψ).Realize v ψ.Realize v
        @[simp]
        theorem FirstOrder.Language.LHom.setOf_realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Formula α) :
        setOf (φ.onFormula ψ).Realize = setOf ψ.Realize
        def FirstOrder.Language.Sentence.Realize {L : FirstOrder.Language} (M : Type w) [L.Structure M] (φ : L.Sentence) :

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

        Equations
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem FirstOrder.Language.Sentence.realize_not {L : FirstOrder.Language} (M : Type w) [L.Structure M] {φ : L.Sentence} :
            @[simp]
            theorem FirstOrder.Language.Formula.realize_equivSentence_symm_con {L : FirstOrder.Language} (M : Type w) [L.Structure M] {α : Type u'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] (φ : (L.withConstants α).Sentence) :
            ((FirstOrder.Language.Formula.equivSentence.symm φ).Realize fun (a : α) => (L.con a)) M φ
            @[simp]
            theorem FirstOrder.Language.Formula.realize_equivSentence {L : FirstOrder.Language} (M : Type w) [L.Structure M] {α : Type u'} [(L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] (φ : L.Formula α) :
            M FirstOrder.Language.Formula.equivSentence φ φ.Realize fun (a : α) => (L.con a)
            theorem FirstOrder.Language.Formula.realize_equivSentence_symm {L : FirstOrder.Language} (M : Type w) [L.Structure M] {α : Type u'} (φ : (L.withConstants α).Sentence) (v : αM) :
            (FirstOrder.Language.Formula.equivSentence.symm φ).Realize v M φ
            @[simp]
            theorem FirstOrder.Language.LHom.realize_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} (M : Type w) [L.Structure M] [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (ψ : L.Sentence) :
            M φ.onSentence ψ M ψ
            def FirstOrder.Language.completeTheory (L : FirstOrder.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
            • L.completeTheory M = {φ : L.Sentence | M φ}
            Instances For
              def FirstOrder.Language.ElementarilyEquivalent (L : FirstOrder.Language) (M : Type w) (N : Type u_1) [L.Structure M] [L.Structure N] :

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

              Equations
              • L.ElementarilyEquivalent M N = (L.completeTheory M = L.completeTheory N)
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem FirstOrder.Language.mem_completeTheory {L : FirstOrder.Language} {M : Type w} [L.Structure M] {φ : L.Sentence} :
                  φ L.completeTheory M M φ
                  theorem FirstOrder.Language.elementarilyEquivalent_iff {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] :
                  L.ElementarilyEquivalent M N ∀ (φ : L.Sentence), M φ N φ
                  class FirstOrder.Language.Theory.Model {L : FirstOrder.Language} (M : Type w) [L.Structure M] (T : L.Theory) :

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

                  • realize_of_mem : φT, M φ
                  Instances

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem FirstOrder.Language.Theory.model_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] (T : L.Theory) :
                      M T φT, M φ
                      theorem FirstOrder.Language.Theory.realize_sentence_of_mem {L : FirstOrder.Language} {M : Type w} [L.Structure M] (T : L.Theory) [M T] {φ : L.Sentence} (h : φ T) :
                      M φ
                      @[simp]
                      theorem FirstOrder.Language.LHom.onTheory_model {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [L.Structure M] [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory) :
                      M φ.onTheory T M T
                      instance FirstOrder.Language.model_empty {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                      Equations
                      • =
                      theorem FirstOrder.Language.Theory.Model.mono {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T T' : L.Theory} (_h : M T') (hs : T T') :
                      M T
                      theorem FirstOrder.Language.Theory.Model.union {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T T' : L.Theory} (h : M T) (h' : M T') :
                      M T T'
                      @[simp]
                      theorem FirstOrder.Language.Theory.model_union_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T T' : L.Theory} :
                      M T T' M T M T'
                      @[simp]
                      theorem FirstOrder.Language.Theory.model_singleton_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {φ : L.Sentence} :
                      M {φ} M φ
                      theorem FirstOrder.Language.Theory.model_insert_iff {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T : L.Theory} {φ : L.Sentence} :
                      M insert φ T M φ M T
                      theorem FirstOrder.Language.Theory.model_iff_subset_completeTheory {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T : L.Theory} :
                      M T T L.completeTheory M
                      theorem FirstOrder.Language.Theory.completeTheory.subset {L : FirstOrder.Language} {M : Type w} [L.Structure M] {T : L.Theory} [MT : M T] :
                      T L.completeTheory M
                      instance FirstOrder.Language.model_completeTheory {L : FirstOrder.Language} {M : Type w} [L.Structure M] :
                      M L.completeTheory M
                      Equations
                      • =
                      theorem FirstOrder.Language.realize_iff_of_model_completeTheory {L : FirstOrder.Language} (M : Type w) (N : Type u_1) [L.Structure M] [L.Structure N] [N L.completeTheory M] (φ : L.Sentence) :
                      N φ M φ
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_alls {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } {φ : L.BoundedFormula α n} {v : αM} :
                      φ.alls.Realize v ∀ (xs : Fin nM), φ.Realize v xs
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_exs {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } {φ : L.BoundedFormula α n} {v : αM} :
                      φ.exs.Realize v ∃ (xs : Fin nM), φ.Realize v xs
                      @[simp]
                      theorem FirstOrder.Language.Formula.realize_iAlls {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {γ : Type u_3} [Finite γ] {f : αβ γ} {φ : L.Formula α} {v : βM} :
                      (FirstOrder.Language.Formula.iAlls f φ).Realize v ∀ (i : γM), φ.Realize fun (a : α) => Sum.elim v i (f a)
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_iAlls {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {γ : Type u_3} [Finite γ] {f : αβ γ} {φ : L.Formula α} {v : βM} {v' : Fin 0M} :
                      FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iAlls f φ) v v' ∀ (i : γM), φ.Realize fun (a : α) => Sum.elim v i (f a)
                      @[simp]
                      theorem FirstOrder.Language.Formula.realize_iExs {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {γ : Type u_3} [Finite γ] {f : αβ γ} {φ : L.Formula α} {v : βM} :
                      (FirstOrder.Language.Formula.iExs f φ).Realize v ∃ (i : γM), φ.Realize fun (a : α) => Sum.elim v i (f a)
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_iExs {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {γ : Type u_3} [Finite γ] {f : αβ γ} {φ : L.Formula α} {v : βM} {v' : Fin 0M} :
                      FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Formula.iExs f φ) v v' ∃ (i : γM), φ.Realize fun (a : α) => Sum.elim v i (f a)
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_toFormula {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {n : } (φ : L.BoundedFormula α n) (v : α Fin nM) :
                      φ.toFormula.Realize v φ.Realize (v Sum.inl) (v Sum.inr)
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_iSup {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : } (s : Finset β) (f : βL.BoundedFormula α n) (v : αM) (v' : Fin nM) :
                      (FirstOrder.Language.BoundedFormula.iSup s f).Realize v v' bs, (f b).Realize v v'
                      @[simp]
                      theorem FirstOrder.Language.BoundedFormula.realize_iInf {L : FirstOrder.Language} {M : Type w} [L.Structure M] {α : Type u'} {β : Type v'} {n : } (s : Finset β) (f : βL.BoundedFormula α n) (v : αM) (v' : Fin nM) :
                      (FirstOrder.Language.BoundedFormula.iInf s f).Realize v v' bs, (f b).Realize v v'
                      @[simp]
                      theorem FirstOrder.Language.StrongHomClass.realize_boundedFormula {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {n : } {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.BoundedFormula α n) {v : αM} {xs : Fin nM} :
                      φ.Realize (g v) (g xs) φ.Realize v xs
                      @[simp]
                      theorem FirstOrder.Language.StrongHomClass.realize_formula {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {α : Type u'} {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.Formula α) {v : αM} :
                      φ.Realize (g v) φ.Realize v
                      theorem FirstOrder.Language.StrongHomClass.realize_sentence {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.Sentence) :
                      M φ N φ
                      theorem FirstOrder.Language.StrongHomClass.theory_model {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {T : L.Theory} {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) [M T] :
                      N T
                      theorem FirstOrder.Language.StrongHomClass.elementarilyEquivalent {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {F : Type u_4} [EquivLike F M N] [L.StrongHomClass F M N] (g : F) :
                      L.ElementarilyEquivalent M N
                      @[simp]
                      theorem FirstOrder.Language.Relations.realize_reflexive {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} :
                      M r.reflexive Reflexive fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]
                      @[simp]
                      theorem FirstOrder.Language.Relations.realize_irreflexive {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} :
                      M r.irreflexive Irreflexive fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]
                      @[simp]
                      theorem FirstOrder.Language.Relations.realize_symmetric {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} :
                      M r.symmetric Symmetric fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]
                      @[simp]
                      theorem FirstOrder.Language.Relations.realize_antisymmetric {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} :
                      M r.antisymmetric AntiSymmetric fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]
                      @[simp]
                      theorem FirstOrder.Language.Relations.realize_transitive {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} :
                      M r.transitive Transitive fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]
                      @[simp]
                      theorem FirstOrder.Language.Relations.realize_total {L : FirstOrder.Language} {M : Type w} [L.Structure M] {r : L.Relations 2} :
                      M r.total Total fun (x y : M) => FirstOrder.Language.Structure.RelMap r ![x, y]
                      @[simp]
                      theorem FirstOrder.Language.model_infiniteTheory_iff (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
                      M L.infiniteTheory Infinite M
                      instance FirstOrder.Language.model_infiniteTheory (L : FirstOrder.Language) {M : Type w} [L.Structure M] [h : Infinite M] :
                      M L.infiniteTheory
                      Equations
                      • =
                      @[simp]
                      theorem FirstOrder.Language.model_nonemptyTheory_iff (L : FirstOrder.Language) {M : Type w} [L.Structure M] :
                      M L.nonemptyTheory Nonempty M
                      instance FirstOrder.Language.model_nonempty (L : FirstOrder.Language) {M : Type w} [L.Structure M] [h : Nonempty M] :
                      M L.nonemptyTheory
                      Equations
                      • =
                      theorem FirstOrder.Language.model_distinctConstantsTheory (L : FirstOrder.Language) {α : Type u'} {M : Type w} [(L.withConstants α).Structure M] (s : Set α) :
                      M L.distinctConstantsTheory s Set.InjOn (fun (i : α) => (L.con i)) s
                      theorem FirstOrder.Language.card_le_of_model_distinctConstantsTheory (L : FirstOrder.Language) {α : Type u'} (s : Set α) (M : Type w) [(L.withConstants α).Structure M] [h : M L.distinctConstantsTheory s] :
                      theorem FirstOrder.Language.ElementarilyEquivalent.symm {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) :
                      L.ElementarilyEquivalent N M
                      theorem FirstOrder.Language.ElementarilyEquivalent.trans {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [L.Structure M] [L.Structure N] [L.Structure P] (MN : L.ElementarilyEquivalent M N) (NP : L.ElementarilyEquivalent N P) :
                      L.ElementarilyEquivalent M P
                      theorem FirstOrder.Language.ElementarilyEquivalent.completeTheory_eq {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) :
                      L.completeTheory M = L.completeTheory N
                      theorem FirstOrder.Language.ElementarilyEquivalent.realize_sentence {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) (φ : L.Sentence) :
                      M φ N φ
                      theorem FirstOrder.Language.ElementarilyEquivalent.theory_model_iff {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {T : L.Theory} (h : L.ElementarilyEquivalent M N) :
                      M T N T
                      theorem FirstOrder.Language.ElementarilyEquivalent.theory_model {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] {T : L.Theory} [MT : M T] (h : L.ElementarilyEquivalent M N) :
                      N T
                      theorem FirstOrder.Language.ElementarilyEquivalent.nonempty_iff {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) :
                      theorem FirstOrder.Language.ElementarilyEquivalent.nonempty {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] [Mn : Nonempty M] (h : L.ElementarilyEquivalent M N) :
                      theorem FirstOrder.Language.ElementarilyEquivalent.infinite_iff {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (h : L.ElementarilyEquivalent M N) :
                      theorem FirstOrder.Language.ElementarilyEquivalent.infinite {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] [Mi : Infinite M] (h : L.ElementarilyEquivalent M N) :