 That is, \(f \hat{\alpha}\) is an expression naming the function which takes a function \(\phi\) to a proposition which asserts \(f\) of the class of \(\phi\)s. (The modern notation shows that in the proposed definition of \(f \hat{\alpha}\) in PM notation, we shouldn’t expect \(\alpha\) in the definiens, since it is really a bound variable in \(f \hat{\alpha}\); similarly, we shouldn’t expect \(\phi\) in the definiendum because it is a bound variable in the definiens.) One might also expect definitions like ∗20·07 and ∗20·071 to hold for cases in which the Roman letter “\(z\)” is replaced by a Greek letter. The definitions in PM are thus not complete, but it is possible to guess at how they would be extended to cover all occurrences of Greek letters. This would complete the project of the “no-classes” theory of classes by showing how all talk of classes can be reduced to the theory of propositional functions.