Hierarchy of Second-Order Arithmetic Theories

Extending the language and the formula hierarchy

Building a second-order theory begins with fixing a first-order base. A second sort of variables is added to the standard language — variables ranging over subsets of the domain of individuals ($X, Y, Z, \dots$). The signature includes a membership predicate $x \in X$, where $x$ is an individual and $X$ is a set. Equality between sets is normally not taken as primitive: $X = Y$ abbreviates $\forall n\,(n \in X \leftrightarrow n \in Y)$, so extensionality holds by definition of the language rather than being postulated as a separate axiom (the standard convention for $L_2$; Simpson, SOSOA, §I.2).

This extension yields a strict hierarchy of formulas. At the bottom lie purely first-order formulas. The base is extended by the class of arithmetical formulas — in the notation of the arithmetical hierarchy, the classes $\Sigma^0_k$ and $\Pi^0_k$ (not to be confused with $\Sigma^1_k$ of the analytical hierarchy): they may contain set variables as parameters, but do not allow quantification over sets. Above this sits the analytical hierarchy — genuinely second-order formulas with quantifiers over sets ($\Sigma^1_k$, $\Pi^1_k$, …).

Arithmetical comprehension and $ACA_0$

A fundamental step is adding a comprehension scheme guaranteeing the existence of sets defined by formulas. Restricting this scheme to arithmetical formulas yields the theory $ACA_0$. Comprehension here is narrowly predicative: defining a set does not rely on quantifiers over sets and does not require “searching through” the universe to which the set being defined itself belongs.

In the broader sense of predicative mathematics (Weyl, 1918; Feferman, 1964; Schütte, 1965), admissible systems extend up to $ATR_0$, whose proof-theoretic ordinal $\Gamma_0$ is customarily taken as the limit of predicativity — substantially stronger than $ACA_0$ (ordinal $\varepsilon_0$). $ACA_0$ is only the lower rung of this range, though it often serves as the entry point to reverse mathematics. Weyl's predicative analysis itself is treated as a separate level of formalization in the material «Levels of Formalization of Mathematical Analysis».

At this stage we move away from the first-order induction scheme and add a single induction axiom for sets:

Thanks to arithmetical comprehension, this single axiom automatically entails induction for all arithmetical formulas. This is the transition from $PA$ to $ACA_0$ — and it is conservative: every arithmetical sentence provable in $ACA_0$ is already provable in $PA$, which is why the two share the proof-theoretic ordinal $\varepsilon_0$.

Replacing a countable axiom scheme by a single axiom is not a technicality but a change in the logical form of the principle itself: a scheme in $PA$, an axiom in $Z_2$, a theorem in $ZFC$. These forms, how they relate, and exactly where the equivalences break down are examined in the material «On Mathematical Induction».

Impredicativity and formal $Z_2$

The comprehension scheme can be extended to all formulas of the second-order language, yielding the impredicative second-order theory $Z_2$. It is important to note that at this stage everything remains, in essence, a first-order theory — but with two sorts of variables and a membership predicate.

As a formal system, $Z_2$ fully inherits the “generic blemishes” of first-order arithmetic. Gödel’s incompleteness theorems apply to it; by the downward Löwenheim–Skolem theorem it has countable models — and none of them is standard, since the second sort of a countable model cannot exhaust the uncountable $\mathcal{P}(\mathbb{N})$. By compactness there are also models whose number sort is nonstandard.

Completeness of the calculus is likewise first-order here: it is achieved over general (Henkin) models, where the second sort is an arbitrary family closed under the comprehension scheme rather than the genuine power set. How such a model is built from a consistent theory is shown in the material «The Henkin Construction».

Model-theoretic arithmetic and categoricity

A principled conceptual shift occurs when one turns to models. Alongside formal $Z_2$, we may consider the class of its standard models, in which set variables are interpreted as elements of the genuine power set of the natural numbers, $\mathcal{P}(\mathbb{N})$. This combination of theory and a restriction on the class of models is model-theoretic second-order arithmetic.

The formal deductive apparatus is the same in both approaches, so the set of theorems provable by finite proofs coincides. Under full semantics, however, the standard model is unique up to isomorphism — the categoricity of second-order arithmetic (in essence Dedekind's theorem, 1888), proved in a metatheory such as $ZF$. Fixing the standard model yields a complete but non-recursively-enumerable set of true statements — the full theory of the standard model, $\mathrm{Th}_2(\mathbb{N})$. Moreover, $\mathrm{Th}_2(\mathbb{N})$ is not definable in the second-order language itself — the second-order form of Tarski's undefinability theorem; defining it already takes third order. Humans can identify truths not formally provable in $Z_2$ only by stepping outside the language and using external methods from stronger metatheories (e.g. $ZFC$).

Expressive power and higher orders ($PA_n$)

In $Z_2$, real numbers are coded as sets of naturals (Dedekind cuts in $\mathbb{Q}$, Cauchy sequences, etc.), so a quantifier over sets yields, after relativization, a quantifier “for every real $x$”: $\forall X\,(\mathrm{IsReal}(X) \to \dots)$. A single set also codes an entire sequence of reals, so countable families stay inside the language as well. Classical analysis — continuous functions, convergence, Borel sets — is formalizable in $Z_2$ without moving to higher orders.

The limitation of $Z_2$ is different: the theory cannot directly quantify over arbitrary sets of real numbers (elements of $\mathcal{P}^2(\mathbb{N})$). For uncountable families of subsets of $\mathbb{R}$, function spaces in full generality, and genuine third-order semantics, one needs theories $PA_n$ with $n \ge 3$ (more often written $Z_n$ in the literature).

Just how modest the means required for analysis are is measured precisely by reverse mathematics. Basic Lebesgue measure theory is already developed over $RCA_0$, and countable additivity of the measure on open sets is equivalent over $RCA_0$ to $WWKL_0$ — “weak weak” König's lemma: every subtree of $2^{<\mathbb{N}}$ of positive measure has an infinite path (Yu–Simpson, 1990). That is strictly below $WKL_0$:

In other words, Lebesgue measure does not even require $ACA_0$, let alone full $Z_2$.

Like $Z_2$, the theories $PA_n$ can be studied in a formal (deductive) or model-theoretic setting.

The cumulative hierarchy and $ZFA$

A global alternative to stacking orders is to move to a theory with urelements ($ZFA$, also written $ZFU$; not to be confused with $ZFA$ in the sense of Aczel's anti-foundation). Here $\mathbb{N}$ is taken as the set of urelements, and the standard cumulative hierarchy of sets is built above it. This provides full freedom to state and prove facts from functional analysis and topology.

The atomic base theory is needed here solely to block the syntactic possibility of writing $x \in \alpha$, where $\alpha$ is a urelement. The theory is thereby detached from the specifics of any particular set-theoretic construction of numbers.

The same device — atoms instead of a construction — is applied one level up in the material «Levels of Formalization of Mathematical Analysis», where the cumulative hierarchy is built over $\mathbb{R}$ as the set of atoms; there one can also see, step by step, what each increase in expressive power buys and what it costs.