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

def FirstOrder.Language.Theory.IsSatisfiable {L : FirstOrder.Language} (T : L.Theory) : Prop

A theory is satisfiable if a structure models it.

Equations

• T.IsSatisfiable = Nonempty T.ModelType

def FirstOrder.Language.Theory.IsFinitelySatisfiable {L : FirstOrder.Language} (T : L.Theory) : Prop

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

Equations

• T.IsFinitelySatisfiable = ∀ (T0 : Finset L.Sentence), ↑T0 ⊆ T → FirstOrder.Language.Theory.IsSatisfiable ↑T0

theorem FirstOrder.Language.Theory.Model.isSatisfiable {L : FirstOrder.Language} {T : L.Theory} (M : Type w) [Nonempty M] [L.Structure M] [M ⊨ T] : T.IsSatisfiable

theorem FirstOrder.Language.Theory.IsSatisfiable.mono {L : FirstOrder.Language} {T : L.Theory} {T' : L.Theory} (h : T'.IsSatisfiable) (hs : T ⊆ T') : T.IsSatisfiable

theorem FirstOrder.Language.Theory.isSatisfiable_empty (L : FirstOrder.Language) : ∅.IsSatisfiable

theorem FirstOrder.Language.Theory.isSatisfiable_of_isSatisfiable_onTheory {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (h : (φ.onTheory T).IsSatisfiable) : T.IsSatisfiable

theorem FirstOrder.Language.Theory.isSatisfiable_onTheory_iff {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective) : (φ.onTheory T).IsSatisfiable ↔ T.IsSatisfiable

theorem FirstOrder.Language.Theory.IsSatisfiable.isFinitelySatisfiable {L : FirstOrder.Language} {T : L.Theory} (h : T.IsSatisfiable) : T.IsFinitelySatisfiable

theorem FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable {L : FirstOrder.Language} {T : L.Theory} : T.IsSatisfiable ↔ T.IsFinitelySatisfiable

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} [Nonempty ι] {T : ι → L.Theory} (h : Directed (fun (x1 x2 : L.Theory) => x1 ⊆ x2) T) : FirstOrder.Language.Theory.IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (i : ι), (T i).IsSatisfiable

theorem FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [Nonempty M] [L.Structure M] [M ⊨ T] (h : Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} (Cardinal.mk M)) : ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

theorem FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite {L : FirstOrder.Language} {α : Type w} (T : L.Theory) (s : Set α) (M : Type w') [L.Structure M] [M ⊨ T] [Infinite M] : ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

theorem FirstOrder.Language.Theory.exists_large_model_of_infinite_model {L : FirstOrder.Language} (T : L.Theory) (κ : Cardinal.{w}) (M : Type w') [L.Structure M] [M ⊨ T] [Infinite M] : ∃ (N : T.ModelType), Cardinal.lift.{max u v w, w} κ ≤ Cardinal.mk ↑N

Any theory with an infinite model has arbitrarily large models.

theorem FirstOrder.Language.Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset {L : FirstOrder.Language} {ι : Type u_1} (T : ι → L.Theory) : FirstOrder.Language.Theory.IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), FirstOrder.Language.Theory.IsSatisfiable (⋃ i ∈ s, T i)

theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le (L : FirstOrder.Language) (M : Type w') [L.Structure M] [Nonempty M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) (h3 : Cardinal.lift.{w', w} κ ≤ Cardinal.lift.{w, w'} (Cardinal.mk M)) : ∃ (N : CategoryTheory.Bundled L.Structure), Nonempty (L.ElementaryEmbedding (↑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 κ.

theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge (L : FirstOrder.Language) (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) (h2 : Cardinal.lift.{w, w'} (Cardinal.mk M) ≤ Cardinal.lift.{w', w} κ) : ∃ (N : CategoryTheory.Bundled L.Structure), Nonempty (L.ElementaryEmbedding 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 κ.

theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq (L : FirstOrder.Language) (M : Type w') [L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) : ∃ (N : CategoryTheory.Bundled L.Structure), (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding 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 κ.

theorem FirstOrder.Language.exists_elementarilyEquivalent_card_eq (L : FirstOrder.Language) (M : Type w') [L.Structure M] [Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) : ∃ (N : CategoryTheory.Bundled L.Structure), L.ElementarilyEquivalent 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.

theorem FirstOrder.Language.Theory.exists_model_card_eq {L : FirstOrder.Language} {T : L.Theory} (h : ∃ (M : T.ModelType), Infinite ↑M) (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) : ∃ (N : T.ModelType), Cardinal.mk ↑N = κ

def FirstOrder.Language.Theory.ModelsBoundedFormula {L : FirstOrder.Language} (T : L.Theory) {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : Prop

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

Equations

• T ⊨ᵇ φ = ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), φ.Realize v xs

def FirstOrder.Language.Theory.«term_⊨ᵇ_» : Lean.TrailingParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.Theory.models_formula_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} : T ⊨ᵇ φ ↔ ∀ (M : T.ModelType) (v : α → ↑M), φ.Realize v

theorem FirstOrder.Language.Theory.models_sentence_iff {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} : T ⊨ᵇ φ ↔ ∀ (M : T.ModelType), ↑M ⊨ φ

theorem FirstOrder.Language.Theory.models_sentence_of_mem {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} (h : φ ∈ T) : T ⊨ᵇ φ

theorem FirstOrder.Language.Theory.models_iff_not_satisfiable {L : FirstOrder.Language} {T : L.Theory} (φ : L.Sentence) : T ⊨ᵇ φ ↔ ¬(T ∪ {FirstOrder.Language.Formula.not φ}).IsSatisfiable

theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} (h : T ⊨ᵇ φ) (M : Type u_1) [L.Structure M] [M ⊨ T] [Nonempty M] : M ⊨ φ

theorem FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} : T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ FirstOrder.Language.Formula.equivSentence φ

theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_formula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} (h : T ⊨ᵇ φ) (M : Type u_1) [L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M} : φ.Realize v

theorem FirstOrder.Language.Theory.models_toFormula_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} : T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} (h : T ⊨ᵇ φ) (M : Type u_1) [L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M} {xs : Fin n → M} : φ.Realize v xs

