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:
“The true gardener then brushes over the ground with slow and gentle hand, to liberate a space for breath round some favourite; but he is not thinking about destruction except incidentally. It is only the amateur like myself who becomes obsessed and rejoices with a sadistic pleasure in weeds that are big and bad enough to pull, and at last, almost forgetting the flowers altogether, turns into a Reformer.”
—Freya Stark (1893–1993)
“Children and old people and the parents in between should be able to live together, in order to learn how to die with grace, together. And I fear that this is purely utopian fantasy ...”
—M.F.K. Fisher (1908–1992)
“‘Tis no extravagant arithmetic to say, that for every ten jokes,—thou hast got an hundred enemies; and till thou hast gone on, and raised a swarm of wasps about thine ears, and art half stung to death by them, thou wilt never be convinced it is so.”
—Laurence Sterne (1713–1768)