# mathlib3documentation

model_theory.satisfiability

# First-Order Satisfiability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file deals with the satisfiability of first-order theories, as well as equivalence over them.

## Main Definitions #

• first_order.language.Theory.is_satisfiable: T.is_satisfiable indicates that T has a nonempty model.
• first_order.language.Theory.is_finitely_satisfiable: T.is_finitely_satisfiable indicates that every finite subset of T is satisfiable.
• first_order.language.Theory.is_complete: T.is_complete indicates that T is satisfiable and models each sentence or its negation.
• first_order.language.Theory.semantically_equivalent: T.semantically_equivalent φ ψ 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, first_order.language.Theory.is_satisfiable_iff_is_finitely_satisfiable, shows that a theory is satisfiable iff it is finitely satisfiable.
• first_order.language.complete_theory.is_complete: The complete theory of a structure is complete.
• first_order.language.Theory.exists_large_model_of_infinite_model shows that any theory with an infinite model has arbitrarily large models.
• first_order.language.Theory.exists_elementary_embedding_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.

Equations

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

Equations

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.

def first_order.language.Theory.models_bounded_formula {L : first_order.language} (T : L.Theory) {α : Type w} {n : } (φ : n) :
Prop

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

Equations
theorem first_order.language.Theory.models_formula_iff {L : first_order.language} {T : L.Theory} {α : Type w} {φ : L.formula α} :
T φ (M : T.Model) (v : α M), φ.realize v

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

Equations

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

Equations
def first_order.language.Theory.semantically_equivalent {L : first_order.language} {α : Type w} {n : } (T : L.Theory) (φ ψ : n) :
Prop

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
Instances for first_order.language.Theory.semantically_equivalent
@[refl]
@[protected, instance]
@[symm]
theorem first_order.language.Theory.semantically_equivalent.symm {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ : n} (h : ψ) :
@[trans]
theorem first_order.language.Theory.semantically_equivalent.trans {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ θ : n} (h1 : ψ) (h2 : θ) :
theorem first_order.language.Theory.semantically_equivalent.realize_bd_iff {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ : n} {M : Type (max u v)} [ne : nonempty M] [str : L.Structure M] [hM : M T] (h : ψ) {v : α M} {xs : fin n M} :
φ.realize v xs ψ.realize v xs
theorem first_order.language.Theory.semantically_equivalent.realize_iff {L : first_order.language} {T : L.Theory} {α : Type w} {φ ψ : L.formula α} {M : Type (max u v)} [ne : nonempty M] [str : L.Structure M] (hM : M T) (h : ψ) {v : α M} :
φ.realize v ψ.realize v

Semantic equivalence forms an equivalence relation on formulas.

Equations
@[protected]
theorem first_order.language.Theory.semantically_equivalent.all {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ : (n + 1)} (h : ψ) :
@[protected]
theorem first_order.language.Theory.semantically_equivalent.ex {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ : (n + 1)} (h : ψ) :
ψ.ex
@[protected]
theorem first_order.language.Theory.semantically_equivalent.not {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ : n} (h : ψ) :
@[protected]
theorem first_order.language.Theory.semantically_equivalent.imp {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ φ' ψ' : n} (h : ψ) (h' : ψ') :
T.semantically_equivalent (φ.imp φ') (ψ.imp ψ')
theorem first_order.language.bounded_formula.is_qf.induction_on_sup_not {L : first_order.language} {α : Type w} {n : } {P : n Prop} {φ : n} (h : φ.is_qf) (hf : P ) (ha : (ψ : n), ψ.is_atomic P ψ) (hsup : {φ₁ φ₂ : n}, P φ₁ P φ₂ P (φ₁ φ₂)) (hnot : {φ : n}, P φ P φ.not) (hse : {φ₁ φ₂ : n}, φ₂ (P φ₁ P φ₂)) :
P φ
theorem first_order.language.bounded_formula.is_qf.induction_on_inf_not {L : first_order.language} {α : Type w} {n : } {P : n Prop} {φ : n} (h : φ.is_qf) (hf : P ) (ha : (ψ : n), ψ.is_atomic P ψ) (hinf : {φ₁ φ₂ : n}, P φ₁ P φ₂ P (φ₁ φ₂)) (hnot : {φ : n}, P φ P φ.not) (hse : {φ₁ φ₂ : n}, φ₂ (P φ₁ P φ₂)) :
P φ
theorem first_order.language.bounded_formula.induction_on_all_ex {L : first_order.language} {α : Type w} {n : } {P : Π {m : }, m Prop} (φ : n) (hqf : {m : } {ψ : m}, ψ.is_qf P ψ) (hall : {m : } {ψ : (m + 1)}, P ψ P ψ.all) (hex : {m : } {φ : (m + 1)}, P φ P φ.ex) (hse : {m : } {φ₁ φ₂ : m}, φ₂ (P φ₁ P φ₂)) :
P φ
theorem first_order.language.bounded_formula.induction_on_exists_not {L : first_order.language} {α : Type w} {n : } {P : Π {m : }, m Prop} (φ : n) (hqf : {m : } {ψ : m}, ψ.is_qf P ψ) (hnot : {m : } {φ : m}, P φ P φ.not) (hex : {m : } {φ : (m + 1)}, P φ P φ.ex) (hse : {m : } {φ₁ φ₂ : m}, φ₂ (P φ₁ P φ₂)) :
P φ
def cardinal.categorical {L : first_order.language} (κ : cardinal) (T : L.Theory) :
Prop

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

Equations
theorem cardinal.categorical.is_complete {L : first_order.language} (κ : cardinal) (T : L.Theory) (h : κ.categorical T) (h1 : cardinal.aleph_0 κ) (h2 : L.card.lift κ.lift) (hS : T.is_satisfiable) (hT : (M : T.Model), ) :

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