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 (x1 x2 : L.Theory) => x1 x2) 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_formula_iff_onTheory_models_equivSentence {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} :
          T ⊨ᵇ φ (L.lhomWithConstants α).onTheory T ⊨ᵇ FirstOrder.Language.Formula.equivSentence φ
          theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_formula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} (h : T ⊨ᵇ φ) (M : Type u_1) [L.Structure M] [M T] [Nonempty M] {v : αM} :
          φ.Realize v
          theorem FirstOrder.Language.Theory.models_toFormula_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} :
          T ⊨ᵇ φ.toFormula T ⊨ᵇ φ
          theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : } {φ : L.BoundedFormula α n} (h : T ⊨ᵇ φ) (M : Type u_1) [L.Structure M] [M T] [Nonempty M] {v : αM} {xs : Fin nM} :
          φ.Realize v xs
          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 ⊨ᵇ φ
              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

              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.