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:
“Through a series of gradual power losses, the modern parent is in danger of losing sight of her own child, as well as her own vision and style. It’s a very big price to pay emotionally. Too bad it’s often accompanied by an equally huge price financially.”
—Sonia Taitz (20th century)
“I marvel at the many ways we, as black people, bend but do not break in order to survive. This astonishes me, and what excites me I write about. Everyone of us is a wonder. Everyone of us has a story.”
—Kristin Hunter (b. 1931)
“Under the dominion of an idea, which possesses the minds of multitudes, as civil freedom, or the religious sentiment, the power of persons are no longer subjects of calculation. A nation of men unanimously bent on freedom, or conquest, can easily confound the arithmetic of statists, and achieve extravagant actions, out of all proportion to their means; as, the Greeks, the Saracens, the Swiss, the Americans, and the French have done.”
—Ralph Waldo Emerson (1803–1882)