Second-order arithmetic

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. 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” (Sieg 2013, p. 291). 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. 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 ⋅ {displaystyle cdot } (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 L = { 0 , S , + , ⋅ , = , < , ∈ } {displaystyle {mathcal {L}}={0,S,+,cdot ,=,<,in }} . For example, ∀ n ( n ∈ X → S n ∈ X ) {displaystyle forall n(nin X ightarrow Snin X)} , 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 ∃ X ∀ n ( n ∈ X ↔ n < S S S S S S 0 ⋅ S S S S S S S 0 ) {displaystyle exists Xforall n(nin Xleftrightarrow n<SSSSSS0cdot SSSSSSS0)} is a well-formed formula that is not arithmetical, having one bound set variable X and one bound individual variable n. 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 number 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 number variables (Shapiro 1991, pp. 74–75).