Fragments of Peano Arithmetic (IΣₙ)

Origin. Parsons, Mints, and Takeuti independently characterized the provably total functions of IΣ₁ (early 1970s). Paris and Kirby developed the model theory of the IΣₙ and BΣₙ hierarchies through the late 1970s; Paris and Harrington (1977) gave the first natural sentence independent of PA, sited exactly by this hierarchy. Hájek and Pudlák's Metamathematics of First-Order Arithmetic (1993) is the reference.

Models. PA's axioms with induction restricted by quantifier complexity. The result is not one theory but a hierarchy that does not collapse: IΣ₁ ⊊ IΣ₂ ⊊ ⋯ ⊊ PA, each level strictly stronger, each with its own class of provably total functions and its own ordinal. Where Bounded Arithmetic restricts quantifiers to terms, this axis leaves quantifiers unbounded and restricts induction — a different cut through the same theory, and the one that measures ordinary strength.

Formalism.

Language: 0, S, +, ×, < — PA's.

Schemata: IΣₙ: induction for Σₙ formulas. IΠₙ: induction for Πₙ formulas. IΣₙ and IΠₙ are equivalent for n ≥ 1. BΣₙ: collection (bounding), ∀x<a ∃y φ(x,y) → ∃b ∀x<a ∃y<b φ(x,y), for Σₙ φ.

The hierarchy, strict at every level: IΔ₀ ⊊ IΣ₁ ⊊ IΣ₂ ⊊ ⋯ ⊊ PA = ⋃ₙ IΣₙ Collection interleaves strictly between the induction levels (Paris–Kirby): IΣₙ ⊊ BΣ_{n+1} ⊊ IΣ_{n+1}

Provably total functions: IΣ₁ — the primitive recursive functions (Parsons, Mints, Takeuti). Hence IΣ₁ is Π⁰₂-conservative over PRA, which is why finitistic reducibility arguments stop here. IΣₙ — the functions in the n-th level of the Grzegorczyk-style hierarchy generated by the ordinal ωₙ. PA — the < ε₀-recursive functions.

Proof-theoretic ordinals: |IΣ₁| = ω^ω, |IΣ₂| = ω^ω^ω, |IΣₙ| = ω_{n+1}, |PA| = ε₀ = sup ω_n.

Independence, sited: Paris–Harrington (1977): the strengthened finite Ramsey theorem is true, Π⁰₂, and unprovable in PA. Goodstein's theorem (Kirby–Paris 1982): unprovable in PA, provable with ε₀-induction. The Kanamori–McAloon and Friedman finite-tree statements sit similarly. Each is placed by the Wainer hierarchy: a statement whose witnessing function grows faster than every < ε₀-recursive function is unprovable in PA, and the fragments give the finer siting.

Interpretability: IΔ₀ is interpretable in S¹₂, and S¹₂ in Q; so IΔ₀ ≡ᵢ Q. The fragments above IΔ₀+exp are not.

Symbols.

Metatheory. The hierarchy is strict, so PA is not finitely axiomatizable — any finite subset lives inside some IΣₙ, and IΣ_{n+1} proves Con(IΣₙ). Each level's provably total functions form a proper subclass of the next's, and the fast-growing hierarchy F_α makes the correspondence exact: IΣₙ proves the totality of F_α precisely for α < ω_{n+1}. This is what turns independence from a Gödelian construction into a measurement — Paris–Harrington is unprovable in PA not because it encodes a self-referential trick but because its Ramsey function dominates every < ε₀-recursive function, and the same calculation places each statement at its level. The Π⁰₂-conservativity of IΣ₁ over PRA is the sharpest form of the finitistic reduction, and it is a theorem about a fragment, not about PA.

Applies to. Ordinal analysis, where the fragments are the objects analyzed. Independence results and the calibration of combinatorial statements against the Wainer hierarchy. Reverse mathematics — RCA₀ and WKL₀ have IΣ₁ as their first-order part, ACA₀ has PA. Formalization of metamathematics, where the question is always which fragment suffices. Model theory of arithmetic: cuts, initial segments, and end-extensions are the tools that separate the levels.

Limitations. The hierarchy is unbounded and PA is the union, so no single fragment is "the" theory of arithmetic; results must specify the level, and levels above IΣ₂ are rarely needed for anything but the hierarchy itself. The provably-total characterizations are exact but the ordinals are notation-dependent — the analysis presupposes an ordinal notation system whose well-foundedness is not provable in the theory being analyzed. Collection and induction interleave in a way that has no simple statement, and the BΣₙ levels are easy to state and hard to use. Below IΔ₀+exp the classification breaks down and the bounded arithmetic axis takes over.

© 2026 Lingenic LLC