theorem FirstOrder.Language.Theory.models_of_models_theory {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {T' : L.Theory} (h : ∀ φ ∈ T', T ⊨ᵇ φ) {φ : L.Formula α} (hφ : T' ⊨ᵇ φ) : T ⊨ᵇ φ

theorem FirstOrder.Language.Theory.models_iff_finset_models {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence} : T ⊨ᵇ φ ↔ ∃ (T0 : Finset L.Sentence), ↑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

def FirstOrder.Language.Theory.IsComplete {L : FirstOrder.Language} (T : L.Theory) : Prop

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

Equations

• T.IsComplete = (T.IsSatisfiable ∧ ∀ (φ : L.Sentence), T ⊨ᵇ φ ∨ T ⊨ᵇ FirstOrder.Language.Formula.not φ)

theorem FirstOrder.Language.Theory.IsComplete.models_not_iff {L : FirstOrder.Language} {T : L.Theory} (h : T.IsComplete) (φ : L.Sentence) : T ⊨ᵇ FirstOrder.Language.Formula.not φ ↔ ¬T ⊨ᵇ φ

theorem FirstOrder.Language.Theory.IsComplete.realize_sentence_iff {L : FirstOrder.Language} {T : L.Theory} (h : T.IsComplete) (φ : L.Sentence) (M : Type u_1) [L.Structure M] [M ⊨ T] [Nonempty M] : M ⊨ φ ↔ T ⊨ᵇ φ

def FirstOrder.Language.Theory.IsMaximal {L : FirstOrder.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

• T.IsMaximal = (T.IsSatisfiable ∧ ∀ (φ : L.Sentence), φ ∈ T ∨ FirstOrder.Language.Formula.not φ ∈ T)

theorem FirstOrder.Language.Theory.IsMaximal.isComplete {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) : T.IsComplete

theorem FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) (φ : L.Sentence) : φ ∈ T ∨ FirstOrder.Language.Formula.not φ ∈ T

theorem FirstOrder.Language.Theory.IsMaximal.mem_of_models {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) {φ : L.Sentence} (hφ : T ⊨ᵇ φ) : φ ∈ T

theorem FirstOrder.Language.Theory.IsMaximal.mem_iff_models {L : FirstOrder.Language} {T : L.Theory} (h : T.IsMaximal) (φ : L.Sentence) : φ ∈ T ↔ T ⊨ᵇ φ

theorem FirstOrder.Language.completeTheory.isSatisfiable (L : FirstOrder.Language) (M : Type w) [L.Structure M] [Nonempty M] : (L.completeTheory M).IsSatisfiable

theorem FirstOrder.Language.completeTheory.mem_or_not_mem (L : FirstOrder.Language) (M : Type w) [L.Structure M] (φ : L.Sentence) : φ ∈ L.completeTheory M ∨ FirstOrder.Language.Formula.not φ ∈ L.completeTheory M

theorem FirstOrder.Language.completeTheory.isMaximal (L : FirstOrder.Language) (M : Type w) [L.Structure M] [Nonempty M] : (L.completeTheory M).IsMaximal

theorem FirstOrder.Language.completeTheory.isComplete (L : FirstOrder.Language) (M : Type w) [L.Structure M] [Nonempty M] : (L.completeTheory M).IsComplete

def Cardinal.Categorical {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : L.Theory) : Prop

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

Equations

• κ.Categorical T = ∀ (M N : T.ModelType), Cardinal.mk ↑M = κ → Cardinal.mk ↑N = κ → Nonempty (L.Equiv ↑M ↑N)

theorem Cardinal.Categorical.isComplete {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : L.Theory) (h : κ.Categorical T) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ) (hS : T.IsSatisfiable) (hT : ∀ (M : T.ModelType), Infinite ↑M) : T.IsComplete

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

theorem Cardinal.empty_theory_categorical (κ : Cardinal.{w}) (T : FirstOrder.Language.empty.Theory) : κ.Categorical T

theorem Cardinal.empty_infinite_Theory_isComplete : FirstOrder.Language.empty.infiniteTheory.IsComplete