Model theory is often described as algebra + logic. While proof theory analyzes the syntactic mechanics of deductions, model theory studies the mathematical structures themselves—rings, fields, graphs, groups—through the lens of formal languages. At its core lies the delicate distinction between isomorphism (algebraic identity) and elementary equivalence (logical indistinguishability). Through the power of Quantifier Elimination, model theory provides constructive algorithms that settle the decidability and geometry of entire mathematical universes.
1. Elementary Equivalence vs Isomorphism
Let $mathcal{M}$ and $mathcal{N}$ be structures in a first-order language $mathcal{L}$.
- Isomorphism ($mathcal{M} cong mathcal{N}$): There exists a bijection $f: M to N$ preserving all constants, functions, and relations. This is total structural identity.
- Elementary Equivalence ($mathcal{M} equiv mathcal{N}$): $mathcal{M}$ and $mathcal{N}$ satisfy precisely the same first-order sentences:
[
forall sigma in text{Sent}(mathcal{L}): quad mathcal{M} vDash sigma iff mathcal{N} vDash sigma
]
Every isomorphic pair is elementarily equivalent ($mathcal{M} cong mathcal{N} implies mathcal{M} equiv mathcal{N}$). However, the converse fails spectacularly! By the Löwenheim-Skolem theorems, any infinite structure has elementarily equivalent models of every infinite cardinality. For example, the rational numbers $(mathbb{Q}, <)$ and the real numbers $(mathbb{R}, <)$ are elementarily equivalent as dense linear orders without endpoints, yet $|mathbb{Q}| = aleph_0$ while $|mathbb{R}| = 2^{aleph_0}$, making an algebraic isomorphism impossible.
2. The Ehrenfeucht-Fraïssé Game
How can one prove that two structures are elementarily equivalent without testing infinitely many formulas? Roland Fraïssé (1954) and Andrzej Ehrenfeucht (1961) converted model theory into a game played between two players: Spoiler and Duplicator.
The $n$-Round EF Game $G_n(mathcal{M}, mathcal{N})$
In each of $n$ rounds, Spoiler picks an element from either $mathcal{M}$ or $mathcal{N}$. Duplicator must respond by picking an element from the other structure. After $n$ rounds, sequences $vec{a} = (a_1, dots, a_n) in M^n$ and $vec{b} = (b_1, dots, b_n) in N^n$ have been chosen.
Winning Condition: Duplicator wins if the mapping $a_i mapsto b_i$ is a partial isomorphism between $mathcal{M}$ and $mathcal{N}$.
The Ehrenfeucht-Fraïssé Theorem
Duplicator has a winning strategy in $G_n(mathcal{M}, mathcal{N})$ for all $n in mathbb{N}$ if and only if $mathcal{M} equiv mathcal{N}$.
The EF game translates abstract logical equivalence into a concrete combinatorial game of spatial mimicking.
3. Quantifier Elimination (QE)
Quantifiers ($forall, exists$) are the source of infinite complexity in mathematical logic. A theory $T$ has Quantifier Elimination if every formula $phi(x_1, dots, x_n)$ is provably equivalent modulo $T$ to a quantifier-free formula $psi(x_1, dots, x_n)$:
[
T vdash forall vec{x} , (phi(vec{x}) leftrightarrow psi(vec{x}))
]
Quantifier elimination implies that the definable sets in models of $T$ are completely determined by boolean combinations of basic equations and inequalities. It immediately yields:
- Completeness: If $T$ has QE and specifies the truth of quantifier-free sentences, $T$ is complete.
- Decidability: Any closed sentence can be algorithmically evaluated by removing all quantifiers and calculating the truth of constants.
4. Landmark Theorems: RCF and ACF
1. Real Closed Fields (Tarski-Seidenberg Theorem, 1948)
The first-order theory of Real Closed Fields ($text{RCF}$)—the theory of the ordered field of real numbers $(mathbb{R}, 0, 1, +, times, <)$—possesses quantifier elimination!
Consequence: Every definable subset in $mathbb{R}^n$ is a semialgebraic set (a finite union of sets defined by polynomial equalities $P(x) = 0$ and inequalities $Q(x) > 0$). Projecting a semialgebraic set onto lower dimensions yields another semialgebraic set. Tarski proved that elementary Euclidean geometry and real algebra are completely decidable by algorithm!
2. Algebraically Closed Fields ($text{ACF}$)
The theory of Algebraically Closed Fields ($text{ACF}$)—such as the complex numbers $(mathbb{C}, 0, 1, +, times)$—has quantifier elimination. By Chevalley’s Theorem in algebraic geometry, the projection of any constructible set is constructible. This establishes the completeness of $text{ACF}_0$, leading directly to the Lefschetz Principle: any first-order algebraic sentence true in the complex numbers $mathbb{C}$ is true in any algebraically closed field of characteristic zero!
