FirstOrder.Language.Theory.CompleteType.isMaximal
theorem FirstOrder.Language.Theory.CompleteType.isMaximal :
∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α),
FirstOrder.Language.Theory.IsMaximal ↑p
This theorem states that for any first-order language `L`, any theory `T` of the language `L`, and any type `α`, if `p` is a complete type of the theory `T` over the type `α`, then `p` is also a maximal theory. A maximal theory is defined as a theory that is satisfiable and includes either any given sentence or its negation.
More concisely: For any first-order language L, theory T, and type α in L, if type p of theory T over α is complete, then p is a maximal theory.
|
FirstOrder.Language.Theory.CompleteType.subset
theorem FirstOrder.Language.Theory.CompleteType.subset :
∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α),
(L.lhomWithConstants α).onTheory T ⊆ ↑p
This theorem asserts that for any First-Order language `L`, any theory `T` of `L`, and any type `α`, if `p` is a complete type of the theory `T` over the type `α`, then the set of sentences in `T` after mapping its symbols via the language map that adds constants from `α` to `L` (done by `FirstOrder.Language.lhomWithConstants L α`) is a subset of `p`. In other words, any sentence in the theory `T` that's extended with constants from another type `α` can be found in the complete type `p` of the theory `T` over `α`.
More concisely: For any First-Order language L, theory T of L, and type α, if p is a complete type of T over α, then the set of sentences in T after extending its constants to α is included in p.
|