Cumulative versus noncumulative ramified types (Q1130235)

In Church's reconstruction of the ramified theory of types, the range of a variable of a given type includes the range of every variable of directly lower type (syntactic cumulativeness). It may also be that if constants form a form/function pair of a given order, then they are true for all higher orders (semantic cumulativeness). Semantic cumulativeness implies syntactic cumulativeness, but not vice versa. One may thus have a ramified theory of types which is (1) semantically cumulative, (2) merely syntactically cumulative (Church's position), or (3) noncumulative. It is argued that (3) offers the most satisfactory solution of the Grelling paradox (\(\ulcorner\phi\urcorner\) is not a \(\phi\) word), and that (1) is the least satisfactory solution to the Bouleus paradox (I believe that at least one of my beliefs is false). The difference between (1) and (2) with respect to paradox solutions would not have been expected. Cumulativeness does not alleviate the need for an axiom of reducibility, nor does noncumulativeness render the expression of that axiom problematic. But a noncumulative theory would require either abandoning circumflexion as a predicate term forming operator, or a predicativity restriction on the abstraction principle, to save Russell's theory of classes.