 Although PM does not single out first order logic from the whole ramified theory of types, the actual deductive apparatus on the page looks exactly like a system of first order logic, and the complications of the logic of higher types can be expressed with an additional apparatus of type indices. In what follows we will use the system of r-types in Church (1976) for type indices, and the use of lambda operators for propositional functions.