Compactness

Origin. Gödel completeness theorem (1929) implies compactness. Fundamental model-theoretic property. If every finite subset satisfiable, whole set satisfiable. Fails for many extensions.

Models. Γ is satisfiable iff every finite Γ₀ ⊆ Γ is satisfiable. Equivalently: if Γ ⊨ φ, then Γ₀ ⊨ φ for finite Γ₀. Topological: theory space is compact.

Formalism.

Compactness theorem: For any set Γ of first-order sentences: Γ has a model iff every finite Γ₀ ⊆ Γ has a model.

Equivalent forms:

If Γ ⊨ φ, then Γ₀ ⊨ φ for some finite Γ₀ ⊆ Γ.
If Γ is unsatisfiable, some finite Γ₀ ⊆ Γ is unsatisfiable.

Proof via completeness: Γ ⊨ φ implies Γ ⊢ φ (completeness). Proofs are finite, use only finite Γ₀.

Ultraproduct proof: Direct construction via ultraproducts. Łoś's theorem: ultraproducts preserve truth.

Applications: Nonstandard models: infinite numbers. Transfer principles. Omitting types. Finite satisfiability ≠ satisfiability.

Failures: Second-order logic: fails. Infinitary logics Lω₁ω: fails. Fixed-point logics: fails. Compactness ↔ not too expressive.

Lindström's theorem: FOL is maximal logic with compactness + Löwenheim-Skolem.

Symbols.

Symbol	Unicode	Name	Meaning
Γ	U+0393	Theory	Set of formulas
⊨	U+22A8	Models	Semantic consequence
Γ₀	—	Finite subset	Part of theory
ℵ₀	U+2135	Aleph-null	Countable

Metatheory. Equivalent to completeness (via proof finiteness). Implies Löwenheim-Skolem. Nonstandard analysis. Abstract model theory.

Applies to. Model theory. Nonstandard methods. Database theory. Satisfiability solving. Logic design.

Limitations. Cannot express "finitely many." Nonstandard models. Limits expressiveness. Extension logics lose it.