Note that all these axioms are first order (that is involve no set variables at all, something even stronger than being arithmetical). The first three, together with mathematical induction, form the usual Peano axioms (the third, actually, is a consequence of even the weakest induction schemes), whereas the subsequent axioms are a definition of addition, multiplication and order on the natural numbers (again, the last two are redundant as soon as any kind of induction axiom is added).
Induction and comprehension schema
If φ("n") is a formula of second-order 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:
:
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.
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:
:
Essentially, this allows us 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. Second-order 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 second-order induction axiom implies each instance of the full induction scheme. Those subsystems, described below, which limit comprehension in some way may offset this limitation by including part of the induction scheme.
Models of second-order arithmetic
Recall that we view second-order arithmetic as a theory in first-order predicate calculus. 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. By omitting "D" we obtain 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 axioms of Peano arithmetic with the second-order induction axiom have only one model under second-order semantics.
When "M" is the usual set of natural numbers with its usual operations, 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 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.
ubsystems of second-order arithmetic
There are many named subsystems of second-order arithmetic.
A subscript 0 in the name of a subsystem indicates that it includes onlya restricted portion of the full second-order induction scheme (Friedman 1976). 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. We may ask whether there is a subsystem of second-order arithmetic which is satisfied by every ω-model that is closed under Turing jump and satisfies some other, more mild, closure conditions. The subsystem just described is called .
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; 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 if and only if S is closed under Turing jump, Turing reducibility, and Turing join.
The subscript 0 in 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 plus induction for all formulas is sometimes called .
The system 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
To define a second subsystem, we will need a bit more terminology.
A formula is called "bounded arithmetical", or Δ00, 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
: