Second-order arithmetic

From Wikipedia, the free encyclopedia

In mathematical logic, second-order arithmetic is a formal system for studying the natural numbers and subsets of the natural numbers. It can be thought of as a stronger version of Peano arithmetic that allows quantification over both numbers and sets of numbers.

Second-order arithmetic can also be thought of as a weaker version of set theory in which all the sets are either natural numbers or sets of natural numbers. Although it is much weaker than Zermelo-Fraenkel set theory, second-order arithmetic is already a very strong axiom system, much stronger than is needed to do essentially all of classical mathematics that it is able to express in its language. For example, it is possible to develop a formal theory of the real numbers in second-order arithmetic, in which quantification over sets of natural numbers allows quantification over the set of real numbers. For this reason, second-order arithmetic is sometimes called “analysis”.

The program of Reverse Mathematics uses subsystems of second-order arithmetic to measure the level of nonconstructivity of mathematical theorems. The reason that second-order arithmetic was chosen for this program is that much of core mathematics can be formalized in weak subsystems of second-order arithmetic. Some of these subsystems are defined below.

1 The language
2 The semantics
3 Basic axioms
4 Induction and comprehension axioms
5 The full system
6 Models of second-order arithmetic
7 Subsystems of second-order arithmetic
8 Coding mathematics in second-order arithmetic
9 See also
10 References

[edit] The language

The language of second-order arithmetic is a two-sorted language. The first sort of terms and variables, usually written in lower case, refer to individuals/numbers, which can be thought of as natural numbers. The other sort of variables, called “set variables” or “class variables” or “predicates” and usually written in upper case, refer to classes/predicates/properties of individuals, which can be thought of as sets of natural numbers. Both individuals and predicates can be quantified, universally or existentially. A formula which has no bound set variables (that is, no quantifiers over set variables) is known as arithmetical. Arithmetical formulas may have free set variables and bound number variables.

Individual terms can be formed by the constant 0, the unary function S (the successor function) and the binary operations + and · (addition and multiplication). The successor function yields a natural number one larger than its input. The relations = (equality) and < (comparison of natural numbers) relate two individuals, whereas the relation ∈ (membership) relates an individual and a class.

For example $\forall n (n\in X \rightarrow Sn \in X)$ is a well-formed formula of second-order arithmetic which is arithmetical, which has one free class variable X and one bound individual variable n (but no bound class variables, as is required of an arithmetical formula), whereas $\exists X \forall n(n\in X \leftrightarrow n < SSSSSS0\cdot SSSSSSS0)$ is a well-formed formula which is not arithmetical with one bound set variable X and one bound individual variable n.

[edit] The semantics

Several different interpretations of the quantifiers are possible. If second-order arithmetic is studied using 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 first-order 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 number variables. Although some have argued that second-order arithmetic should be studied with full second-order semantics, the vast majority of current research treats second-order arithmetic in first-order predicate calculus. This is because the model theory of subsystems of second-order arithmetic is more interesting in the setting of first-order logic.

[edit] Basic axioms

The following axioms are known as the basic axioms, or sometimes the Robinson axioms. The first-order system they define, known as Robinson arithmetic, is essentially Peano arithmetic without induction.

$\forall m (Sm=0 \rightarrow \bot)$ (“the successor of a natural number is never zero”)
$\forall m \forall n (Sm=Sn \rightarrow m=n)$ (“the successor function is injective”)
$\forall n (0=n \lor \exists m (Sm=n))$ (“every natural number is zero or a successor”)
$\forall m (m+0=m)$
$\forall m \forall n (m+Sn = S(m+n))$
$\forall m (m\cdot 0 = 0)$
$\forall m \forall n (m \cdot Sn = (m\cdot n)+m)$
$\forall m (m<0 \rightarrow \bot)$
$\forall m (m<Sn \leftrightarrow (m<n \lor m=n))$
$\forall n (0=n \lor 0<n)$
$\forall m \forall n ((Sm<n \lor Sm=n) \leftrightarrow m<n)$

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).

[edit] Induction and comprehension axioms

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:

