What does the ramified in ramified type theory mean?

Question

I've recently become intrigued by the ramified type theory of Russell and Whitehead, for various reasons. I had thought it had been superseded by all the work since then. But now, I wonder whether I had made a mistake. If so, it seems a mistake common to the set theory and logic texts I've seen.

Q. Is this simply due to the hegemony that ZFC exerts upon the mathematical imagination?

Q. What does ramify in ramified type theory mean? I've taken the liberty of looking up ramify in a dictionary, and there it mentions that it means branching.

edit

@David Roberts: I've hardly seen in mentioned in the set theory books I've looked; but not being a specialist in set theory, I haven't looked that far.

@Gerald Edgar: Thanks. So, I've discovered. According to one article, I've read: ZFC < Higher order logic < ZFC + one inaccessible cardinal.

@Andrej Bauer: ZFC hegemony is quite clear to me as I've discovered just how many ways of thinking about logic and sets there are, and how little they are mentioned in textbooks. But perhaps that's not fair to textbook writers ... I've also been browsing that article. But I thought I may as well ask here.

I apologise for answering here: my phone is not allowing me to add comments.

Answer 1

As far as I know, the word "ramified", in reference to type theory, means that one pays attention not only to the ranks of sets (where sets of rank $n$ have members of rank $n-1$) but also to the complexity of their definitions. So for example, a set of fairly low rank, like a set of natural numbers, might be defined by a formula that quantifies over sets of high ranks and would be considered to have high "level". The comprehension axioms of such a type theory would impose limitations on both the ranks and the levels of the sets involved.

This rather complicated arrangement was introduced in Russell and Whitehead's "Principia Mathematica" to enforce predicativity of their type theory. Unfortunately, it proved too restrictive to serve as a foundation of ordinary mathematics, so it was supplemented with an "axiom of reducibility", saying that any set of high level is extensionally equal to (i.e., has the same members as) some set of suitably low level. Afterward (around 1920, I think) Chwistek and Ramsey (independently) noticed that the reducibility axiom had the effect of completely annihilating the structure of levels. So the theory can be reformulated by ignoring levels and working with ranks alone. This is now called either "simple type theory" or just "type theory".

The idea of levels resurfaced in Gödel's definition of the constructible universe $L$. There a set is put into $L_{\alpha+1}$ if (1) all its members are in $L_\alpha$ and (2) it is defined using quantification only over $L_\alpha$. Here, (1) is analogous to a limitation on ranks, and (2) is analogous to a limitation on levels.