Documentation

Mathlib.ModelTheory.Satisfiability

First-Order Satisfiability #

This file deals with the satisfiability of first-order theories, as well as equivalence over them.

Main Definitions #

Main Results #

Implementation Details #

A theory is satisfiable if a structure models it.

Equations
Instances For

    A theory is finitely satisfiable if all of its finite subtheories are satisfiable.

    Equations
    Instances For
      theorem FirstOrder.Language.Theory.Model.isSatisfiable {L : FirstOrder.Language} {T : L.Theory} (M : Type w) [Nonempty M] [L.Structure M] [M T] :
      T.IsSatisfiable
      theorem FirstOrder.Language.Theory.IsSatisfiable.mono {L : FirstOrder.Language} {T : L.Theory} {T' : L.Theory} (h : T'.IsSatisfiable) (hs : T T') :
      T.IsSatisfiable
      theorem FirstOrder.Language.Theory.isSatisfiable_of_isSatisfiable_onTheory {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (h : (φ.onTheory T).IsSatisfiable) :
      T.IsSatisfiable
      theorem FirstOrder.Language.Theory.isSatisfiable_onTheory_iff {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) :
      (φ.onTheory T).IsSatisfiable T.IsSatisfiable
      theorem FirstOrder.Language.Theory.IsSatisfiable.isFinitelySatisfiable {L : FirstOrder.Language} {T : L.Theory} (h : T.IsSatisfiable) :
      T.IsFinitelySatisfiable
      theorem FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable {L : FirstOrder.Language} {T : L.Theory} :
      T.IsSatisfiable T.IsFinitelySatisfiable

      The Compactness Theorem of first-order logic: A theory is satisfiable if and only if it is finitely satisfiable.

      theorem FirstOrder.Language.Theory.isSatisfiable_directed_union_iff {L : FirstOrder.Language} {ι : Type u_1} [Nonempty ι] {T : ιL.Theory} (h : Directed (fun (x x_1 : L.Theory) => x x_1) T) :
      FirstOrder.Language.Theory.IsSatisfiable (⋃ (i : ι), T i) ∀ (i : ι), (T i).IsSatisfiable
      theorem FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [Nonempty M] [L.Structure M] [M T] (h : Cardinal.lift.{w', w} (Cardinal.mk s) Cardinal.lift.{w, w'} (Cardinal.mk M)) :
      ((L.lhomWithConstants α).onTheory T L.distinctConstantsTheory s).IsSatisfiable
      theorem FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [L.Structure M] [M T] [Infinite M] :
      ((L.lhomWithConstants α).onTheory T L.distinctConstantsTheory s).IsSatisfiable
      theorem FirstOrder.Language.Theory.exists_large_model_of_infinite_model {L : FirstOrder.Language} (T : L.Theory) (κ : Cardinal.{w}) (M : Type w') [L.Structure M] [M T] [Infinite M] :
      ∃ (N : T.ModelType), Cardinal.lift.{max u v w, w} κ Cardinal.mk N

      Any theory with an infinite model has arbitrarily large models.

      A version of The Downward Löwenheim–Skolem theorem where the structure N elementarily embeds into M, but is not by type a substructure of M, and thus can be chosen to belong to the universe of the cardinal κ.

      The Upward Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of L and an infinite L-structure M, then M has an elementary extension of cardinality κ.

      theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq (L : FirstOrder.Language) (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 κ) (h2 : Cardinal.lift.{w, max u v} L.card Cardinal.lift.{max u v, w} κ) :
      ∃ (N : CategoryTheory.Bundled L.Structure), (Nonempty (L.ElementaryEmbedding (N) M) Nonempty (L.ElementaryEmbedding M N)) Cardinal.mk N = κ

      The Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of L and an infinite L-structure M, then there is an elementary embedding in the appropriate direction between then M and a structure of cardinality κ.

      theorem FirstOrder.Language.exists_elementarilyEquivalent_card_eq (L : FirstOrder.Language) (M : Type w') [L.Structure M] [Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 κ) (h2 : Cardinal.lift.{w, max u v} L.card Cardinal.lift.{max u v, w} κ) :
      ∃ (N : CategoryTheory.Bundled L.Structure), L.ElementarilyEquivalent M N Cardinal.mk N = κ

      A consequence of the Löwenheim–Skolem Theorem: If κ is a cardinal greater than the cardinalities of L and an infinite L-structure M, then there is a structure of cardinality κ elementarily equivalent to M.

      theorem FirstOrder.Language.Theory.exists_model_card_eq {L : FirstOrder.Language} {T : L.Theory} (h : ∃ (M : T.ModelType), Infinite M) (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 κ) (h2 : Cardinal.lift.{w, max u v} L.card Cardinal.lift.{max u v, w} κ) :
      ∃ (N : T.ModelType), Cardinal.mk N = κ
      def FirstOrder.Language.Theory.ModelsBoundedFormula {L : FirstOrder.Language} (T : L.Theory) {α : Type w} {n : } (φ : L.BoundedFormula α n) :

      A theory models a (bounded) formula when any of its nonempty models realizes that formula on all inputs.

      Equations
      • T ⊨ᵇ φ = ∀ (M : T.ModelType) (v : αM) (xs : Fin nM), φ.Realize v xs
      Instances For

        A theory models a (bounded) formula when any of its nonempty models realizes that formula on all inputs.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem FirstOrder.Language.Theory.models_formula_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} :
          T ⊨ᵇ φ ∀ (M : T.ModelType) (v : αM), φ.Realize v
          theorem FirstOrder.Language.Theory.models_sentence_iff {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} :
          T ⊨ᵇ φ ∀ (M : T.ModelType), M φ
          theorem FirstOrder.Language.Theory.models_sentence_of_mem {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} (h : φ T) :
          T ⊨ᵇ φ
          theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} (h : T ⊨ᵇ φ) (M : Type u_1) [L.Structure M] [M T] [Nonempty M] :
          M φ
          theorem FirstOrder.Language.Theory.models_of_models_theory {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {T' : L.Theory} (h : φT', T ⊨ᵇ φ) {φ : L.Formula α} (hφ : T' ⊨ᵇ φ) :
          T ⊨ᵇ φ
          theorem FirstOrder.Language.Theory.models_iff_finset_models {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} :
          T ⊨ᵇ φ ∃ (T0 : Finset L.Sentence), T0 T T0 ⊨ᵇ φ

          An alternative statement of the Compactness Theorem. A formula φ is modeled by a theory iff there is a finite subset T0 of the theory such that φ is modeled by T0

          A theory is complete when it is satisfiable and models each sentence or its negation.

          Equations
          Instances For
            theorem FirstOrder.Language.Theory.IsComplete.realize_sentence_iff {L : FirstOrder.Language} {T : L.Theory} (h : T.IsComplete) (φ : L.Sentence) (M : Type u_1) [L.Structure M] [M T] [Nonempty M] :
            M φ T ⊨ᵇ φ

            A theory is maximal when it is satisfiable and contains each sentence or its negation. Maximal theories are complete.

            Equations
            Instances For
              theorem FirstOrder.Language.Theory.IsMaximal.isComplete {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) :
              T.IsComplete
              theorem FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) (φ : L.Sentence) :
              theorem FirstOrder.Language.Theory.IsMaximal.mem_of_models {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) {φ : L.Sentence} (hφ : T ⊨ᵇ φ) :
              φ T
              theorem FirstOrder.Language.Theory.IsMaximal.mem_iff_models {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) (φ : L.Sentence) :
              φ T T ⊨ᵇ φ
              def FirstOrder.Language.Theory.SemanticallyEquivalent {L : FirstOrder.Language} {α : Type w} {n : } (T : L.Theory) (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) :

              Two (bounded) formulas are semantically equivalent over a theory T when they have the same interpretation in every model of T. (This is also known as logical equivalence, which also has a proof-theoretic definition.)

              Equations
              • T.SemanticallyEquivalent φ ψ = T ⊨ᵇ φ.iff ψ
              Instances For
                theorem FirstOrder.Language.Theory.SemanticallyEquivalent.refl {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α n) :
                T.SemanticallyEquivalent φ φ
                instance FirstOrder.Language.Theory.instIsReflBoundedFormulaSemanticallyEquivalent {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } :
                IsRefl (L.BoundedFormula α n) T.SemanticallyEquivalent
                Equations
                • =
                theorem FirstOrder.Language.Theory.SemanticallyEquivalent.symm {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) :
                T.SemanticallyEquivalent ψ φ
                theorem FirstOrder.Language.Theory.SemanticallyEquivalent.trans {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} (h1 : T.SemanticallyEquivalent φ ψ) (h2 : T.SemanticallyEquivalent ψ θ) :
                T.SemanticallyEquivalent φ θ
                theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {M : Type (max u v)} [Nonempty M] [L.Structure M] [M T] (h : T.SemanticallyEquivalent φ ψ) {v : αM} {xs : Fin nM} :
                φ.Realize v xs ψ.Realize v xs
                theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} {ψ : L.Formula α} {M : Type (max u v)} [Nonempty M] [L.Structure M] (_hM : M T) (h : T.SemanticallyEquivalent φ ψ) {v : αM} :
                φ.Realize v ψ.Realize v
                def FirstOrder.Language.Theory.semanticallyEquivalentSetoid {L : FirstOrder.Language} {α : Type w} {n : } (T : L.Theory) :
                Setoid (L.BoundedFormula α n)

                Semantic equivalence forms an equivalence relation on formulas.

                Equations
                • T.semanticallyEquivalentSetoid = { r := T.SemanticallyEquivalent, iseqv := }
                Instances For
                  theorem FirstOrder.Language.Theory.SemanticallyEquivalent.all {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α (n + 1)} {ψ : L.BoundedFormula α (n + 1)} (h : T.SemanticallyEquivalent φ ψ) :
                  T.SemanticallyEquivalent φ.all ψ.all
                  theorem FirstOrder.Language.Theory.SemanticallyEquivalent.ex {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α (n + 1)} {ψ : L.BoundedFormula α (n + 1)} (h : T.SemanticallyEquivalent φ ψ) :
                  T.SemanticallyEquivalent φ.ex ψ.ex
                  theorem FirstOrder.Language.Theory.SemanticallyEquivalent.not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) :
                  T.SemanticallyEquivalent φ.not ψ.not
                  theorem FirstOrder.Language.Theory.SemanticallyEquivalent.imp {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {φ' : L.BoundedFormula α n} {ψ' : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) (h' : T.SemanticallyEquivalent φ' ψ') :
                  T.SemanticallyEquivalent (φ.imp φ') (ψ.imp ψ')
                  theorem FirstOrder.Language.completeTheory.isSatisfiable (L : FirstOrder.Language) (M : Type w) [L.Structure M] [Nonempty M] :
                  (L.completeTheory M).IsSatisfiable
                  theorem FirstOrder.Language.completeTheory.mem_or_not_mem (L : FirstOrder.Language) (M : Type w) [L.Structure M] (φ : L.Sentence) :
                  φ L.completeTheory M FirstOrder.Language.Formula.not φ L.completeTheory M
                  theorem FirstOrder.Language.completeTheory.isMaximal (L : FirstOrder.Language) (M : Type w) [L.Structure M] [Nonempty M] :
                  (L.completeTheory M).IsMaximal
                  theorem FirstOrder.Language.completeTheory.isComplete (L : FirstOrder.Language) (M : Type w) [L.Structure M] [Nonempty M] :
                  (L.completeTheory M).IsComplete
                  theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_not_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α n) :
                  T.SemanticallyEquivalent φ φ.not.not
                  theorem FirstOrder.Language.BoundedFormula.imp_semanticallyEquivalent_not_sup {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) :
                  T.SemanticallyEquivalent (φ.imp ψ) (φ.not ψ)
                  theorem FirstOrder.Language.BoundedFormula.sup_semanticallyEquivalent_not_inf_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) :
                  T.SemanticallyEquivalent (φ ψ) (φ.not ψ.not).not
                  theorem FirstOrder.Language.BoundedFormula.inf_semanticallyEquivalent_not_sup_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) :
                  T.SemanticallyEquivalent (φ ψ) (φ.not ψ.not).not
                  theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α (n + 1)) :
                  T.SemanticallyEquivalent φ.all φ.not.ex.not
                  theorem FirstOrder.Language.BoundedFormula.ex_semanticallyEquivalent_not_all_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α (n + 1)) :
                  T.SemanticallyEquivalent φ.ex φ.not.all.not
                  theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_all_liftAt {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } (φ : L.BoundedFormula α n) :
                  T.SemanticallyEquivalent φ (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all
                  theorem FirstOrder.Language.Formula.semanticallyEquivalent_not_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) :
                  T.SemanticallyEquivalent φ φ.not.not
                  theorem FirstOrder.Language.Formula.imp_semanticallyEquivalent_not_sup {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) :
                  T.SemanticallyEquivalent (φ.imp ψ) (φ.not ψ)
                  theorem FirstOrder.Language.Formula.sup_semanticallyEquivalent_not_inf_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) :
                  T.SemanticallyEquivalent (φ ψ) (φ.not ψ.not).not
                  theorem FirstOrder.Language.Formula.inf_semanticallyEquivalent_not_sup_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) :
                  T.SemanticallyEquivalent (φ ψ) (φ.not ψ.not).not
                  theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not {L : FirstOrder.Language} {α : Type w} {n : } {P : L.BoundedFormula α nProp} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomicP ψ) (hsup : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁P φ₂P (φ₁ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φP φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, .SemanticallyEquivalent φ₁ φ₂(P φ₁ P φ₂)) :
                  P φ
                  theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not {L : FirstOrder.Language} {α : Type w} {n : } {P : L.BoundedFormula α nProp} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomicP ψ) (hinf : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁P φ₂P (φ₁ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φP φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, .SemanticallyEquivalent φ₁ φ₂(P φ₁ P φ₂)) :
                  P φ
                  theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_toPrenex {L : FirstOrder.Language} {α : Type w} {n : } (φ : L.BoundedFormula α n) :
                  .SemanticallyEquivalent φ φ.toPrenex
                  theorem FirstOrder.Language.BoundedFormula.induction_on_all_ex {L : FirstOrder.Language} {α : Type w} {n : } {P : {m : } → L.BoundedFormula α mProp} (φ : L.BoundedFormula α n) (hqf : ∀ {m : } {ψ : L.BoundedFormula α m}, ψ.IsQFP ψ) (hall : ∀ {m : } {ψ : L.BoundedFormula α (m + 1)}, P ψP ψ.all) (hex : ∀ {m : } {φ : L.BoundedFormula α (m + 1)}, P φP φ.ex) (hse : ∀ {m : } {φ₁ φ₂ : L.BoundedFormula α m}, .SemanticallyEquivalent φ₁ φ₂(P φ₁ P φ₂)) :
                  P φ
                  theorem FirstOrder.Language.BoundedFormula.induction_on_exists_not {L : FirstOrder.Language} {α : Type w} {n : } {P : {m : } → L.BoundedFormula α mProp} (φ : L.BoundedFormula α n) (hqf : ∀ {m : } {ψ : L.BoundedFormula α m}, ψ.IsQFP ψ) (hnot : ∀ {m : } {φ : L.BoundedFormula α m}, P φP φ.not) (hex : ∀ {m : } {φ : L.BoundedFormula α (m + 1)}, P φP φ.ex) (hse : ∀ {m : } {φ₁ φ₂ : L.BoundedFormula α m}, .SemanticallyEquivalent φ₁ φ₂(P φ₁ P φ₂)) :
                  P φ

                  A theory is κ-categorical if all models of size κ are isomorphic.

                  Equations
                  Instances For
                    theorem Cardinal.Categorical.isComplete {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : L.Theory) (h : κ.Categorical T) (h1 : Cardinal.aleph0 κ) (h2 : Cardinal.lift.{w, max u v} L.card Cardinal.lift.{max u v, w} κ) (hS : T.IsSatisfiable) (hT : ∀ (M : T.ModelType), Infinite M) :
                    T.IsComplete

                    The Łoś–Vaught Test : a criterion for categorical theories to be complete.