 Given that the system of PM contains a ramified theory of types, however, the move to discussion of classes for the remainder of the work after ∗20 requires a further axiom, the axiom of reducibility, in order to allow a simple theory of types of classes. Consider the fundamental notion from the theory of real numbers of the least upper bound (l.u.b.) of a bounded class of real numbers. Consider the class of all real numbers whose square is less than or equal to 2, i.e., \(\{ x \mid x^2 \leq 2\}\). A class of reals S has an upper bound if and only if \(\exists r \forall s ( s \in S \supset s \leq r)\). If a bounded class S of real numbers has members of some r-type \(\tau\), then the least upper bound must belong to an r-type \(\tau / 1\) because of the quantifier in the definition ranging over the elements s of S. We say that the definition of S is “impredicative” because it involves quantification over a totality to which it is intended to belong. The theory of real numbers, however, requires that sometimes the least upper bound of a class is a member of that class, in this case, the least upper bound of S, namely \(\sqrt{2}\), is an element of S.