Predicate Logic - Applications

TheoremCompactness Theorem for First-Order Logic

A set $\Gamma$ of first-order sentences has a model if and only if every finite subset of $\Gamma$ has a model.

Equivalently: If $\Gamma \models \phi$ , then there exists a finite subset $\Gamma_0 \subseteq \Gamma$ such that $\Gamma_0 \models \phi$ .

The compactness theorem is a powerful tool with surprising applications throughout mathematics. It follows from Gödel's completeness theorem: if every finite subset of $\Gamma$ is consistent (has a model), then $\Gamma$ itself is consistent (cannot prove a contradiction), hence by completeness, $\Gamma$ has a model.

ExampleNon-Standard Models of Arithmetic

Consider Peano arithmetic PA with the standard axioms for $0, S, +, \times$ plus the induction schema. Add new sentences:

\Gamma = \text{PA} \cup \{c > 0, c > S(0), c > S(S(0)), \ldots\}

where $c$ is a new constant. Every finite subset of $\Gamma$ has a model (the standard natural numbers with $c$ interpreted as a sufficiently large number). By compactness, $\Gamma$ has a model $\mathcal{M}$ .

In $\mathcal{M}$ , the element $c^\mathcal{M}$ is greater than all standard natural numbers—it's an "infinite" element. This proves the existence of non-standard models of arithmetic containing elements that are infinite from the standard perspective.

TheoremLöwenheim-Skolem Theorem (Downward)

If a countable first-order theory $T$ has an infinite model, then $T$ has a countable model.

This theorem has a paradoxical flavor: even theories that describe uncountable structures (like set theory with uncountably many sets) must have countable models. This is Skolem's paradox—the resolution is that "uncountable" is a relative notion defined within each model.

TheoremLöwenheim-Skolem Theorem (Upward)

If a first-order theory $T$ in a countable language has an infinite model, then for every infinite cardinal $\kappa$ , $T$ has a model of cardinality $\kappa$ .

ExampleApplication to Graph Theory

Consider the theory of infinite graphs with arbitrarily large finite cliques:

T = \{\text{"$G$ is a graph"}\} \cup \{\text{"$G$ has a clique of size $n$"} : n \in \mathbb{N}\}

Every finite subset is satisfiable (take a large enough complete graph). By compactness, $T$ has a model—an infinite graph with arbitrarily large cliques. By the upward Löwenheim-Skolem theorem, such graphs exist in all infinite cardinalities.

TheoremCraig's Interpolation Theorem

If $\phi \models \psi$ in first-order logic, then there exists a formula $\chi$ (the interpolant) such that:

$\phi \models \chi$ and $\chi \models \psi$
Every non-logical symbol in $\chi$ appears in both $\phi$ and $\psi$

The interpolant $\chi$ uses only the "common vocabulary" of $\phi$ and $\psi$ .

Remark

Craig's interpolation theorem has applications in:

Software verification: Decomposing complex verification conditions
Modular reasoning: Reasoning about systems built from components
Definability theory: Understanding what concepts can be defined using which primitives

The theorem reveals deep structural properties of logical consequence and has analogues in modal logic, temporal logic, and other logical systems.

These theorems demonstrate that first-order logic, despite being more complex than propositional logic, has a rich and well-behaved theory with powerful applications across mathematics and computer science.