Lagmental Vicfred

Compactness Reduces Infinite Satisfiability to Finite Pieces by Vicfred

tags: mathematics, mathematical logic, model theory, compactness

A first-order theory has a model exactly when every finite subtheory has a model. A small computation will anchor the general statement before the abstraction takes over.

Objects and notation

A first-order language \(\mathcal L\) supplies symbols, formulas, and structures. Semantic consequence \(T\models\varphi\) is truth in every model, while provability \(T\vdash\varphi\) is a finite formal derivation.

$$ T\ \text{a set of first-order sentences} $$

The typography mirrors the proof: first declare \(\mathsf D\), then state \(\mathsf C\). The symbol \(\Longrightarrow\) below is a logical dependency, not extra mathematical structure.

$$ T\ \text{satisfiable}\Longleftrightarrow\forall T_0\subseteq_{\mathrm{fin}}T,\ T_0\ \text{satisfiable} $$

Push the symbols

The following line is the smallest calculation that still exercises the mechanism. It keeps nested delimiters and the order of operations explicit.

$$ T=\{c>n:n\in\mathbf N\}\cup\operatorname{Th}(\mathbf N)\quad\Longrightarrow\quad\mathcal M\models T\ \text{has an element }c^\mathcal M\text{ larger than every standard numeral} $$

Structural reading

A good test for understanding is to change the presentation while keeping the invariant fixed. The aligned form makes that comparison unusually easy.

$$ \begin{aligned} \mathsf{D}\;&:\quad T\ \text{a set of first-order sentences},\\[5pt] \mathsf{C}\;&:\quad T\ \text{satisfiable}\Longleftrightarrow\forall T_0\subseteq_{\mathrm{fin}}T,\ T_0\ \text{satisfiable}. \end{aligned} $$

A hypothesis worth keeping

First-order compactness does not apply to arbitrary second-order properties. Finiteness and categorical characterization of the natural numbers lie beyond its direct reach.

$$ \boxed{\begin{gathered} \text{compact conclusion}\\[-2pt] T\ \text{satisfiable}\Longleftrightarrow\forall T_0\subseteq_{\mathrm{fin}}T,\ T_0\ \text{satisfiable} \end{gathered}} $$

The result is compact enough to reuse without pretending that the caveat has disappeared. The worked line remains the quickest consistency check.

This article was posted on Sat 15 November 2014. Facts and circumstances may have changed since publication.
Please contact me before jumping to conclusions if something seems wrong or unclear.