Stratified systems of logic

The suffixes used in logic to indicate differences of type may be regarded either as belonging to the formalism itself, or as being part of the machinery for deciding which rows of symbols (without suffixes) are to be admitted as significant. The two different attitudes do not necessarily lead to different formalisms, but when types are regarded as only one way of regulating the calculus it is natural to consider other possible ways, in particular the direct characterization of the significant formulae. Direct criteria for stratification were given by Quine, in his ‘New Foundations for Mathematical Logic’ (7). In the corresponding typed form of this theory ordinary integers are adequate as type-suffixes, and the direct description is correspondingly simple, but in other theories, including that recently proposed by Church(4), a partially ordered set of types must be used. In the present paper criteria, equivalent to the existence of a correct typing, are given for a general class of formalisms, which includes Church's system, several systems proposed by Quine, and (with some slight modifications, given in the last paragraph) Principia Mathematica. (The discussion has been given this general form rather with a view to clarity than to comprehensiveness.)