 Church’s (1976) formulation of the logic of PM with r-types The language of the higher-order quantificational logic of PM is called ramified type theory, and the system of types, following Church (1976) will be called r-types. Note that there are two kinds of variables, but they are all assigned to an r-type. Individual variables behave as a special case of propositional function variables.