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 world and life’s too big to pass for a dream,”
—Robert Browning (1812–1889)
“This entire most beautiful order of good things is going to pass away after its measure has been exhausted; for both morning and evening were made in them.”
—St. Augustine (354–430)
“O! O! another stroke! that makes the third.
He stabs me to the heart against my wish.
If that be so, thy state of health is poor;
But thine arithmetic is quite correct.”
—A.E. (Alfred Edward)