 Interestingly, the basic idea underlying Russell’s ramified hierarchy of types is a crucial ingredient in Gödel’s later consistency proof of the continuum hypothesis via its inner model \(L\) of constructible sets. Also, as already observed in Gödel (1944), a form of AR becomes true in \(L\) in the sense that, roughly, an arbitrary propositional function of natural numbers is extensionally equivalent to some function of order \(\alpha\), for some countable ordinal \(\alpha\) (see the entry  Kurt Gödel).  Other important applications of ramified hierarchies have been given since the late fifties in different fields (from recursion theory to proof theory; see the entry on  type theory).