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.

Instances For

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

    Instances For

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

      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 κ.

      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 κ.

      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.

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

      Instances For

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

        Instances For

          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.

          Instances For

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

            Instances For

              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.)

              Instances For

                Semantic equivalence forms an equivalence relation on formulas.

                Instances For
                  theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not {L : FirstOrder.Language} {α : Type w} {n : } {P : FirstOrder.Language.BoundedFormula L α nProp} {φ : FirstOrder.Language.BoundedFormula L α n} (h : FirstOrder.Language.BoundedFormula.IsQF φ) (hf : P ) (ha : (ψ : FirstOrder.Language.BoundedFormula L α n) → FirstOrder.Language.BoundedFormula.IsAtomic ψP ψ) (hsup : {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α n} → P φ₁P φ₂P (φ₁ φ₂)) (hnot : {φ : FirstOrder.Language.BoundedFormula L α n} → P φP (FirstOrder.Language.BoundedFormula.not φ)) (hse : ∀ {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.Theory.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ P φ₂)) :
                  P φ
                  theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not {L : FirstOrder.Language} {α : Type w} {n : } {P : FirstOrder.Language.BoundedFormula L α nProp} {φ : FirstOrder.Language.BoundedFormula L α n} (h : FirstOrder.Language.BoundedFormula.IsQF φ) (hf : P ) (ha : (ψ : FirstOrder.Language.BoundedFormula L α n) → FirstOrder.Language.BoundedFormula.IsAtomic ψP ψ) (hinf : {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α n} → P φ₁P φ₂P (φ₁ φ₂)) (hnot : {φ : FirstOrder.Language.BoundedFormula L α n} → P φP (FirstOrder.Language.BoundedFormula.not φ)) (hse : ∀ {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.Theory.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ P φ₂)) :
                  P φ
                  theorem FirstOrder.Language.BoundedFormula.induction_on_all_ex {L : FirstOrder.Language} {α : Type w} {n : } {P : {m : } → FirstOrder.Language.BoundedFormula L α mProp} (φ : FirstOrder.Language.BoundedFormula L α n) (hqf : {m : } → {ψ : FirstOrder.Language.BoundedFormula L α m} → FirstOrder.Language.BoundedFormula.IsQF ψP m ψ) (hall : {m : } → {ψ : FirstOrder.Language.BoundedFormula L α (m + 1)} → P (m + 1) ψP m (FirstOrder.Language.BoundedFormula.all ψ)) (hex : {m : } → {φ : FirstOrder.Language.BoundedFormula L α (m + 1)} → P (m + 1) φP m (FirstOrder.Language.BoundedFormula.ex φ)) (hse : ∀ {m : } {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α m}, FirstOrder.Language.Theory.SemanticallyEquivalent φ₁ φ₂ → (P m φ₁ P m φ₂)) :
                  P n φ
                  theorem FirstOrder.Language.BoundedFormula.induction_on_exists_not {L : FirstOrder.Language} {α : Type w} {n : } {P : {m : } → FirstOrder.Language.BoundedFormula L α mProp} (φ : FirstOrder.Language.BoundedFormula L α n) (hqf : {m : } → {ψ : FirstOrder.Language.BoundedFormula L α m} → FirstOrder.Language.BoundedFormula.IsQF ψP m ψ) (hnot : {m : } → {φ : FirstOrder.Language.BoundedFormula L α m} → P m φP m (FirstOrder.Language.BoundedFormula.not φ)) (hex : {m : } → {φ : FirstOrder.Language.BoundedFormula L α (m + 1)} → P (m + 1) φP m (FirstOrder.Language.BoundedFormula.ex φ)) (hse : ∀ {m : } {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α m}, FirstOrder.Language.Theory.SemanticallyEquivalent φ₁ φ₂ → (P m φ₁ P m φ₂)) :
                  P n φ

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

                  Instances For