English
If a theory is satisfiable, then it is finitely satisfiable.
Русский
Если теория удовлетворима, то она удовлетворима для некоторых конечных подмножеств.
LaTeX
$$$$ T.IsSatisfiable \\Rightarrow T.IsFinitelySatisfiable. $$$$
Lean4
/-- The **Compactness Theorem of first-order logic**: A theory is satisfiable if and only if it is
finitely satisfiable. -/
theorem isSatisfiable_iff_isFinitelySatisfiable {T : L.Theory} : T.IsSatisfiable ↔ T.IsFinitelySatisfiable :=
⟨Theory.IsSatisfiable.isFinitelySatisfiable, fun h => by
classical
set M : Finset T → Type max u v := fun T0 : Finset T =>
(h (T0.map (Function.Embedding.subtype fun x => x ∈ T)) T0.map_subtype_subset).some.Carrier
let M' := Filter.Product (Ultrafilter.of (Filter.atTop : Filter (Finset T))) M
have h' : M' ⊨ T := by
refine ⟨fun φ hφ => ?_⟩
rw [Ultraproduct.sentence_realize]
refine
Filter.Eventually.filter_mono (Ultrafilter.of_le _)
(Filter.eventually_atTop.2
⟨{⟨φ, hφ⟩}, fun s h' =>
Theory.realize_sentence_of_mem (s.map (Function.Embedding.subtype fun x => x ∈ T)) ?_⟩)
simp only [Finset.coe_map, Function.Embedding.coe_subtype, Set.mem_image, Finset.mem_coe, Subtype.exists,
exists_and_right, exists_eq_right]
exact ⟨hφ, h' (Finset.mem_singleton_self _)⟩
exact ⟨ModelType.of T M'⟩⟩
