FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable
theorem FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable :
∀ {L : FirstOrder.Language} {T : L.Theory}, T.IsSatisfiable ↔ T.IsFinitelySatisfiable
This is the Compactness Theorem of first-order logic: for any first-order language `L` and any theory `T` over that language, `T` is satisfiable (there exists a structure that models it) if and only if `T` is finitely satisfiable (every finite subset of `T` has a model). This theorem is a cornerstone of model theory and has profound implications in the study of formal systems.
More concisely: A first-order theory is satisfiable if and only if every finite subset of it is satisfiable.
|
Cardinal.Categorical.isComplete
theorem Cardinal.Categorical.isComplete :
∀ {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : L.Theory),
κ.Categorical T →
Cardinal.aleph0 ≤ κ →
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
T.IsSatisfiable → (∀ (M : T.ModelType), Infinite ↑M) → T.IsComplete
The theorem `Cardinal.Categorical.isComplete` states the Łoś–Vaught Test, providing a criterion for a categorical theory to be complete. Specifically, given a first-order language `L`, a cardinal number `κ`, and a `L` theory `T`, if `T` is categorical in `κ`, `κ` is greater than or equal to the smallest infinite cardinal (`Cardinal.aleph0`), the cardinality of `L` after universe lifting is less than or equal to `κ` after universe lifting, `T` is satisfiable, and every model type `M` of `T` is infinite, then `T` is complete. Completeness here means any Cauchy filter `f` such that `T` is in `f` has a limit in `T`.
More concisely: A first-order theory `T` in a language `L` is complete if it is categorical, satisfiable, and every model of `T` is infinite, assuming `L`'s cardinality after universe lifting is less than or equal to the infinite cardinal `κ`, `κ` is greater than or equal to `Cardinal.aleph0`, and `T` is satisfiable in a structure of size `κ`.
|
FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge
theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge :
∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}),
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
Cardinal.lift.{w, w'} (Cardinal.mk M) ≤ Cardinal.lift.{w', w} κ →
∃ N, Nonempty (L.ElementaryEmbedding M ↑N) ∧ Cardinal.mk ↑N = κ
The theorem, known as the "Upward Löwenheim–Skolem Theorem", states that for any first-order language `L` and an infinite `L`-structure `M`, if `κ` is a cardinal number greater than or equal to the cardinalities of `L` and `M` (when lifted to the appropriate universes), then there exists an `L`-structure `N` and an elementary embedding from `M` into `N` such that the cardinality of `N` is `κ`. In other words, any sufficiently large infinite `L`-structure `M` can be embedded into a larger `L`-structure `N` of any given cardinality `κ`.
More concisely: For any first-order language `L` and infinite `L`-structure `M`, there exists an `L`-structure `N` of greater cardinality and an elementary embedding from `M` into `N`.
|
FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le
theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le :
∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [inst_1 : Nonempty M] (κ : Cardinal.{w}),
Cardinal.aleph0 ≤ κ →
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
Cardinal.lift.{w', w} κ ≤ Cardinal.lift.{w, w'} (Cardinal.mk M) →
∃ N, Nonempty (L.ElementaryEmbedding (↑N) M) ∧ Cardinal.mk ↑N = κ
This theorem, known as a version of The Downward Löwenheim–Skolem theorem, states that for any first-order language `L` and any structure `M` of that language, if `M` is nonempty and there exists a cardinal number `κ` such that `κ` is not smaller than the smallest infinite cardinal (ℵ₀), the cardinality of `L` lifted to the maximum of universe levels `u` and `v` is not greater than `κ` lifted to the same universe, and `κ` lifted to the universe level `w'` is not greater than the cardinality of `M` lifted to the same universe, then there exists a structure `N` which elementarily embeds into `M` and whose cardinality is exactly `κ`. This theorem essentially asserts that a larger structure can always have a substructure of any smaller cardinality which still preserves the elementary properties of the original structure.
More concisely: Given a first-order language `L` and a nonempty structure `M` with cardinality smaller than any infinite cardinality strictly greater than the smallest infinite cardinal (ℵ₀), there exists an elementary substructure `N` of `M` with the same infinite cardinality.
|
FirstOrder.Language.exists_elementaryEmbedding_card_eq
theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq :
∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}),
Cardinal.aleph0 ≤ κ →
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
∃ N, (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding M ↑N)) ∧ Cardinal.mk ↑N = κ
The Löwenheim–Skolem Theorem: For any first-order language `L` and any infinite `L`-structure `M` of type `w'`, and for any cardinal `κ` in `Type w` that is greater than or equal to the smallest infinite cardinal (`Cardinal.aleph0`) and larger than the cardinality of `L` after lifting its universe, there exists another structure `N` such that there is an elementary embedding from `N` to `M` or `M` to `N`, and the cardinality of `N` is `κ`. In other words, if we have an infinite model of a theory, then for any infinite cardinal, we can find another model of the same theory that has that cardinality.
More concisely: For any infinite first-order model `M` of cardinality smaller than `κ` in a given language `L`, there exists an elementary embeddable `L`-structure `N` of cardinality `κ`.
|
FirstOrder.Language.Theory.models_iff_finset_models
theorem FirstOrder.Language.Theory.models_iff_finset_models :
∀ {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence}, T.ModelsBoundedFormula φ ↔ ∃ T0, ↑T0 ⊆ T ∧ ↑T0 ⊨ᵇ φ
This theorem is an alternative statement of the Compactness Theorem in first-order logic. It states that for any first-order language `L`, theory `T` in `L`, and sentence `φ` in `L`, the theory `T` models the bounded formula `φ` if and only if there exists a finite subset `T0` of the theory `T` such that `T0` models the bounded formula `φ`. In other words, a sentence is true in a theory if it is true in some finite subset of that theory.
More concisely: For any first-order language, theory, and bounded formula, a theory models the formula if and only if some finite subset of the theory does.
|
FirstOrder.Language.Theory.Model.isSatisfiable
theorem FirstOrder.Language.Theory.Model.isSatisfiable :
∀ {L : FirstOrder.Language} {T : L.Theory} (M : Type w) [inst : Nonempty M] [inst : L.Structure M] [inst : M ⊨ T],
T.IsSatisfiable
This theorem states that for any first-order language `L` and any theory `T` over that language, if there exists a type `M` such that `M` is nonempty, `M` is a structure for the language `L`, and `M` models the theory `T`, then the theory `T` is satisfiable. In other words, if we have a structure that correctly interprets all the sentences in a theory, then it is possible to find a model for that theory, thus proving its satisfiability.
More concisely: If a first-order theory over a language has a model, then the theory is satisfiable.
|
FirstOrder.Language.Theory.models_sentence_iff
theorem FirstOrder.Language.Theory.models_sentence_iff :
∀ {L : FirstOrder.Language} {T : L.Theory} {φ : L.Sentence},
T.ModelsBoundedFormula φ ↔ ∀ (M : T.ModelType), ↑M ⊨ φ
This theorem states that for any first-order language `L`, any theory `T` of `L`, and any sentence `φ` of `L`, that theory `T` semantically entails sentence `φ` if and only if for every model `M` of the theory `T`, `M` also semantically entails `φ`. In other words, if `φ` is entailed by a theory, then `φ` must be true in every model of the theory. On the other hand, if `φ` is true in every model of the theory, then it must also be entailed by the theory.
More concisely: For any first-order language L, theory T, and sentence φ in L, T semantically entails φ if and only if every model M of T satisfies φ.
|
FirstOrder.Language.Theory.IsSatisfiable.mono
theorem FirstOrder.Language.Theory.IsSatisfiable.mono :
∀ {L : FirstOrder.Language} {T T' : L.Theory}, T'.IsSatisfiable → T ⊆ T' → T.IsSatisfiable
This theorem states that for any first-order language `L`, and for any two theories `T` and `T'` of `L`, if `T'` is satisfiable and `T` is a subset of `T'`, then `T` is also satisfiable. In other words, if a larger theory (in terms of inclusion of sentences) has a structure that models it, then any of its smaller subsets also have a structure that models them.
More concisely: If `T` is a subset of satisfiable theory `T'` in a first-order language `L`, then `T` is also satisfiable.
|
FirstOrder.Language.Theory.models_iff_not_satisfiable
theorem FirstOrder.Language.Theory.models_iff_not_satisfiable :
∀ {L : FirstOrder.Language} {T : L.Theory} (φ : L.Sentence),
T.ModelsBoundedFormula φ ↔ ¬(T ∪ {FirstOrder.Language.Formula.not φ}).IsSatisfiable
The theorem `FirstOrder.Language.Theory.models_iff_not_satisfiable` in Lean 4, states that for any First-Order Language `L` and any theory `T` of that language, along with a sentence `φ` of that language, `T` models `φ` if and only if the theory that includes `T` and the negation of `φ` is not satisfiable. In simpler terms, a sentence is true in a theory if there is no model where both the theory and the negation of the sentence hold.
More concisely: For any First-Order language L, theory T, and sentence φ in L, T models φ if and only if the theory T ∪ {~φ} is unsatisfiable. (Here, {~φ} denotes the set containing the negation of φ.)
|
FirstOrder.Language.exists_elementarilyEquivalent_card_eq
theorem FirstOrder.Language.exists_elementarilyEquivalent_card_eq :
∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [inst_1 : Infinite M] (κ : Cardinal.{w}),
Cardinal.aleph0 ≤ κ →
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
∃ N, L.ElementarilyEquivalent M ↑N ∧ Cardinal.mk ↑N = κ
This theorem is a consequence of the Löwenheim–Skolem Theorem in the field of mathematical logic. It states that for any language `L` and an infinite `L`-structure `M`, if there exists a cardinal `κ` that is greater than the cardinalities of `L` and `M` and at least as large as aleph-zero (the smallest infinite cardinal), then there exists a structure `N` with cardinality `κ` that is elementarily equivalent to `M`. This means that `M` and `N` satisfy the same first-order sentences in the language `L`.
More concisely: For any infinite `L`-structure `M` and cardinal `κ` greater than or equal to the cardinalities of `L` and aleph-zero, there exists an `L`-structure `N` of cardinality `κ` that is elementarily equivalent to `M`.
|
FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff
theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff :
∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n} {M : Type (max u v)}
[inst : Nonempty M] [inst : L.Structure M] [inst_1 : M ⊨ T],
T.SemanticallyEquivalent φ ψ → ∀ {v : α → M} {xs : Fin n → M}, φ.Realize v xs ↔ ψ.Realize v xs
This theorem states that for any first-order language `L`, a theory `T` of `L`, a type `α`, a natural number `n`, two bounded formulas `φ` and `ψ` of `L` over `α` of length `n`, a type `M`, and given that `M` is nonempty, `M` is a structure of `L`, and `M` is a model of `T`, if `φ` and `ψ` are semantically equivalent over `T`, then for any valuation `v` from `α` to `M` and any sequence `xs` of length `n` in `M`, the bounded formulas `φ` and `ψ` are realized in the same way, i.e., the realization of `φ` with `v` and `xs` is equivalent to the realization of `ψ` with `v` and `xs`. In other words, if two formulas are semantically equivalent in a theory, they evaluate to the same truth value under any interpretation in any model of the theory.
More concisely: For any first-order language L, theory T, type α, natural number n, nonempty type M model of T, valuation v from α to M, sequence xs of length n in M, and bounded formulas φ and ψ of L over α of length n that are semantically equivalent over T, their realizations with v and xs are equivalent.
|
FirstOrder.Language.completeTheory.isMaximal
theorem FirstOrder.Language.completeTheory.isMaximal :
∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] [inst_1 : Nonempty M],
(L.completeTheory M).IsMaximal
The theorem `FirstOrder.Language.completeTheory.isMaximal` states that for any first-order language `L` and any type `M` that has a `FirstOrder.Language.Structure` instance, and assuming that `M` is not empty, the complete theory of `M` in `L` is a maximal theory. In other words, the complete theory of `M` in `L` is satisfiable and for every sentence `φ` in `L`, either `φ` or its negation is in the theory. This captures the notion that a complete theory includes every possible statement or its negation for a given language and structure.
More concisely: Given a non-empty first-order structure `M` in a first-order language `L`, the complete theory of `M` in `L` is a maximal consistent theory.
|
Mathlib.ModelTheory.Satisfiability._auxLemma.16
theorem Mathlib.ModelTheory.Satisfiability._auxLemma.16 :
∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
{v : α → M} {xs : Fin l → M}, (φ.iff ψ).Realize v xs = (φ.Realize v xs ↔ ψ.Realize v xs)
This theorem states that for any first-order language `L`, structure `M`, a type `α`, a natural number `l`, two bounded formulas `φ` and `ψ` of the language `L`, a function `v` from `α` to `M`, and a function `xs` from the finite sequence of length `l` to `M`, the realization of the biimplication (logical equivalence) of the bounded formulas `φ` and `ψ` given the functions `v` and `xs` is equivalent to the biimplication (logical equivalence) of the realizations of `φ` and `ψ` given the same functions. In other words, the realization process preserves logical equivalence between two formulas in a first-order language.
More concisely: For any first-order language L, structure M, type α, natural number l, functions v : α -> M, xs : fin l -> M, and bounded formulas φ and ψ of L, the realizability of φ iff ψ given v and xs is equivalent to φ(v, xs) iff ψ(v, xs).
|
FirstOrder.Language.Theory.exists_large_model_of_infinite_model
theorem FirstOrder.Language.Theory.exists_large_model_of_infinite_model :
∀ {L : FirstOrder.Language} (T : L.Theory) (κ : Cardinal.{w}) (M : Type w') [inst : L.Structure M] [inst : M ⊨ T]
[inst : Infinite M], ∃ N, Cardinal.lift.{max u v w, w} κ ≤ Cardinal.mk ↑N
This theorem states that for any first order language `L` and any theory `T` in this language, if `M` is a type that serves as an infinite model of this theory (i.e., `M` satisfies all statements in the theory `T`), then there exists a larger model `N` such that the cardinality of `N` (possibly lifted to a larger universe) is greater or equal to a given cardinal number `κ`. Essentially, if there is an infinite model of a theory, we can find models of the theory that are arbitrarily large.
More concisely: If `L` is a first-order language and `T` is a theory in `L` with an infinite model `M`, then there exists a larger model `N` of `T` with cardinality greater than or equal to a given cardinal number `κ`.
|