 Second-order arithmetic

Second-order arithmetic has variables for natural numbers and for sets of natural numbers. Subsystems restrict comprehension and induction; arithmetical transfinite recursion theory is one important subsystem stronger than the first-order system Peano arithmetic.

Second-order arithmetic is a foundational system in mathematical logic and set theory that extends first-order arithmetic by allowing quantification over sets of natural numbers, in addition to quantifying over individual natural numbers. In first-order arithmetic, the language contains symbols for natural numbers, addition, multiplication, and logical connectives, as well as quantification over individual natural numbers. A typical axiom system for first-order arithmetic is Peano Arithmetic (PA).