Axiom introduced by Russell and Whitehead in Principia Mathematica. In that system propositional functions are sorted into levels, as part of the ramified theory of types. The axiom says that for any function at any level there exists a formally equivalent function at the first level. The axiom is needed to allow the construction of elementary mathematics, in particular to certify the principle of mathematical induction. Its effect, as Ramsey pointed out, was largely to nullify the point of introducing different orders of functions.