$\forall m_\bullet \forall X_\bullet ((\varphi(0) \land \forall n (\varphi(n) \rightarrow \varphi(Sn)) \rightarrow \forall n \varphi(n))$

One particularly important instance of this axiom 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 “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:

$\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.

[edit] 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, which we define below. If second-order semantics are used then no comprehension axiom is required, 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 first-order induction scheme. In subsystems described below in which comprehension is limited, sometimes part of the first order induction scheme is added to compensate.

[edit] 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 of subsets of M which is the range of the set variables. By omitting the latter we obtain a model of the language of first order arithmetic.

When the set of subsets of M is the full powerset of M, we speak of a full model. If we used second-order semantics, we would essentially limit ourselves to studying only full models. In fact, the axioms of second-order arithmetic have only one model under full second-order semantics. This follows from the fact that the axioms of first-order 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, we say that M is an ω-model. In this case we may identify the model with its collection of sets of naturals, since this is enough to completely determine an ω-model.

The only full ω-model, in other words 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. It is clearly a model of full second-order arithmetic.

[edit] Subsystems of second-order arithmetic

A subsystem of second-order arithmetic is a theory in the same language whose axioms are all provable from the axioms of full second-order arithmetic. Such subsystems are essential to the program of Reverse mathematics.

[edit] 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 $ACA 0$ .

$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 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 $ACA 0$ if and only if S is closed under Turing jump, Turing reducibility, and Turing join.

The subscript 0 in $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 $ACA 0$ plus induction for all formulas is sometimes called $ACA$ .

The system $ACA 0$ 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 ε₀ (this is because of the limited induction).

[edit] The arithmetical hierarchy for formulas

Main article: Arithmetical hierarchy

To define a second subsystem, we will need a bit more terminology.

A formula is called bounded arithmetical, or Δ⁰₀, 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<t(\cdots)$

stands for

$\forall n(n<t \rightarrow \cdots)$

and

$\exists n<t(\cdots)$

stands for

$\exists n(n<t \land \cdots)$ .

A formula is called Σ⁰₁ (or sometimes Σ₁), respectively Π⁰₁ (or sometimes Π₁) 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 Σ⁰_n, respectively Π⁰_n when it is obtained by adding existential, respectively universal, individual quantifiers to a Π⁰_n−1, respectively Σ⁰_n−1 formula (and Σ⁰₀ and Π⁰₀ are all equivalent to Δ⁰₀). 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 Σ⁰_n or Π⁰_n formula for all large enough n.

[edit] Recursive Comprehension

The subsystem $RCA 0$ is an even weaker system than $ACA o$ and is often used as the base system in Reverse Mathematics. It consists of: the basic axioms, the Σ⁰₁ induction scheme, and the Δ⁰₁ comprehension scheme. The former term is clear: the Σ⁰₁ induction scheme is the induction axiom for every Σ⁰₁ formula φ. The term “Δ⁰₁ comprehension” requires a little more explaining, however: there is no such thing as a Δ⁰₁ formula (the intended meaning is a formula which is both Σ⁰₁ and Π⁰₁), but we are instead postulating the comprehension axiom for every Σ⁰₁ formula subject to the condition that it is equivalent to a Π⁰₁ formula, in other words, for every Σ⁰₁ formula φ and every Π⁰₁ formula ψ we postulate

$\forall m_\bullet \forall X_\bullet ((\forall n (\varphi(n) \leftrightarrow \psi(n))) \rightarrow \exists Z \forall n (n\in Z \leftrightarrow \varphi(n)))$

$RCA 0$ is a conservative extension of Peano arithmetic with induction restricted to Σ⁰₁ formulas, and has proof theoretic ordinal ω^ω (because of the limited induction).

It can be seen that a collection S of subsets of ω determines an ω-model of $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 $RCA 0$ . This is the motivation behind the name of this system --- if a set can be proved to exist using $RCA 0$ , then the set is computable (i.e. recursive).

[edit] Weaker systems

Sometimes an even weaker system than $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 Δ⁰₁ comprehension plus Δ⁰₀ induction.

[edit] Stronger systems

Much as we have defined Σ_n and Π_n (or, more accurately, Σ⁰_n and Π⁰_n) formulae, we can define Σ¹_n and Π¹_n formulae in the following way: a Δ¹₀ (or Σ¹₀ or Π¹₀) formula is just an arithmetical formula, and a Σ¹_n, respectively Π¹_n, formula is obtained by adding existential, respectively universal, class quantifiers in front of a Π¹_n−1, respectively Σ¹_n−1.

It is not too hard to see that over a not too weak system, any formula of second-order arithmetic is equivalent to a Σ¹_n or Π¹_n formula for all large enough n. The system Π¹₁-comprehension is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every Π¹₁ formula φ. It is an easy exercise to show that this is actually equivalent to Σ¹₁-comprehension (on the other hand, Δ¹₁-comprehension, defined by the same trick as introduced earlier for Δ⁰₁ comprehension, is actually weaker).

[edit] Coding mathematics in second-order arithmetic

Second-order 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 first-class citizens in the same manner as natural numbers. Functions between these sets can be encoded as sets of pairs, so as subsets of the natural numbers, without difficulty. Real numbers can be defined as Cauchy sequences of rational numbers, but for technical reasons which we will not go into (in the weak axiom systems) it is preferable to put an actual constraint on the convergence rate (say, asking that the distance between the n-th and (n+1)-th term is less than 2⁻ⁿ). Real functions, or subsets of the reals, cannot be spoken of directly in the system, but continuous real functions are legitimate objects of study since they are defined by their values on the rationals, and by a similar trick it is possible to speak, for example, of open subsets of the reals. Even Borel sets of reals can be coded in the language of second-order arithmetic (though it is a bit tricky).

[edit] See also

[edit] References

Takeuti, Proof theory ISBN 0-444-10492-5
S. R. Buss, Handbook of proof theory ISBN 0-444-89840-9
Stephen G. Simpson, Subsystems of Second Order Arithmetic. Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999. ISBN 3-540-64882-8.

Retrieved from "http://en.wikipedia.org../../../s/e/c/Second-order_arithmetic.html"

Category: Mathematical logic