Mathematical logic and foundations Definition

Second-order arithmetic

Builds on Peano axioms Robinson arithmetic Theory Well-formed formula

Definition

The language of second-order arithmetic has number variables $n, m, x, y, \ldots$ and set variables $X, Y, \ldots$ . It has the constants $0$ and $1$ , the operations $+$ and $\cdot$ , and the relation $<$ on numbers. It also has the membership relation $n \in X$ between a number and a set. Second-order arithmetic $\mathsf{Z}_2$ is the theory in this two-sorted first-order language with these axioms:

the basic axioms: the axioms of a discretely ordered commutative semiring with least element $0$ and successor $n + 1$ , in the style of Robinson arithmetic;
the induction axiom: $\forall X\, \big( (0 \in X \wedge \forall n\, (n \in X \to n + 1 \in X)) \to \forall n\, (n \in X) \big)$ ;
the comprehension scheme: $\exists X\, \forall n\, (n \in X \leftrightarrow \varphi(n))$ for every formula $\varphi(n)$ in which $X$ does not occur free.

Remarks

Example: the full structure, with number domain $\N$ and set domain the power set of $\N$ , is a model of $\mathsf{Z}_2$ . Each clause holds because every subset of $\N$ is available, and ordinary induction holds in $\N$ .

Non-example: the structure with number domain $\N$ and set domain the computable subsets of $\N$ satisfies clauses 1 and 2 but not clause 3. The formula $\varphi(e)$ that says "program $e$ halts on input $e$ " uses only number quantifiers, and the set it defines is the halting problem, which is not computable.

Subsystems are obtained by restricting comprehension and induction to classes of formulas, for example arithmetical comprehension in $\mathsf{ACA}_0$ . Despite the name, $\mathsf{Z}_2$ is a first-order theory: its models may have a set domain smaller than the full power set. Together with clause 2, the comprehension scheme proves induction for every formula, so the first-order Peano axioms are provable in $\mathsf{Z}_2$ .

Reading path

To understand this page from the ground up, read these 5 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Tag	`Y92NXGEQBD`
URI	`m2://Y92NXGEQBD`
Kind	definition
Writing	W0 stub
MSC	03F35, 03B30
Defines	Second-order arithmetic
Uses	Peano axioms, Robinson arithmetic, Theory, Well-formed formula
Changed	2 November 2026

Second-order arithmetic

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here