The Big Five Subsystems of Second Order Arithmetic
Second order arithmetic is a formal theory of the natural numbers and sets of natural numbers. Many mathematical objects, such as countable rings, groups, and fields, as well as points in effective Polish spaces, can be represented as sets of natural numbers, and modulo this representation can be studied in second order arithmetic.
Reverse mathematics makes use of several subsystems of second order arithmetic. A typical reverse mathematics theorem shows that a particular mathematical theorem T is equivalent to a particular subsystem S of second order arithmetic over a weaker subsystem B. This weaker system B is known as the base system for the result; in order for the reverse mathematics result to have meaning, this system must not itself be able to prove the mathematical theorem T.
Simpson (2009) describes five particular subsystems of second order arithmetic, which he calls the Big Five, that occur frequently in reverse mathematics. In order of increasing strength, these systems are named by the initialisms RCA0, WKL0, ACA0, ATR0, and Π11-CA0.
The following table summarizes the "big five" systems Simpson (2009, p.42)
| Subsystem | Stands for | Ordinal | Corresponds roughly to | Comments |
|---|---|---|---|---|
| RCA0 | Recursive comprehension axiom | ωω | Constructive mathematics (Bishop) | The base system for reverse mathematics |
| WKL0 | Weak König's lemma | ωω | Finitistic reductionism (Hilbert) | Conservative over PRA for Π0 2 sentences. Conservative over RCA0 for Π1 1 sentences. |
| ACA0 | Arithmetical comprehension axiom | ε0 | Predicativism (Weyl, Feferman) | Conservative over Peano arithmetic for arithmetical sentences |
| ATR0 | Arithmetical transfinite recursion | Γ0 | Predicative reductionism (Friedman, Simpson) | Conservative over Feferman's system IR for Π1 1 sentences |
| Π1 1-CA0 |
Π1 1 comprehension axiom |
Ψ0(Ωω) | Impredicativism |
The subscript 0 in these names means that the induction scheme has been restricted from the full second-order induction scheme (Simpson 2009, p. 6). For example, ACA0 includes the induction axiom (0∈X ∧ ∀n(n∈X → n+1∈X)) → ∀n n∈X. This together with the full comprehension axiom of second order arithmetic implies the full second-order induction scheme given by the universal closure of (φ(0) ∧ ∀n(φ(n) → φ(n+1))) → ∀n φ(n) for any second order formula φ. However ACA0 does not have the full comprehension axiom, and the subscript 0 is a reminder that it does not have the full second-order induction scheme either. This restriction is important: systems with restricted induction have significantly lower proof-theoretical ordinals than systems with the full second-order induction scheme.
Read more about this topic: Reverse Mathematics
Famous quotes containing the words big, order and/or arithmetic:
“Tom: All right, boys. C’mon. Why don’t you say I’m a yellow belly and a big mouth at that?
Shep: You yellow? Who thinks you’re yellow? Did you hear what he said? A guy who’s got the nerve to marry? That’s more than Flash Gordon ever did.”
—Billy Wilder (b. 1906)
“Since [Rousseau’s] time, and largely thanks to him, the Ego has steadily tended to efface itself, and, for purposes of model, to become a manikin on which the toilet of education is to be draped in order to show the fit or misfit of the clothes. The object of study is the garment, not the figure.”
—Henry Brooks Adams (1838–1918)
“Your discovery of the contradiction caused me the greatest surprise and, I would almost say, consternation, since it has shaken the basis on which I intended to build my arithmetic.... It is all the more serious since, with the loss of my rule V, not only the foundations of my arithmetic, but also the sole possible foundations of arithmetic seem to vanish.”
—Gottlob Frege (1848–1925)