mathlib documentation

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

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.

theorem first_order.language.Theory.exists_model_card_eq {L : first_order.language} {T : L.Theory} (h : ∃ (M : T.Model), infinite M) (κ : cardinal) (h1 : cardinal.aleph_0 κ) (h2 : L.card.lift κ.lift) :
∃ (N : T.Model), cardinal.mk N = κ
def first_order.language.Theory.models_bounded_formula {L : first_order.language} (T : L.Theory) {α : Type w} {n : } (φ : L.bounded_formula α 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
def first_order.language.Theory.semantically_equivalent {L : first_order.language} {α : Type w} {n : } (T : L.Theory) (φ ψ : L.bounded_formula α 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
@[trans]
theorem first_order.language.Theory.semantically_equivalent.realize_bd_iff {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ : L.bounded_formula α n} {M : Type (max u v)} [ne : nonempty M] [str : L.Structure M] [hM : M T] (h : T.semantically_equivalent φ ψ) {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 : T.semantically_equivalent φ ψ) {v : α → M} :
φ.realize v ψ.realize v

Semantic equivalence forms an equivalence relation on formulas.

Equations
@[protected]
@[protected]
@[protected]
@[protected]
theorem first_order.language.Theory.semantically_equivalent.imp {L : first_order.language} {T : L.Theory} {α : Type w} {n : } {φ ψ φ' ψ' : L.bounded_formula α n} (h : T.semantically_equivalent φ ψ) (h' : T.semantically_equivalent φ' ψ') :
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 : L.bounded_formula α n → Prop} {φ : L.bounded_formula α n} (h : φ.is_qf) (hf : P ) (ha : ∀ (ψ : L.bounded_formula α n), ψ.is_atomicP ψ) (hsup : ∀ {φ₁ φ₂ : L.bounded_formula α n}, P φ₁P φ₂P (φ₁ φ₂)) (hnot : ∀ {φ : L.bounded_formula α n}, P φP φ.not) (hse : ∀ {φ₁ φ₂ : L.bounded_formula α n}, .semantically_equivalent φ₁ φ₂(P φ₁ P φ₂)) :
P φ
theorem first_order.language.bounded_formula.is_qf.induction_on_inf_not {L : first_order.language} {α : Type w} {n : } {P : L.bounded_formula α n → Prop} {φ : L.bounded_formula α n} (h : φ.is_qf) (hf : P ) (ha : ∀ (ψ : L.bounded_formula α n), ψ.is_atomicP ψ) (hinf : ∀ {φ₁ φ₂ : L.bounded_formula α n}, P φ₁P φ₂P (φ₁ φ₂)) (hnot : ∀ {φ : L.bounded_formula α n}, P φP φ.not) (hse : ∀ {φ₁ φ₂ : L.bounded_formula α n}, .semantically_equivalent φ₁ φ₂(P φ₁ P φ₂)) :
P φ
theorem first_order.language.bounded_formula.induction_on_all_ex {L : first_order.language} {α : Type w} {n : } {P : Π {m : }, L.bounded_formula α m → Prop} (φ : L.bounded_formula α n) (hqf : ∀ {m : } {ψ : L.bounded_formula α m}, ψ.is_qfP ψ) (hall : ∀ {m : } {ψ : L.bounded_formula α (m + 1)}, P ψP ψ.all) (hex : ∀ {m : } {φ : L.bounded_formula α (m + 1)}, P φP φ.ex) (hse : ∀ {m : } {φ₁ φ₂ : L.bounded_formula α m}, .semantically_equivalent φ₁ φ₂(P φ₁ P φ₂)) :
P φ
theorem first_order.language.bounded_formula.induction_on_exists_not {L : first_order.language} {α : Type w} {n : } {P : Π {m : }, L.bounded_formula α m → Prop} (φ : L.bounded_formula α n) (hqf : ∀ {m : } {ψ : L.bounded_formula α m}, ψ.is_qfP ψ) (hnot : ∀ {m : } {φ : L.bounded_formula α m}, P φP φ.not) (hex : ∀ {m : } {φ : L.bounded_formula α (m + 1)}, P φP φ.ex) (hse : ∀ {m : } {φ₁ φ₂ : L.bounded_formula α m}, .semantically_equivalent φ₁ φ₂(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), infinite M) :

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