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. Extensionality for sets is postulated as well.

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, Feferman, Schütte), admissible systems extend up to $ATR_0$ (proof-theoretic ordinal $\Gamma_0$) — 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.

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$.

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 and the Löwenheim–Skolem theorem on the existence of countable nonstandard models apply to it as well.

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. Within $ZF$, however, the standard model is unique up to isomorphism (total categoricity). Fixing the standard model yields a complete but non-enumerable set of true statements — the elementary theory of the standard model, $\mathrm{Th}_2(\mathbb{N})$. 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 second-order quantifiers over sets are precisely quantifiers “for every real $x$” ($\forall X\;(IsReal(X) \to \dots)$). 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 sets of real numbers (elements of $\mathcal{P}^2(\mathbb{N})$). For arbitrary 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$. Basic Lebesgue measure theory on $\mathbb{R}$ (including countable additivity) is already formalizable in weak subsystems such as $WWKL_0$, below $ACA_0$; $Z_2$ is more than adequate for this.

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$). 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.