 In this theory, predicative functions of one argument, i.e., those having as order the successor of the order of their argument, play a crucial role. For instance, a predicative function of an individual variable must have order 1 (in current terminology, it is elementarily definable and quantifies only over individuals). The axiom of reducibility (AR) states that every propositional function is equivalent, for all its values, to a predicative function of the same variables. So, for instance, we might have a definition of a property \(P(n)\) of natural numbers (regarded as individuals) which quantifies over, say, second-order propositions. But AR implies that there exists a function \(P^* (n)\) which is satisfied by exactly the same numbers as \(P(n)\) and is predicative, i.e., it involves quantification only on numbers.