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.

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 (x x_1 : L.Theory) => x ⊆ x_1) 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_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 ⊨ᵇ φ

def FirstOrder.Language.Theory.SemanticallyEquivalent {L : FirstOrder.Language} {α : Type w} {n : ℕ} (T : L.Theory) (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α 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

• T.SemanticallyEquivalent φ ψ = T ⊨ᵇ φ.iff ψ

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.refl {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.SemanticallyEquivalent φ φ

instance FirstOrder.Language.Theory.instIsReflBoundedFormulaSemanticallyEquivalent {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} : IsRefl (L.BoundedFormula α n) T.SemanticallyEquivalent

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.symm {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent ψ φ

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.trans {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {θ : L.BoundedFormula α n} (h1 : T.SemanticallyEquivalent φ ψ) (h2 : T.SemanticallyEquivalent ψ θ) : T.SemanticallyEquivalent φ θ

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {M : Type (max u v)} [Nonempty M] [L.Structure M] [M ⊨ T] (h : T.SemanticallyEquivalent φ ψ) {v : α → M} {xs : Fin n → M} : φ.Realize v xs ↔ ψ.Realize v xs

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {φ : L.Formula α} {ψ : L.Formula α} {M : Type (max u v)} [Nonempty M] [L.Structure M] (_hM : M ⊨ T) (h : T.SemanticallyEquivalent φ ψ) {v : α → M} : φ.Realize v ↔ ψ.Realize v

def FirstOrder.Language.Theory.semanticallyEquivalentSetoid {L : FirstOrder.Language} {α : Type w} {n : ℕ} (T : L.Theory) : Setoid (L.BoundedFormula α n)

Semantic equivalence forms an equivalence relation on formulas.

Equations

• T.semanticallyEquivalentSetoid = { r := T.SemanticallyEquivalent, iseqv := ⋯ }

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.all {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} {ψ : L.BoundedFormula α (n + 1)} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent φ.all ψ.all

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.ex {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α (n + 1)} {ψ : L.BoundedFormula α (n + 1)} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent φ.ex ψ.ex

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) : T.SemanticallyEquivalent φ.not ψ.not

theorem FirstOrder.Language.Theory.SemanticallyEquivalent.imp {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n} {ψ : L.BoundedFormula α n} {φ' : L.BoundedFormula α n} {ψ' : L.BoundedFormula α n} (h : T.SemanticallyEquivalent φ ψ) (h' : T.SemanticallyEquivalent φ' ψ') : T.SemanticallyEquivalent (φ.imp φ') (ψ.imp ψ')

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

theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_not_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.SemanticallyEquivalent φ φ.not.not

theorem FirstOrder.Language.BoundedFormula.imp_semanticallyEquivalent_not_sup {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.SemanticallyEquivalent (φ.imp ψ) (φ.not ⊔ ψ)

theorem FirstOrder.Language.BoundedFormula.sup_semanticallyEquivalent_not_inf_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.SemanticallyEquivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not

theorem FirstOrder.Language.BoundedFormula.inf_semanticallyEquivalent_not_sup_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α n) : T.SemanticallyEquivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not

theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : T.SemanticallyEquivalent φ.all φ.not.ex.not

theorem FirstOrder.Language.BoundedFormula.ex_semanticallyEquivalent_not_all_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α (n + 1)) : T.SemanticallyEquivalent φ.ex φ.not.all.not

theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_all_liftAt {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : T.SemanticallyEquivalent φ (FirstOrder.Language.BoundedFormula.liftAt 1 n φ).all

theorem FirstOrder.Language.Formula.semanticallyEquivalent_not_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) : T.SemanticallyEquivalent φ φ.not.not

theorem FirstOrder.Language.Formula.imp_semanticallyEquivalent_not_sup {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) : T.SemanticallyEquivalent (φ.imp ψ) (φ.not ⊔ ψ)

theorem FirstOrder.Language.Formula.sup_semanticallyEquivalent_not_inf_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) : T.SemanticallyEquivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not

theorem FirstOrder.Language.Formula.inf_semanticallyEquivalent_not_sup_not {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (φ : L.Formula α) (ψ : L.Formula α) : T.SemanticallyEquivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not

theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not {L : FirstOrder.Language} {α : Type w} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ⊥) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) (hsup : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊔ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not {L : FirstOrder.Language} {α : Type w} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n} (h : φ.IsQF) (hf : P ⊥) (ha : ∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) (hinf : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) (hnot : ∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) (hse : ∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_toPrenex {L : FirstOrder.Language} {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n) : ∅.SemanticallyEquivalent φ φ.toPrenex

theorem FirstOrder.Language.BoundedFormula.induction_on_all_ex {L : FirstOrder.Language} {α : Type w} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n) (hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) (hall : ∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all) (hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) (hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

theorem FirstOrder.Language.BoundedFormula.induction_on_exists_not {L : FirstOrder.Language} {α : Type w} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop} (φ : L.BoundedFormula α n) (hqf : ∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) (hnot : ∀ {m : ℕ} {φ : L.BoundedFormula α m}, P φ → P φ.not) (hex : ∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) (hse : ∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.SemanticallyEquivalent φ₁ φ₂ → (P φ₁ ↔ P φ₂)) : P φ

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