# Second-order arithmetic

In

A precursor to second-order arithmetic that involves third-order parameters was introduced by David Hilbert and Paul Bernays in their book *Grundlagen der Mathematik*.^{[1]} The standard axiomatization of second-order arithmetic is denoted by **Z _{2}**.

Second-order arithmetic includes, but is significantly stronger than, its

^{[2]}

Second-order arithmetic can also be seen as a weak version of set theory in which every element is either a natural number or a set of natural numbers. Although it is much weaker than Zermelo–Fraenkel set theory, second-order arithmetic can prove essentially all of the results of classical mathematics expressible in its language.

A **subsystem of second-order arithmetic** is a

## Definition

### Syntax

The language of second-order arithmetic is

**arithmetical**. An arithmetical formula may have free set variables and bound individual variables.

Individual terms are formed from the constant 0, the unary function *S* (the *successor function*), and the binary operations + and (addition and multiplication). The successor function adds 1 to its input. The relations = (equality) and < (comparison of natural numbers) relate two individuals, whereas the relation ∈ (membership) relates an individual and a set (or class). Thus in notation the language of second-order arithmetic is given by the signature .

For example, , is a well-formed formula of second-order arithmetic that is arithmetical, has one free set variable *X* and one bound individual variable *n* (but no bound set variables, as is required of an arithmetical formula)—whereas is a well-formed formula that is not arithmetical, having one bound set variable *X* and one bound individual variable *n*.

### Semantics

Several different interpretations of the quantifiers are possible. If second-order arithmetic is studied using the full semantics of

^{[3]}

### Axioms

#### Basic

The following axioms are known as the *basic axioms*, or sometimes the *Robinson axioms.* The resulting

**N**, and including the distinguished member , called "

The primitive functions are the unary successor function, denoted by prefix , and two

Axioms governing the

- ("the successor of a natural number is never zero")
- ("the successor function is injective")
- ("every natural number is zero or a successor")

Addition defined recursively:

Multiplication defined recursively:

Axioms governing the

- ("no natural number is smaller than zero")
- ("every natural number is zero or bigger than zero")

These axioms are all

**N**. Adding to these axioms any sort of axiom schema of induction

#### Induction and comprehension schema

If *φ*(*n*) is a formula of second-order arithmetic with a free individual variable *n* and possibly other free individual or set variables (written *m*_{1},...,*m*_{k} and *X*_{1},...,*X*_{l}), the **induction axiom** for *φ* is the axiom:

The (**full**) **second-order induction scheme** consists of all instances of this axiom, over all second-order formulas.

One particularly important instance of the induction scheme is when *φ* is the formula "" expressing the fact that *n* is a member of *X* (*X* being a free set variable): in this case, the induction axiom for *φ* is

This sentence is called the **second-order induction axiom**.

If *φ*(*n*) is a formula with a free variable *n* and possibly other free variables, but not the variable *Z*, the

**comprehension axiom**

*φ*is the formula

This axiom makes it possible to form the set of natural numbers satisfying *φ*(*n*). There is a technical restriction that the formula *φ* may not contain the variable *Z*, for otherwise the formula would lead to the comprehension axiom

- ,

which is inconsistent. This convention is assumed in the remainder of this article.

### The full system

The formal theory of **second-order arithmetic** (in the language of second-order arithmetic) consists of the basic axioms, the comprehension axiom for every formula *φ* (arithmetic or otherwise), and the second-order induction axiom. This theory is sometimes called *full second-order arithmetic* to distinguish it from its subsystems, defined below. Because full second-order semantics imply that every possible set exists, the comprehension axioms may be taken to be part of the deductive system when full second-order semantics is employed.^{}[3]

## Models

This section describes second-order arithmetic with first-order semantics. Thus a **model** of the language of second-order arithmetic consists of a set *M* (which forms the range of individual variables) together with a constant 0 (an element of *M*), a function *S* from *M* to *M*, two binary operations + and · on *M*, a binary relation < on *M*, and a collection *D* of subsets of *M*, which is the range of the set variables. Omitting *D* produces a model of the language of first-order arithmetic.

When *D* is the full powerset of *M*, the model is called a **full model**. The use of full second-order semantics is equivalent to limiting the models of second-order arithmetic to the full models. In fact, the axioms of second-order arithmetic have only one full model. This follows from the fact that the Peano axioms with the second-order induction axiom have only one model under second-order semantics.

### Definable functions

The first-order functions that are provably

