English
For a maximal theory, either φ is in T or φ.not is in T.
Русский
Для максимальной теории либо φ ∈ T, либо φ.not ∈ T.
LaTeX
$$$φ \\in T \\lor φ.not \\in T$$$
Lean4
/-- 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` -/
theorem models_iff_finset_models {φ : L.Sentence} :
T ⊨ᵇ φ ↔ ∃ T0 : Finset L.Sentence, (T0 : L.Theory) ⊆ T ∧ (T0 : L.Theory) ⊨ᵇ φ :=
by
simp only [models_iff_not_satisfiable]
rw [← not_iff_not, not_not, isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
push_neg
letI := Classical.decEq (Sentence L)
constructor
· intro h T0 hT0
simpa using
h (T0 ∪ {Formula.not φ})
(by
simp only [Finset.coe_union, Finset.coe_singleton]
exact Set.union_subset_union hT0 (Set.Subset.refl _))
· intro h T0 hT0
exact IsSatisfiable.mono (h (T0.erase (Formula.not φ)) (by simpa using hT0)) (by simp)
