In mathematical logic, secondorder arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their book Grundlagen der Mathematik. The standard axiomatization of secondorder arithmetic is denoted Z_{2}.
Secondorder arithmetic includes, but is significantly stronger than, its firstorder counterpart Peano arithmetic. Unlike Peano arithmetic, secondorder arithmetic allows quantification over sets of numbers as well as numbers themselves. Because real numbers can be represented as (infinite) sets of natural numbers in wellknown ways, and because second order arithmetic allows quantification over such sets, it is possible to formalize the real numbers in secondorder arithmetic. For this reason, secondorder arithmetic is sometimes called “analysis”.
Secondorder 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 ZermeloFraenkel set theory, secondorder arithmetic can prove essentially all of the results of classical mathematics expressible in its language.
A subsystem of secondorder arithmetic is a theory in the language of secondorder arithmetic each axiom of which is a theorem of full secondorder arithmetic (Z_{2}). Such subsystems are essential to reverse mathematics, a research program investigating how much of classical mathematics can be derived in certain weak subsystems of varying strength. Much of core mathematics can be formalized in these weak subsystems, some of which are defined below. Reverse mathematics also clarifies the extent and manner in which classical mathematics is nonconstructive.
Definition
Syntax
The language of secondorder arithmetic is twosorted. The first sort of terms and variables, usually denoted by lower case letters, consists of individuals, whose intended interpretation is as natural numbers. The other sort of variables, variously called “set variables,” “class variables,” or even “predicates” are usually denoted by upper case letters. They refer to classes/predicates/properties of individuals, and so can be thought of as sets of natural numbers. Both individuals and set variables can be quantified universally or existentially. A formula with no bound set variables (that is, no quantifiers over set variables) is called 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 (=S0) 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).
For example, \forall n (n\in X \rightarrow Sn \in X), is a wellformed formula of secondorder 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 \exists X \forall n(n\in X \leftrightarrow n < SSSSSS0\cdot SSSSSSS0) is a wellformed formula that is not arithmetical with one bound set variable X and one bound individual variable n.
Semantics
Several different interpretations of the quantifiers are possible. If secondorder arithmetic is studied using the full semantics of secondorder logic then the set quantifiers range over all subsets of the range of the number variables. If secondorder arithmetic is formalized using the semantics of firstorder logic then any model includes a domain for the set variables to range over, and this domain may be a proper subset of the full powerset of the domain of number variables.
Although secondorder arithmetic was originally studied using full secondorder semantics, the vast majority of current research treats secondorder arithmetic in firstorder predicate calculus. This is because the model theory of subsystems of secondorder arithmetic is more interesting in the setting of firstorder logic.
Axioms
Basic
The following axioms are known as the basic axioms, or sometimes the Robinson axioms. The resulting firstorder theory, known as Robinson arithmetic, is essentially Peano arithmetic without induction. The domain of discourse for the quantified variables is the natural numbers, collectively denoted by N, and including the distinguished member \ 0, called "zero."
The primitive functions are the unary successor function, denoted by prefix \ S,, and two binary operations, addition and multiplication, denoted by infix "+" and " \cdot", respectively. There is also a primitive binary relation called order, denoted by infix "<".
Axioms governing the successor function and zero:

1. \forall m [Sm=0 \rightarrow \bot]. (“the successor of a natural number is never zero”)

2. \forall m \forall n [Sm=Sn \rightarrow m=n]. (“the successor function is injective”)

3. \forall n [0=n \lor \exists m [Sm=n] ]. (“every natural number is zero or a successor”)
Addition defined recursively:

4. \forall m [m+0=m].

5. \forall m \forall n [m+Sn = S(m+n)].
Multiplication defined recursively:

6. \forall m [m\cdot 0 = 0].

7. \forall m \forall n [m \cdot Sn = (m\cdot n)+m].
Axioms governing the order relation "<":

8. \forall m [m<0 \rightarrow \bot]. (“no natural number is smaller than zero”)

9. \forall m [m

10. \forall n [0=n \lor 0 (“every natural number is zero or bigger than zero”)

11. \forall m \forall n [(Sm
These axioms are all first order statements. That is, all variables range over the natural numbers and not sets thereof, a fact even stronger than their being arithmetical. Moreover, there is but one existential quantifier, in axiom 3. Axioms 1 and 2, together with an axiom schema of induction make up the usual PeanoDedekind definition of N. Adding to these axioms any sort of axiom schema of induction makes redundant the axioms 3, 10, and 11.
Induction and comprehension schema
If φ(n) is a formula of secondorder arithmetic with a free number variable n and possible other free number or set variables (written m_{•} and X_{•}), the induction axiom for φ is the axiom:

\forall m_\bullet \forall X_\bullet ((\varphi(0) \land \forall n (\varphi(n) \rightarrow \varphi(Sn)) \rightarrow \forall n \varphi(n))
The (full) secondorder induction scheme consists of all instances of this axiom, over all secondorder formulas.
One particularly important instance of the induction scheme is when φ is the formula “n \in X” expressing the fact that n is a member of X (X being a free set variable): in this case, the induction axiom for φ is

\forall X ((0\in X \land \forall n (n\in X \rightarrow Sn\in X)) \rightarrow \forall n (n\in X))
This sentence is called the secondorder induction axiom.
Returning to the case where φ(n) is a formula with a free variable n and possibly other free variables, we define the comprehension axiom for φ to be:

\forall m_\bullet \forall X_\bullet \exists Z \forall n (n\in Z \leftrightarrow \varphi(n))
Essentially, this allows us to form the set Z = \{ n  \varphi(n) \} of natural numbers satisfying φ(n). There is a technical restriction that the formula φ may not contain the variable Z, for otherwise the formula n \not \in Z would lead to the comprehension axiom

\exists Z \forall n ( n \in Z \leftrightarrow n \not \in Z),
which is inconsistent. This convention is assumed in the remainder of this article.
The full system
The formal theory of secondorder arithmetic (in the language of secondorder arithmetic) consists of the basic axioms, the comprehension axiom for every formula φ, (arithmetic or otherwise) and the secondorder induction axiom. This theory is sometimes called full second order arithmetic to distinguish it from its subsystems, defined below. Secondorder semantics eliminates the need for the comprehension axiom, because these semantics imply that every possible set exists.
In the presence of the unrestricted comprehension scheme, the single secondorder induction axiom implies each instance of the full induction scheme. Subsystems that limit comprehension in some way may offset this limitation by including part of the induction scheme. Examples of such systems are provided below.
Models of secondorder arithmetic
Recall that we view secondorder arithmetic as a theory in firstorder predicate calculus. Thus a model \mathcal{M} of the language of secondorder 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. By omitting D we obtain a model of the language of first order arithmetic.
When D is the full powerset of M, the model \mathcal{M} is called a full model. The use of full secondorder semantics is equivalent to limiting the models of secondorder arithmetic to the full models. In fact, the axioms of secondorder arithmetic have only one full model. This follows from the fact that the axioms of Peano arithmetic with the secondorder induction axiom have only one model under secondorder semantics.
When M is the usual set of natural numbers with its usual operations, \mathcal{M} is called an ωmodel. In this case we may identify the model with D, its collection of sets of naturals, because this set is enough to completely determine an ωmodel.
The unique full \omegamodel, which is the usual set of natural numbers with its usual structure and all its subsets, is called the intended or standard model of secondorder arithmetic.
Definable functions of secondorder arithmetic
The firstorder functions that are provably total in secondorder arithmetic are precisely the same as those representable in system F (Girard et al., 1987, pp. 122–123). Almost equivalently, system F is the theory of functionals corresponding to secondorder arithmetic in a manner parallel to how Gödel's system T corresponds to firstorder arithmetic in the Dialectica interpretation.
Subsystems of secondorder arithmetic
There are many named subsystems of secondorder arithmetic.
A subscript 0 in the name of a subsystem indicates that it includes only a restricted portion of the full secondorder induction scheme (Friedman 1976). Such a restriction lowers the prooftheoretic strength of the system significantly. For example, the system ACA_{0} described below is equiconsistent with Peano arithmetic. The corresponding theory ACA, consisting of ACA_{0} plus the full secondorder induction scheme, is stronger than Peano arithmetic.
Arithmetical comprehension
Many of the wellstudied subsystems are related to closure properties of models. For example, it can be shown that every ωmodel of full secondorder arithmetic is closed under Turing jump, but not every ωmodel closed under Turing jump is a model of full secondorder arithmetic. We may ask whether there is a subsystem of secondorder arithmetic satisfied by every ωmodel that is closed under Turing jump and satisfies some other, more mild, closure conditions. The subsystem just described is called \mathrm{ACA}_0.
\mathrm{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 secondorder induction axiom; again, we could also choose to include the arithmetical induction axiom scheme, in other words the induction axiom for every arithmetical formula φ, without making a difference.
It can be seen that a collection S of subsets of ω determines an ωmodel of \mathrm{ACA}_0 if and only if S is closed under Turing jump, Turing reducibility, and Turing join.
The subscript 0 in \mathrm{ACA}_0 indicates that we have not included every instance of the induction axiom in this subsystem. This makes no difference when we study only ωmodels, which automatically satisfy every instance of the induction axiom. It is of crucial importance, however, when we study models that are not ωmodels. The system consisting of \mathrm{ACA}_0 plus induction for all formulas is sometimes called \mathrm{ACA}.
The system \mathrm{ACA}_0 is a conservative extension of firstorder arithmetic (or firstorder 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 prooftheoretic ordinal ε_{0} as firstorder arithmetic, owing to the limited induction schema.
The arithmetical hierarchy for formulas
To define a second subsystem, we will need a bit more terminology.
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

\forall n
stands for

\forall n(n
and

\exists n
stands for

\exists n(n.
A formula is called Σ^{0}_{1} (or sometimes Σ_{1}), respectively Π^{0}_{1} (or sometimes Π_{1}) when it 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 all equivalent to Δ^{0}_{0}). Note that by construction all these formulas are arithmetical (no class variables are ever bound) and, in fact, by putting the formula in Skolem prenex form one can see that every arithmetical formula is equivalent to a Σ^{0}_{n} or Π^{0}_{n} formula for all large enough n.
Recursive comprehension
The subsystem \mathrm{RCA}_0 is an even weaker system than \mathrm{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” requires a little more explaining, however: there is no such thing as a Δ^{0}_{1} formula (the intended meaning is a formula that is both Σ^{0}_{1} and Π^{0}_{1}), but we are instead postulating the comprehension axiom for every Σ^{0}_{1} formula subject to the condition that it is equivalent to a Π^{0}_{1} formula, in other words, for every Σ^{0}_{1} formula φ and every Π^{0}_{1} formula ψ we postulate

\forall m \forall X ((\forall n (\varphi(n) \leftrightarrow \psi(n))) \rightarrow \exists Z \forall n (n\in Z \leftrightarrow \varphi(n)))
The set of firstorder consequences of \mathrm{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 \Pi^0_2 sentences. Moreover, the prooftheoretic ordinal of \mathrm{RCA}_0 is ω^{ω}, the same as that of PRA.
It can be seen that a collection S of subsets of ω determines an ωmodel of \mathrm{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 \mathrm{RCA}_0. This is the motivation behind the name of this system—if a set can be proved to exist using \mathrm{RCA}_0, then the set is computable (i.e. recursive).
Weaker systems
Sometimes an even weaker system than \mathrm{RCA}_0 is desired. One such system is defined as follows: one must first augment the language of arithmetic with an exponential function (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
Much as we have defined Σ_{n} and Π_{n} (or, more accurately, Σ^{0}_{n} and Π^{0}_{n}) formulae, we can define Σ^{1}_{n} and Π^{1}_{n} formulae in the following way: a Δ^{1}_{0} (or Σ^{1}_{0} or Π^{1}_{0}) formula is just an arithmetical formula, and a Σ^{1}_{n}, respectively Π^{1}_{n}, formula is obtained by adding existential, respectively universal, class quantifiers in front of a Π^{1}_{n−1}, respectively Σ^{1}_{n−1}.
It is not too hard to see that over a not too weak system, any formula of secondorder 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 secondorder induction axiom and the comprehension axiom for every Π^{1}_{1} formula φ. It is an easy exercise to show that this is actually equivalent to Σ^{1}_{1}comprehension (on the other hand, Δ^{1}_{1}comprehension, defined by the same trick as introduced earlier for Δ^{0}_{1} comprehension, is actually weaker).
Projective Determinacy
Projective determinacy is the assertion that every twoplayer perfect information game with moves being integers, game length ω and projective payoff set is determined, that is one of the players has a winning strategy. (The first player wins the game if the play belongs to the payoff set; otherwise, the second player wins.) A set is projective iff (as a predicate) it is expressible by a formula in the language of second order arithmetic, allowing real numbers as parameters, so projective determinacy is expressible as a schema in the language of Z_{2}.
Many natural propositions expressible in the language of second order arithmetic are independent of Z_{2} and even ZFC but are provable from projective determinacy. Examples include coanalytic perfect subset property, measurability and the property of Baire for \Sigma^1_2 sets, \Pi^1_3 uniformization, etc. Over a weak base theory (such as RCA_{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.^{[1]}
ZFC + {there are n Woodin cardinals: n is a natural number} is conservative over Z_{2} with projective determinacy, that is a statement in the language of second order arithmetic is provable in Z_{2} with projective determinacy iff its translation into the language of set theory is provable in ZFC + {there are n Woodin cardinals: n∈N}.
Coding mathematics in secondorder arithmetic
Secondorder arithmetic allows us to speak directly (without coding) of natural numbers and sets of natural numbers. Pairs of natural numbers can be coded in the usual way as natural numbers, so arbitrary integers or rational numbers are firstclass citizens in the same manner as natural numbers. Functions between these sets can be encoded as sets of pairs, and hence as subsets of the natural numbers, without difficulty. Real numbers can be defined as Cauchy sequences of rational numbers, but for technical reasons not discussed here, it is preferable (in the weak axiom systems above) to constrain the convergence rate (say by requiring that the distance between the nth and (n+1)th term be less than 2^{−n}). These systems cannot speak of real functions, or subsets of the reals. Nevertheless, continuous real functions are legitimate objects of study, since they are defined by their values on the rationals. Moreover, a related trick makes it possible to speak of open subsets of the reals. Even Borel sets of reals can be coded in the language of secondorder arithmetic, although doing so is a bit tricky.
References

Burgess, John P., 2005. Fixing Frege. Princeton University Press.

Buss, S. R., Handbook of proof theory ISBN 0444898409

Friedman, Harvey. "Systems of second order arithmetic with restricted induction," I, II (Abstracts). Journal of Symbolic Logic, v.41, pp. 557– 559, 1976. JStor

Girard, Lafont and Taylor, 1987. Proofs and Types. Cambridge University Press.


Simpson, Stephen G. (2009), Subsystems of second order arithmetic, Perspectives in Logic (2nd ed.),

Gaisi Takeuti (1975) Proof theory ISBN 0444104925

^ W. Hugh Woodin (2001). "The Continuum Hypothesis, Part I". Notices of the American Mathematical Society 48 (6).
See also
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.