# 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:*
1. If Γ ⊨ φ, then Γ₀ ⊨ φ for some finite Γ₀ ⊆ Γ.
2. 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.

© 2026 Lingenic LLC