^{[4]}Almost equivalently, system F is the theory of functionals corresponding to second-order arithmetic in a manner parallel to how Gödel's system T corresponds to first-order arithmetic in the Dialectica interpretation

### More types of models

When a model of the language of second-order arithmetic has certain properties, it can also be called these other names:

- When
*M*is the usual set of natural numbers with its usual operations, is called an**ω-model**. In this case, the model may be identified with*D*, its collection of sets of naturals, because this set is enough to completely determine an ω-model. The unique full -model, which is the usual set of natural numbers with its usual structure and all its subsets, is called the**intended**or**standard**model of second-order arithmetic.^{}[5] - A model of the language of second-order arithmetic is called a
**β-model**if , i.e. the Σ^{1}_{1}-statements with parameters from that are satisfied by are the same as those satisfied by the full model.^{[6]}Some notions that are absolute with respect to β-models include " encodes a well-order"^{[7]}and " is a tree".^{[6]} - The above result has been extended to the concept of a
**β**for , which has the same definition as the above except is replaced by , i.e. is replaced by ._{n}-model^{[6]}Using this definition β_{0}-models are the same as ω-models.^{[8]}

## Subsystems

There are many named subsystems of second-order arithmetic.

A subscript 0 in the name of a subsystem indicates that it includes only
a restricted portion of the full second-order induction scheme.^{}

_{0}plus the full second-order induction scheme, is stronger than Peano arithmetic.

### Arithmetical comprehension

Many of the well-studied subsystems are related to closure properties of models. For example, it can be shown that every ω-model of full second-order arithmetic is closed under Turing jump, but not every ω-model closed under Turing jump is a model of full second-order arithmetic. The subsystem ACA_{0} includes just enough axioms to capture the notion of closure under Turing jump.

ACA_{0} is defined as the theory consisting of the basic axioms, the **arithmetical comprehension axiom** scheme (in other words the comprehension axiom for every *arithmetical* formula *φ*) and the ordinary second-order induction axiom. It would be equivalent to also include the entire arithmetical induction axiom scheme, in other words to include the induction axiom for every arithmetical formula *φ*.

It can be shown that a collection *S* of subsets of ω determines an ω-model of ACA_{0} if and only if *S* is closed under Turing jump,

^{[10]}

The subscript 0 in ACA_{0} indicates that not every instance of the induction axiom scheme is included this subsystem. This makes no difference for ω-models, which automatically satisfy every instance of the induction axiom. It is of importance, however, in the study of non-ω-models. The system consisting of ACA_{0} plus induction for all formulas is sometimes called ACA with no subscript.

The system ACA_{0} is a conservative extension of **first-order arithmetic** (or first-order Peano axioms), defined as the basic axioms, plus the first-order induction axiom scheme (for all formulas *φ* involving no class variables at all, bound or otherwise), in the language of first-order arithmetic (which does not permit class variables at all). In particular it has the same proof-theoretic ordinal ε_{0} as first-order arithmetic, owing to the limited induction schema.

### The arithmetical hierarchy for formulas

A formula is called *bounded arithmetical*, or Δ^{0}_{0}, when all its quantifiers are of the form ∀*n*<*t* or ∃*n*<*t* (where *n* is the individual variable being quantified and *t* is an individual term), where

stands for

and

stands for

- .

A formula is called Σ^{0}_{1} (or sometimes Σ_{1}), respectively Π^{0}_{1} (or sometimes Π_{1}) when it is of the form ∃*m*_{}*φ*, respectively ∀*m*_{}*φ* where *φ* is a bounded arithmetical formula and *m* is an individual variable (that is free in *φ*). More generally, a formula is called Σ^{0}_{n}, respectively Π^{0}_{n} when it is obtained by adding existential, respectively universal, individual quantifiers to a Π^{0}_{n−1}, respectively Σ^{0}_{n−1} formula (and Σ^{0}_{0} and Π^{0}_{0} are both equal to Δ^{0}_{0}). By construction, all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula in

^{0}

_{n}or Π

^{0}

_{n}formula for all large enough

*n*.

### Recursive comprehension

The subsystem RCA_{0} is a weaker system than ACA_{0} and is often used as the base system in reverse mathematics. It consists of: the basic axioms, the Σ^{0}_{1} induction scheme, and the Δ^{0}_{1} comprehension scheme. The former term is clear: the Σ^{0}_{1} induction scheme is the induction axiom for every Σ^{0}_{1} formula *φ*. The term "Δ^{0}_{1} comprehension" is more complex, because there is no such thing as a Δ^{0}_{1} formula. The Δ^{0}_{1} comprehension scheme instead asserts the comprehension axiom for every Σ^{0}_{1} formula that is logically equivalent to a Π^{0}_{1} formula. This scheme includes, for every Σ^{0}_{1} formula *φ* and every Π^{0}_{1} formula *ψ*, the axiom:

