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 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.