 Arithmetical comprehension theory

This subsystem of second-order arithmetic allows comprehension for arithmetical formulas and induction in its standard restricted presentation. Its first-order arithmetical consequences are those of Peano arithmetic. It is a useful base for comparing well-quasi-ordering principles with ordinal notation systems without assuming their global well-foundedness.