Ordinal analysis (Bachmann hierarchy)

Layer 0 — Mathematicsin the proof-theory subtree

Schutte-Bachmann ordinal-analysis: each formal theory T proves termination of recursion up to its proof-theoretic ordinal; ATR_0 -> Gamma_0; PA -> epsilon_0.