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:
“There are big men, men of intellect, intellectual men, men of talent and men of action; but the great man is difficult to find, and it needs—apart from discernment—a certain greatness to find him.”
—Margot Asquith (1864–1945)
“What an infernal set of fools those schoolmarms must be! Well, if in order to please men they wish to live on air, let them. The sooner the present generation of women dies out, the better. We have idiots enough in the world now without such women propagating any more.”
—Elizabeth Cady Stanton (1815–1902)
“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)