 Russell’s Axiom of Reducibility in type theory states that every propositional function is coextensive with a predicative one—that is, one whose quantifiers range only over types lower than that of the propositional function itself. The non-trivial content of this axiom is that every impredicative propositional function is coextensive with a predicative one. A well known example to illustrate this is the impredicative propositional function ∀F(Fx ↔ Fy). The Axiom of Reducibility could be vindicated on this example by adducing the predicative propositional function x = y—provided that one accepts Leibniz’s controversial principle of the identity of indiscernibles. If, contra Leibniz, one believes it is possible for indiscernibles to be distinct, then, in order to vindicate the Axiom of Reducibility, it would be necessary to adduce some other predicative propositional function, x ∼ y say, for which it is true that 