  Ramsey rightly saw that a ‘simple’ theory of types (sometimes called ‘ramseyfied’) that distinguishes types of propositional functions by their arguments would deal with ‘logical’ paradoxes, but in order to deal with the other paradoxes, Whitehead and Russell had introduced a ‘branched’ or ‘ramified’ theory of types with a hierarchy of levels of functions (and of propositions), that led to further difficulties, one of which being the inability even to formulate theorems of classical mathematics such as the least upper bound theorem, unless one introduced the ‘Axiom of Reducibility’ according to which for any function at any level there exists an equivalent one at the first level (1925a, [PP] 187–192). (Another worry, that one could not formulate mathematical induction in its full generality turns out to have been unfounded.)  Wittgenstein had pointed out in the Tractatus that it is not a tautology (6.1233), so that it could hardly serve as an axiom. To circumvent this, Ramsey introduced his own notion of ‘predicative function’ and showed that if one gets rid of the ‘vicious-circle principle’, the levels can be collapsed and the need for the ‘Axiom of Reducibility’ is obviated (1925a, [PP] 195–205). Thus, Ramsey had in effect shown how to deal with the paradoxes and the ‘extensionality’ of mathematics without the need for a ‘ramified’ theory of types. (In this he was preceded by Leon Chwistek (Chwistek 1921).) This, Ramsey concluded, would secure mathematics against the “Bolshevik menace” of the intuitionist critique of Brouwer and Weyl (1925a, [PP] 219).