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 : FirstOrder.Language.Theory L) : Prop

A theory is satisfiable if a structure models it.

Equations

• FirstOrder.Language.Theory.IsSatisfiable T = Nonempty (FirstOrder.Language.Theory.ModelType T)

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

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

Equations

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

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

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

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

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

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

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

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

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 : ι → FirstOrder.Language.Theory L} (h : Directed (fun (x x_1 : FirstOrder.Language.Theory L) => x ⊆ x_1) T) : FirstOrder.Language.Theory.IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (i : ι), FirstOrder.Language.Theory.IsSatisfiable (T i)

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

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

theorem FirstOrder.Language.Theory.exists_large_model_of_infinite_model {L : FirstOrder.Language} (T : FirstOrder.Language.Theory L) (κ : Cardinal.{w}) (M : Type w') [FirstOrder.Language.Structure L M] [M ⊨ T] [Infinite M] : ∃ (N : FirstOrder.Language.Theory.ModelType T), 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 : ι → FirstOrder.Language.Theory L) : 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') [FirstOrder.Language.Structure L M] [Nonempty M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} (FirstOrder.Language.card L) ≤ Cardinal.lift.{max u v, w} κ) (h3 : Cardinal.lift.{w', w} κ ≤ Cardinal.lift.{w, w'} (Cardinal.mk M)) : ∃ (N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), Nonempty (FirstOrder.Language.ElementaryEmbedding L (↑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') [FirstOrder.Language.Structure L M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.lift.{w, max u v} (FirstOrder.Language.card L) ≤ Cardinal.lift.{max u v, w} κ) (h2 : Cardinal.lift.{w, w'} (Cardinal.mk M) ≤ Cardinal.lift.{w', w} κ) : ∃ (N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), Nonempty (FirstOrder.Language.ElementaryEmbedding L 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') [FirstOrder.Language.Structure L M] [iM : Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} (FirstOrder.Language.card L) ≤ Cardinal.lift.{max u v, w} κ) : ∃ (N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), (Nonempty (FirstOrder.Language.ElementaryEmbedding L (↑N) M) ∨ Nonempty (FirstOrder.Language.ElementaryEmbedding L 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') [FirstOrder.Language.Structure L M] [Infinite M] (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} (FirstOrder.Language.card L) ≤ Cardinal.lift.{max u v, w} κ) : ∃ (N : CategoryTheory.Bundled (FirstOrder.Language.Structure L)), FirstOrder.Language.ElementarilyEquivalent L 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 : FirstOrder.Language.Theory L} (h : ∃ (M : FirstOrder.Language.Theory.ModelType T), Infinite ↑M) (κ : Cardinal.{w}) (h1 : Cardinal.aleph0 ≤ κ) (h2 : Cardinal.lift.{w, max u v} (FirstOrder.Language.card L) ≤ Cardinal.lift.{max u v, w} κ) : ∃ (N : FirstOrder.Language.Theory.ModelType T), Cardinal.mk ↑N = κ

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

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

Equations

• T ⊨ᵇ φ = ∀ (M : FirstOrder.Language.Theory.ModelType T) (v : α → ↑M) (xs : Fin n → ↑M), FirstOrder.Language.BoundedFormula.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 : FirstOrder.Language.Theory L} {α : Type w} {φ : FirstOrder.Language.Formula L α} : T ⊨ᵇ φ ↔ ∀ (M : FirstOrder.Language.Theory.ModelType T) (v : α → ↑M), FirstOrder.Language.Formula.Realize φ v

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

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

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

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

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

• FirstOrder.Language.Theory.SemanticallyEquivalent T φ ψ = T ⊨ᵇ FirstOrder.Language.BoundedFormula.iff φ ψ

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

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

Equations

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

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

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

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

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

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

Semantic equivalence forms an equivalence relation on formulas.

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

theorem Cardinal.empty_infinite_Theory_isComplete : FirstOrder.Language.Theory.IsComplete (FirstOrder.Language.infiniteTheory FirstOrder.Language.empty)