The set of first-order consequences of RCA_{0} is the same as those of the subsystem IΣ_{1} of Peano arithmetic in which induction is restricted to Σ^{0}_{1} formulas. In turn, IΣ_{1} is conservative over primitive recursive arithmetic (PRA) for sentences. Moreover, the proof-theoretic ordinal of is ω^{ω}, the same as that of PRA.

It can be seen that a collection *S* of subsets of ω determines an ω-model of RCA_{0} if and only if *S *is closed under Turing reducibility and Turing join. In particular, the collection of all computable subsets of ω gives an ω-model of RCA_{0}. This is the motivation behind the name of this system—if a set can be proved to exist using RCA_{0}, then the set is recursive (i.e. computable).

### Weaker systems

Sometimes an even weaker system than RCA_{0} is desired. One such system is defined as follows: one must first augment the language of arithmetic with an exponential function symbol (in stronger systems the exponential can be defined in terms of addition and multiplication by the usual trick, but when the system becomes too weak this is no longer possible) and the basic axioms by the obvious axioms defining exponentiation inductively from multiplication; then the system consists of the (enriched) basic axioms, plus Δ^{0}_{1} comprehension, plus Δ^{0}_{0} induction.

### Stronger systems

Over ACA_{0}, each formula of second-order arithmetic is equivalent to a Σ^{1}_{n} or Π^{1}_{n} formula for all large enough *n*. The system **Π ^{1}_{1}-comprehension** is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every (

^{[11]}

^{1}

_{1}formula

*φ*. This is equivalent to Σ

^{1}

_{1}-comprehension (on the other hand, Δ

^{1}

_{1}-comprehension, defined analogously to Δ

^{0}

_{1}-comprehension, is weaker).

## Projective determinacy

_{2}.

Many natural propositions expressible in the language of second-order arithmetic are independent of Z_{2} and even

_{0}), projective determinacy implies comprehension and provides an essentially complete theory of second-order arithmetic — natural statements in the language of Z

_{2}that are independent of Z

_{2}with projective determinacy are hard to find.

^{[12]}

ZFC + {there are *n* Woodin cardinals: *n* is a natural number} is conservative over Z_{2} with projective determinacy^{[citation needed]}, that is a statement in the language of second-order arithmetic is provable in Z_{2} with projective determinacy if and only if its translation into the language of set theory is provable in ZFC + {there are *n* Woodin cardinals: *n*∈N}.

## Coding mathematics

Second-order arithmetic directly formalizes natural numbers and sets of natural numbers. However, it is able to formalize other mathematical objects indirectly via coding techniques, a fact that was first noticed by Weyl.^{[13]} The integers, rational numbers, and real numbers can all be formalized in the subsystem RCA_{0}, along with complete separable metric spaces and continuous functions between them.^{[14]}

The research program of reverse mathematics uses these formalizations of mathematics in second-order arithmetic to study the set-existence axioms required to prove mathematical theorems.^{[15]} For example, the intermediate value theorem for functions from the reals to the reals is provable in RCA_{0},^{[16]} while the Bolzano**–**Weierstrass theorem is equivalent to ACA_{0} over RCA_{0}.^{[17]}

The aforementioned coding works well for continuous and total functions, assuming a higher-order base theory plus weak Kőnig's lemma.^{[18]} As perhaps expected, in the case of topology, coding is not without problems.^{[19]}

## See also

## References

- MR 0237246.
**.**- ^ .
**.****.**- ^ .
**.****.****.****^**Simpson 2009, pp. 311–313.- MR 2830409.
**^**Woodin, W. H. (2001). "The Continuum Hypothesis, Part I".*Notices of the American Mathematical Society*.**48**(6).**^**Simpson 2009, p. 16.**^**Simpson 2009, Chapter II.**^**Simpson 2009, p. 32.**^**Simpson 2009, p. 87.**^**Simpson 2009, p. 34.- MR 1943304.
**^**Hunter, James (2008).*Higher order Reverse Topology*(PDF) (Doctoral dissertation). University of Madison-Wisconsin.

**
**## Further reading

- Burgess, J. P. (2005).
*Fixing Frege*. Princeton University Press. - ISBN 0-444-89840-9.
- .