In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets.
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.
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.
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 domain of discourse for the quantified variables is the natural numbers, collectively denoted by N, and including the distinguished member
There is also a primitive binary relation called order, denoted by the infix operator "<".
That is, all variables range over the natural numbers and not sets thereof, a fact even stronger than their being arithmetical.
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.
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.
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.
The first-order functions that are provably total in second-order arithmetic are precisely the same as those representable in system F.[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.
A subscript 0 in the name of a subsystem indicates that it includes only a restricted portion of the full second-order induction scheme.
The corresponding theory ACA, consisting of ACA0 plus the full second-order induction scheme, is stronger than Peano arithmetic.
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.
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 φ.
[10] 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.
The system consisting of ACA0 plus induction for all formulas is sometimes called ACA with no subscript.
In particular it has the same proof-theoretic ordinal ε0 as first-order arithmetic, owing to the limited induction schema.
A formula is called bounded arithmetical, or Δ00, when all its quantifiers are of the form ∀n 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 Δ01 comprehension, plus Δ00 induction. Projective determinacy is the assertion that every two-player perfect information game with moves being natural numbers, game length ω and projective payoff set is determined, that is, one of the players has a winning strategy. A set is projective if and only if (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 Z2. Many natural propositions expressible in the language of second-order arithmetic are independent of Z2 and even ZFC but are provable from projective determinacy. Over a weak base theory (such as RCA0), projective determinacy implies comprehension and provides an essentially complete theory of second-order arithmetic — natural statements in the language of Z2 that are independent of Z2 with projective determinacy are hard to find. [12] ZFC + {there are n Woodin cardinals: n is a natural number} is conservative over Z2 with projective determinacy[citation needed], that is a statement in the language of second-order arithmetic is provable in Z2 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}. However, it is able to formalize other mathematical objects indirectly via coding techniques, a fact that was first noticed by Weyl. [17] The aforementioned coding works well for continuous and total functions, assuming a higher-order base theory plus weak Kőnig's lemma.