In mathematical logic, second-order 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.
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. The standard axiomatization of second-order arithmetic is denoted by Z2.
Second-order arithmetic includes, but is significantly stronger than, its first-order counterpart Peano arithmetic. Unlike Peano arithmetic, second-order arithmetic allows quantification over sets of natural numbers as well as numbers themselves. Because real numbers can be represented as (infinite) sets of natural numbers in well-known ways, and because second-order arithmetic allows quantification over such sets, it is possible to formalize the real numbers in second-order arithmetic. For this reason, second-order arithmetic is sometimes called "analysis".
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 theory in the language of second-order arithmetic each axiom of which is a theorem of full second-order arithmetic (Z2). 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 second-order arithmetic is two-sorted. The first sort of terms and in particular 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 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 second-order logic then the set quantifiers range over all subsets of the range of the individual variables. If second-order arithmetic is formalized using the semantics of first-order logic (Henkin semantics) 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 individual variables.
Axioms
Basic The following axioms are known as the basic axioms, or sometimes the Robinson axioms. The resulting first-order 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 , called "zero."
The primitive functions are the unary successor function, denoted by prefix , and two binary operations, addition and multiplication, denoted by the infix operator "+" and "", respectively. There is also a primitive binary relation called order, denoted by the infix operator "<".
Axioms governing the successor function and zero: ("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 order relation "<": ("no natural number is smaller than zero")
("every natural number is zero or bigger than zero")
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 Peano–Dedekind 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 second-order arithmetic with a free individual variable n and possibly other free individual or set variables (written m1,...,mk and X1,...,Xl), 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 for φ 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.
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 total in second-order arithmetic are precisely the same as those representable in system F. 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. A model of the language of second-order arithmetic is called a β-model if , i.e. the Σ11-statements with parameters from that are satisfied by are the same as those satisfied by the full model. Some notions that are absolute with respect to β-models include " encodes a well-order" and " is a tree". The above result has been extended to the concept of a βn-model for , which has the same definition as the above except is replaced by , i.e. is replaced by . Using this definition β0-models are the same as ω-models.
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. Such a restriction lowers the proof-theoretic strength of the system significantly. For example, the system ACA0 described below is equiconsistent with Peano arithmetic. The corresponding theory ACA, consisting of ACA0 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 ACA0 includes just enough axioms to capture the notion of closure under Turing jump.
ACA0 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 ACA0 if and only if S is closed under Turing jump, Turing reducibility, and Turing join.
The subscript 0 in ACA0 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 ACA0 plus induction for all formulas is sometimes called ACA with no subscript.
The system ACA0 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