Predicativity: The Outer Limits

Stephen G. Simpson


Beginning with ideas of Poincaré and Weyl, Feferman in the sixties undertook a profound analysis of the predicativist foundational program. He presented a subystem of second order arithmetic $\mathsf{IR}$ and argued convincingly that it represents the outer limits of what is predicatively provable. Much later, Friedman introduced another system $\mathsf{ATR}_0$ which is conservative over $\mathsf{IR}$ for $\Pi^1_1$ sentences yet includes several well known theorems of algebra, descriptive set theory, and countable combinatorics that are not provable in $\mathsf{IR}$. The proof-theoretic ordinal of both systems is $\Gamma_0$. $\mathsf{ATR}_0$ has emerged as one of a handful of systems that are important for reverse mathematics. From a foundational standpoint, we may say that $\mathsf{IR}$ represents predicative provability while $\mathsf{ATR}_0$ represents predicative reducibility. Subsequently Friedman formulated mathematically natural finite combinatorial theorems that are not only not predicatively provable but go beyond $\Gamma_0$ and therefore are not predicatively reducible. I plan to report on recent developments in this area.