Predicative Mathematics

Predicative mathematics is mathematics constructed without impredicative definitions — definitions that quantify over a totality to which the defined object itself belongs. The restriction was first imposed systematically in the ramified type theory of Principia Mathematica, where Russell and Whitehead attempted to eliminate the circularity they believed produced paradox.

The predicative program faces a fundamental tension: much of classical analysis relies on impredicative constructions. The least upper bound of a bounded set of real numbers, defined as the smallest number greater than or equal to every member, quantifies over the set of all upper bounds — a totality that includes the bound being defined. Predicative analysis can recover significant portions of mathematics — including the basic theorems of calculus — but cannot prove the existence of certain pathological functions and spaces that classical analysis takes for granted.

Modern predicative mathematics, developed by Solomon Feferman and others, uses systems of strength far below full ZFC but sufficient for scientifically applicable mathematics. The question whether nature requires impredicative mathematics — whether the physical world instantiates truths that cannot be proved predicatively — remains open. Constructive mathematics and type theory provide frameworks in which predicativity is not a restriction but a natural feature of the foundational architecture.