## Predicativity: The Outer Limits

Stephen G. Simpson

**Abstract**

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 IR and argued convincingly that it represents the outer
limits of what is predicatively provable. Much later, Friedman
introduced another system ATR0 which is conservative over IR for Pi11
sentences yet includes several well known theorems of algebra,
descriptive set theory, and countable combinatorics that are not
provable in IR. The proof-theoretic ordinal of both systems is
Gamma0. ATR0 has emerged as one of a handful of systems that are
important for reverse mathematics. From a foundational standpoint, we
may say that IR represents predicative provability while ATR0
represents predicative reducibility. Subsequently Friedman formulated
mathematically natural finite combinatorial theorems that are not only
not predicatively provable but go beyond Gamma0 and therefore are not
predicatively reducible. I plan to report on recent developments in
this area.