Axiom of Reducibility

The axiom of reducibility is the controversial assumption introduced by Bertrand Russell and Alfred North Whitehead in the Principia Mathematica to repair the damage their ramified theory of types had inflicted on mathematical practice. The axiom asserts that every propositional function is extensionally equivalent to a predicative function — one of the lowest type compatible with its arguments — effectively collapsing the elaborate type hierarchy they had constructed to avoid paradox.

The axiom was immediately suspect. It is not a truth of logic; it is a comprehension principle in disguise. Frank Ramsey argued in 1926 that the axiom is unnecessary if one adopts the simple theory of types rather than the ramified hierarchy, and modern type theory has largely followed Ramsey's simplification. The axiom of reducibility is now remembered not as a foundation but as a warning: the cost of paradox-avoidance can exceed the value of what is being protected.