# Russell and Whitehead's types: ramified and unramified

I was reading Logicomix (a fictionalised account of logic from Frege to Gödel through Russell's eyes) and there was mention about two different versions of types developed by Russell and Whitehead for Principia Mathematica, unramified (first) and ramified. I don't expect that there is too much relation to the modern type theory (or is there?), but I'm curious to know what the difference is between them. In particular, it is stated that unramified types were not sufficient. How so?

I know the intuitive description of RW's types as a hierarchy of sets, but nothing beyond that.

-
A quick Google search brings up plato.stanford.edu/entries/type-theory . –  Qiaochu Yuan Jun 11 '10 at 8:12
+1 for reading Logicomix –  Michael Blackmon Jan 27 '11 at 9:57

Yes, this still occurs in modern type theory; in particular, you'll find it in the calculus of constructions employed by the Coq language.

Consider the type called Prop, whose inhabitants are logical propositions (which are in turn inhabited by proofs). The type Prop does not belong to Prop -- this means that Prop exhibits stratification:

Check Prop.
Prop
: Type


However, note that (forall a:Prop, a) does have type Prop. So although Prop does not belong to Prop, things which quantify over all of Prop may still belong to Prop. So we can be more specific and say that Prop exhibits unramified stratification.

Check (forall a:Prop, a).
forall a : Prop, a
: Prop


By contrast, consider Set, whose inhabitants are datatypes (which are in turn inhabited by computations and the results of computations). Set does not belong to itself, so it too exhibits stratification:

Check Set.
Set
: Type


Unlike the previous example, things which quantify over all of Set do not belong to Set. This means that Set exhibits ramified stratification.

Check (forall a:Set, a).
forall a : Set, a
: Type


So, in short, "ramification" in Russell's type hierarchy is embodied today by what Coq calls "predicative" types -- that is, all types except Prop. If you quantify over a type, the resulting term no longer inhabits that type unless the type was impreciative (and Prop is the only impredicative type).

The higher levels of the Coq universe (Type) are also ramified, but Coq hides the ramification indices from you unless you ask to see them:

Set Printing Universes.
Check (forall a:Type, Type).
Type (* Top.15 *) -> Type (* Top.16 *)
: Type (* max((Top.15)+1, (Top.16)+1) *)


Think of Top.15 as a variable, like $\alpha_{15}$. Here, Coq is telling you that if you quantify over the $\alpha_{15}^{th}$ universe to produce a result in the $\alpha_{16}^{th}$ universe, the resulting term will fall in the $max(\alpha_{15}+1, \alpha_{16}+1)^{th}$ universe -- which is at least "one level up" from what you're quantifying over.

Just as it was later discovered that Russell's ramification was unnecessary (for logic), it turns out that predicativity is unnecessary for the purely logical portion of CiC (that is, Prop).

-
I'd like to add that impredicativity of Prop gives CiC a huge amount of logical strength that isn't available in other systems (such as Agda). CiC's impredictativity allows you to build honest power sets that, as far as I know, can't be done in Agda. One application is Benjamin Werner model of Z in Coq. Whether this is a good thing or not depends on what your opinion of strong theories is, and if you think Z is consistent or not. –  Russell O'Connor Jun 27 '10 at 22:09

Here is an interesting quote from Gödel about PM and ramified type theory therein that is of some relevance:

It is to be regretted that this first comprehensive and thorough-going presentation of a mathematical logic and the derivation of mathematics from it is so greatly lacking in formal precision in the foundations (contained in *1-*21 of Principia) that it presents in this respect a considerable step backwards as compared with Frege (Collected Works, Volume II, p. 120)

I read this at http://www.cs.nyu.edu/pipermail/fom/2011-July/015668.html, an email by Alasdair Urquhart to the fom mailing list. Urqhart also says that Church, Myhill and Schutte gave formalisations of ramified type theory, but the relevance of these to PM is unclear

-

You can find an excellent introduction to the evolution of type theory from Russell all the way to the Calculus of Constructions (as mentioned in the answer by Adam) in a book A modern perspective on type theory by Fairouz Kamereddine, Twan Laan, and Rob Nederpelt. This book walks you through most of the historically important developments, with a definite emphasis on the even lesser known (but splendid!) logical work embodied by AUTOMATH.

-