Second-order Arithmetic - Stronger Systems

Stronger Systems

Much as we have defined Σ_n and Π_n (or, more accurately, Σ0_n and Π0_n) formulae, we can define Σ1_n and Π1_n formulae in the following way: a Δ1₀ (or Σ1₀ or Π1₀) formula is just an arithmetical formula, and a Σ1_n, respectively Π1_n, formula is obtained by adding existential, respectively universal, class quantifiers in front of a Π1_n−1, respectively Σ1_n−1.

It is not too hard to see that over a not too weak system, any formula of second-order arithmetic is equivalent to a Σ1_n or Π1_n formula for all large enough n. The system Π1₁-comprehension is the system consisting of the basic axioms, plus the ordinary second-order induction axiom and the comprehension axiom for every Π1₁ formula φ. It is an easy exercise to show that this is actually equivalent to Σ1₁-comprehension (on the other hand, Δ1₁-comprehension, defined by the same trick as introduced earlier for Δ0₁ comprehension, is actually weaker).