show/hide this revision's text 4 added 475 characters in body; deleted 97 characters in body; added 19 characters in body

Consider the type called Prop, whose inhabitants are logical propositions (which are in turn inhabited by proofs). The fact that type Prop itself does not have type belong to Prop is an example of unramified -- this means that Prop exhibits stratification(if Prop:Prop then the calculus would be unstratified, but also inconsistent).:

However, note that (forall a:Prop, a):Propa) does have type Prop. So although Prop doesn't " does not belong to itself"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.

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

Check Set (assuming you're not using the old deprecated -impredicative-set" mode).This is an 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.
show/hide this revision's text 3 added 542 characters in body

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

The fact that Prop itself does not have type Prop is an example of unramified stratification (if Prop:Prop then the calculus would be unstratified, but also inconsistent).

Check Prop.
Prop
 : Type

However, note that (forall a:Prop, a):Prop as shown below does have type Prop. So although Prop doesn't "belong to itself", things which quantify over all of Prop still belong to Prop:

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

The fact that

By contrast, (forall a:Set, a) does not have type Set is an example of ramified stratification (assuming you're not using the old deprecated -impredicative-set" mode). This is an example of 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).
show/hide this revision's text 2 add example with higher universes

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

The fact that Prop itself does not have type Prop is an example of unramified stratification (if Prop:Prop then the calculus would be unstratified, but also inconsistent).

Check Prop.
Prop
 : Type

However, note that (forall a:Prop, a):Prop as shown below:

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

The fact that (forall a:Set, a) does not have type Set is an example of ramified stratification (assuming you're not using the old deprecated -impredicative-set" mode).

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 stratification 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) *)

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).
show/hide this revision's text 1