mathlib3 documentation

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 #

Main Results #

Implementation Details #

source
def first_order.language.Theory.is_satisfiable {L : first_order.language} (T : L.Theory) :
Prop

A theory is satisfiable if a structure models it.

Equations
source
def first_order.language.Theory.is_finitely_satisfiable {L : first_order.language} (T : L.Theory) :
Prop

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

Equations
source
theorem first_order.language.Theory.model.is_satisfiable {L : first_order.language} {T : L.Theory} (M : Type w) [n : nonempty M] [S : L.Structure M] [M ⊨ T] :
T.is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable.mono {L : first_order.language} {T T' : L.Theory} (h : T'.is_satisfiable) (hs : T ⊆ T') :
T.is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable_empty (L : first_order.language) :
∅.is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable_of_is_satisfiable_on_Theory {L : first_order.language} {T : L.Theory} {L' : first_order.language} (φ : L →ᴸ L') (h : (φ.on_Theory T).is_satisfiable) :
T.is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable_on_Theory_iff {L : first_order.language} {T : L.Theory} {L' : first_order.language} {φ : L →ᴸ L'} (h : φ.injective) :
(φ.on_Theory T).is_satisfiable ↔ T.is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable.is_finitely_satisfiable {L : first_order.language} {T : L.Theory} (h : T.is_satisfiable) :
T.is_finitely_satisfiable
source
theorem first_order.language.Theory.is_satisfiable_iff_is_finitely_satisfiable {L : first_order.language} {T : L.Theory} :
T.is_satisfiable ↔ T.is_finitely_satisfiable

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

source
theorem first_order.language.Theory.is_satisfiable_directed_union_iff {L : first_order.language} {ι : Type u_1} [nonempty ι] {T : ι → L.Theory} (h : directed has_subset.subset T) :
first_order.language.Theory.is_satisfiable (⋃ (i : ι), T i) ↔ ∀ (i : ι), (T i).is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable_union_distinct_constants_theory_of_card_le {L : first_order.language} {α : Type w} (T : L.Theory) (s : set α) (M : Type w') [nonempty M] [L.Structure M] [M ⊨ T] (h : (cardinal.mk ↥s).lift ≤ (cardinal.mk M).lift) :
((L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s).is_satisfiable
source
theorem first_order.language.Theory.is_satisfiable_union_distinct_constants_theory_of_infinite {L : first_order.language} {α : Type w} (T : L.Theory) (s : set α) (M : Type w') [L.Structure M] [M ⊨ T] [infinite M] :
((L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s).is_satisfiable
source
theorem first_order.language.Theory.exists_large_model_of_infinite_model {L : first_order.language} (T : L.Theory) (κ : cardinal) (M : Type w') [L.Structure M] [M ⊨ T] [infinite M] :
∃ (N : T.Model), κ.lift ≤ cardinal.mk ↥N

Any theory with an infinite model has arbitrarily large models.

source
theorem first_order.language.Theory.is_satisfiable_Union_iff_is_satisfiable_Union_finset {L : first_order.language} {ι : Type u_1} (T : ι → L.Theory) :
first_order.language.Theory.is_satisfiable (⋃ (i : ι), T i) ↔ ∀ (s : finset ι), first_order.language.Theory.is_satisfiable (⋃ (i : ι) (H : i ∈ s), T i)
source
theorem first_order.language.exists_elementary_embedding_card_eq_of_le (L : first_order.language) (M : Type w') [L.Structure M] [nonempty M] (κ : cardinal) (h1 : cardinal.aleph_0 ≤ κ) (h2 : L.card.lift ≤ κ.lift) (h3 : κ.lift ≤ (cardinal.mk M).lift) :
∃ (N : category_theory.bundled L.Structure), nonempty (L.elementary_embedding ↥N M) ∧ cardinal.mk ↥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 κ.

source
theorem first_order.language.exists_elementary_embedding_card_eq_of_ge (L : first_order.language) (M : Type w') [L.Structure M] [iM : infinite M] (κ : cardinal) (h1 : L.card.lift ≤ κ.lift) (h2 : (cardinal.mk M).lift ≤ κ.lift) :
∃ (N : category_theory.bundled L.Structure), nonempty (L.elementary_embedding M ↥N) ∧ cardinal.mk ↥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 κ.

source
theorem first_order.language.exists_elementary_embedding_card_eq (L : first_order.language) (M : Type w') [L.Structure M] [iM : infinite M] (κ : cardinal) (h1 : cardinal.aleph_0 ≤ κ) (h2 : L.card.lift ≤ κ.lift) :
∃ (N : category_theory.bundled L.Structure), (nonempty (L.elementary_embedding ↥N M) ∨ nonempty (L.elementary_embedding 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 κ.

source
theorem first_order.language.exists_elementarily_equivalent_card_eq (L : first_order.language) (M : Type w') [L.Structure M] [infinite M] (κ : cardinal) (h1 : cardinal.aleph_0 ≤ κ) (h2 : L.card.lift ≤ κ.lift) :
∃ (N : category_theory.bundled L.Structure), L.elementarily_equivalent 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.

source
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 = κ
source
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
source
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
source
theorem first_order.language.Theory.models_sentence_iff {L : first_order.language} {T : L.Theory} {φ : L.sentence} :
T ⊨ φ ↔ ∀ (M : T.Model), ↥M ⊨ φ
source
theorem first_order.language.Theory.models_sentence_of_mem {L : first_order.language} {T : L.Theory} {φ : L.sentence} (h : φ ∈ T) :
T ⊨ φ
source
theorem first_order.language.Theory.models_iff_not_satisfiable {L : first_order.language} {T : L.Theory} (φ : L.sentence) :
T ⊨ φ ↔ ¬(T ∪ {first_order.language.formula.not φ}).is_satisfiable
source
theorem first_order.language.Theory.models_bounded_formula.realize_sentence {L : first_order.language} {T : L.Theory} {φ : L.sentence} (h : T ⊨ φ) (M : Type u_1) [L.Structure M] [M ⊨ T] [nonempty M] :
M ⊨ φ
source
def first_order.language.Theory.is_complete {L : first_order.language} (T : L.Theory) :
Prop

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

Equations
source
theorem first_order.language.Theory.is_complete.models_not_iff {L : first_order.language} {T : L.Theory} (h : T.is_complete) (φ : L.sentence) :
T ⊨ first_order.language.formula.not φ ↔ ¬T ⊨ φ
source
theorem first_order.language.Theory.is_complete.realize_sentence_iff {L : first_order.language} {T : L.Theory} (h : T.is_complete) (φ : L.sentence) (M : Type u_1) [L.Structure M] [M ⊨ T] [nonempty M] :
M ⊨ φ ↔ T ⊨ φ
source
def first_order.language.Theory.is_maximal {L : first_order.language} (T : L.Theory) :
Prop

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

Equations
source
theorem first_order.language.Theory.is_maximal.is_complete {L : first_order.language} {T : L.Theory} (h : T.is_maximal) :
T.is_complete
source
theorem first_order.language.Theory.is_maximal.mem_or_not_mem {L : first_order.language} {T : L.Theory} (h : T.is_maximal) (φ : L.sentence) :
φ ∈ T ∨ first_order.language.formula.not φ ∈ T
source
theorem first_order.language.Theory.is_maximal.mem_of_models {L : first_order.language} {T : L.Theory} (h : T.is_maximal) {φ : L.sentence} (hφ : T ⊨ φ) :
φ ∈ T
source
theorem first_order.language.Theory.is_maximal.mem_iff_models {L : first_order.language} {T : L.Theory} (h : T.is_maximal) (φ : L.sentence) :
φ ∈ T ↔ T ⊨ φ
source
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
source
@[refl]
theorem first_order.language.Theory.semantically_equivalent.refl {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.bounded_formula α n) :
T.semantically_equivalent φ φ
source
@[protected, instance]
def first_order.language.Theory.semantically_equivalent.is_refl {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} :
is_refl (L.bounded_formula α n) T.semantically_equivalent
source
@[symm]
theorem first_order.language.Theory.semantically_equivalent.symm {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.bounded_formula α n} (h : T.semantically_equivalent φ ψ) :
T.semantically_equivalent ψ φ
source
@[trans]
theorem first_order.language.Theory.semantically_equivalent.trans {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.bounded_formula α n} (h1 : T.semantically_equivalent φ ψ) (h2 : T.semantically_equivalent ψ θ) :
T.semantically_equivalent φ θ
source
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
source
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
source
def first_order.language.Theory.semantically_equivalent_setoid {L : first_order.language} {α : Type w} {n : ℕ} (T : L.Theory) :
setoid (L.bounded_formula α n)

Semantic equivalence forms an equivalence relation on formulas.

Equations
source
@[protected]
theorem first_order.language.Theory.semantically_equivalent.all {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.bounded_formula α (n + 1)} (h : T.semantically_equivalent φ ψ) :
T.semantically_equivalent φ.all ψ.all
source
@[protected]
theorem first_order.language.Theory.semantically_equivalent.ex {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.bounded_formula α (n + 1)} (h : T.semantically_equivalent φ ψ) :
T.semantically_equivalent φ.ex ψ.ex
source
@[protected]
theorem first_order.language.Theory.semantically_equivalent.not {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.bounded_formula α n} (h : T.semantically_equivalent φ ψ) :
T.semantically_equivalent φ.not ψ.not
source
@[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 ψ')
source
theorem first_order.language.complete_theory.is_satisfiable (L : first_order.language) (M : Type w) [L.Structure M] [nonempty M] :
(L.complete_theory M).is_satisfiable
source
theorem first_order.language.complete_theory.mem_or_not_mem (L : first_order.language) (M : Type w) [L.Structure M] (φ : L.sentence) :
φ ∈ L.complete_theory M ∨ first_order.language.formula.not φ ∈ L.complete_theory M
source
theorem first_order.language.complete_theory.is_maximal (L : first_order.language) (M : Type w) [L.Structure M] [nonempty M] :
(L.complete_theory M).is_maximal
source
theorem first_order.language.complete_theory.is_complete (L : first_order.language) (M : Type w) [L.Structure M] [nonempty M] :
(L.complete_theory M).is_complete
source
theorem first_order.language.bounded_formula.semantically_equivalent_not_not {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.bounded_formula α n) :
T.semantically_equivalent φ φ.not.not
source
theorem first_order.language.bounded_formula.imp_semantically_equivalent_not_sup {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.bounded_formula α n) :
T.semantically_equivalent (φ.imp ψ) (φ.not ⊔ ψ)
source
theorem first_order.language.bounded_formula.sup_semantically_equivalent_not_inf_not {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.bounded_formula α n) :
T.semantically_equivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not
source
theorem first_order.language.bounded_formula.inf_semantically_equivalent_not_sup_not {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.bounded_formula α n) :
T.semantically_equivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not
source
theorem first_order.language.bounded_formula.all_semantically_equivalent_not_ex_not {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
T.semantically_equivalent φ.all φ.not.ex.not
source
theorem first_order.language.bounded_formula.ex_semantically_equivalent_not_all_not {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.bounded_formula α (n + 1)) :
T.semantically_equivalent φ.ex φ.not.all.not
source
theorem first_order.language.bounded_formula.semantically_equivalent_all_lift_at {L : first_order.language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.bounded_formula α n) :
T.semantically_equivalent φ (first_order.language.bounded_formula.lift_at 1 n φ).all
source
theorem first_order.language.formula.semantically_equivalent_not_not {L : first_order.language} {T : L.Theory} {α : Type w} (φ : L.formula α) :
T.semantically_equivalent φ φ.not.not
source
theorem first_order.language.formula.imp_semantically_equivalent_not_sup {L : first_order.language} {T : L.Theory} {α : Type w} (φ ψ : L.formula α) :
T.semantically_equivalent (φ.imp ψ) (φ.not ⊔ ψ)
source
theorem first_order.language.formula.sup_semantically_equivalent_not_inf_not {L : first_order.language} {T : L.Theory} {α : Type w} (φ ψ : L.formula α) :
T.semantically_equivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not
source
theorem first_order.language.formula.inf_semantically_equivalent_not_sup_not {L : first_order.language} {T : L.Theory} {α : Type w} (φ ψ : L.formula α) :
T.semantically_equivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not
source
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_atomic → P ψ) (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 φ
source
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_atomic → P ψ) (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 φ
source
theorem first_order.language.bounded_formula.semantically_equivalent_to_prenex {L : first_order.language} {α : Type w} {n : ℕ} (φ : L.bounded_formula α n) :
∅.semantically_equivalent φ φ.to_prenex
source
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_qf → P ψ) (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 φ
source
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_qf → P ψ) (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 φ
source
def cardinal.categorical {L : first_order.language} (κ : cardinal) (T : L.Theory) :
Prop

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

Equations
source
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) :
T.is_complete

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

source
theorem cardinal.empty_Theory_categorical (κ : cardinal) (T : first_order.language.empty.Theory) :
κ.categorical T
source
theorem cardinal.empty_infinite_Theory_is_complete  :
first_order.language.empty.infinite_theory.is_complete