# 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 #

• FirstOrder.Language.Theory.IsSatisfiable: T.IsSatisfiable indicates that T has a nonempty model.
• FirstOrder.Language.Theory.IsFinitelySatisfiable: T.IsFinitelySatisfiable indicates that every finite subset of T is satisfiable.
• FirstOrder.Language.Theory.IsComplete: T.IsComplete indicates that T is satisfiable and models each sentence or its negation.
• FirstOrder.Language.Theory.SemanticallyEquivalent: T.SemanticallyEquivalent φ ψ indicates that φ and ψ are equivalent formulas or sentences in models of T.
• Cardinal.Categorical: A theory is κ-categorical if all models of size κ are isomorphic.

## Main Results #

• The Compactness Theorem, FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable, shows that a theory is satisfiable iff it is finitely satisfiable.
• FirstOrder.Language.completeTheory.isComplete: The complete theory of a structure is complete.
• FirstOrder.Language.Theory.exists_large_model_of_infinite_model shows that any theory with an infinite model has arbitrarily large models.
• FirstOrder.Language.Theory.exists_elementaryEmbedding_card_eq: 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 κ.

## Implementation Details #

• Satisfiability of an L.Theory T is defined in the minimal universe containing all the symbols of L. By Löwenheim-Skolem, this is equivalent to satisfiability in any universe.

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.

theorem FirstOrder.Language.Theory.isSatisfiable_directed_union_iff {L : FirstOrder.Language} {ι : Type u_1} [] {T : } (h : Directed (fun x x_1 => x x_1) T) :
FirstOrder.Language.Theory.IsSatisfiable (⋃ (i : ι), T i) ∀ (i : ι),

Any theory with an infinite model has arbitrarily large models.

theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le (L : FirstOrder.Language) (M : Type w') [] (κ : Cardinal.{w}) (h1 : ) (h2 : ) (h3 : ) :
N, = κ

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

theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge (L : FirstOrder.Language) (M : Type w') [iM : ] (κ : Cardinal.{w}) (h1 : ) (h2 : ) :
N, = κ

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') [iM : ] (κ : Cardinal.{w}) (h1 : ) (h2 : ) :
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 κ.

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 : } (h : M, Infinite M) (κ : Cardinal.{w}) (h1 : ) (h2 : ) :
N, = κ

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
theorem FirstOrder.Language.Theory.models_formula_iff {L : FirstOrder.Language} {T : } {α : Type w} {φ : } :
T ⊨ᵇ φ ∀ (M : ) (v : αM),
theorem FirstOrder.Language.Theory.models_sentence_iff {L : FirstOrder.Language} {T : } {φ : } :
T ⊨ᵇ φ ∀ (M : ), M φ
theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence {L : FirstOrder.Language} {T : } {φ : } (h : T ⊨ᵇ φ) (M : Type u_1) [M T] [] :
M φ
theorem FirstOrder.Language.Theory.models_of_models_theory {L : FirstOrder.Language} {T : } {α : Type w} {T' : } (h : ∀ (φ : ), φ T'T ⊨ᵇ φ) {φ : } (hφ : T' ⊨ᵇ φ) :
T ⊨ᵇ φ
theorem FirstOrder.Language.Theory.models_iff_finset_models {L : FirstOrder.Language} {T : } {φ : } :
T ⊨ᵇ φ T0, 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.

Instances For

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

Instances For
def FirstOrder.Language.Theory.SemanticallyEquivalent {L : FirstOrder.Language} {α : Type w} {n : } (T : ) (φ : ) (ψ : ) :

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
theorem FirstOrder.Language.Theory.SemanticallyEquivalent.trans {L : FirstOrder.Language} {T : } {α : Type w} {n : } {φ : } {ψ : } {θ : } :
theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff {L : FirstOrder.Language} {T : } {α : Type w} {n : } {φ : } {ψ : } {M : Type (max u v)} [] [M T] {v : αM} {xs : Fin nM} :
theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff {L : FirstOrder.Language} {T : } {α : Type w} {φ : } {ψ : } {M : Type (max u v)} [] (_hM : M T) {v : αM} :

Semantic equivalence forms an equivalence relation on formulas.

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

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

Instances For
theorem Cardinal.Categorical.isComplete {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : ) (h : ) (h1 : ) (h2 : ) (hT : ∀ (M : ), Infinite M) :

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