Russell and Whitehead's types: ramified and unramified - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-19T22:10:22Z http://mathoverflow.net/feeds/question/27793 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified Russell and Whitehead's types: ramified and unramified David Roberts 2010-06-11T07:03:29Z 2011-07-31T02:06:32Z <p>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? </p> <p>I know the intuitive description of RW's types as a hierarchy of sets, but nothing beyond that. </p> http://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified/27806#27806 Answer by Carl Mummert for Russell and Whitehead's types: ramified and unramified Carl Mummert 2010-06-11T11:20:14Z 2010-06-11T11:20:14Z <p>I was also going to point at the SEP article <a href="http://plato.stanford.edu/entries/type-theory" rel="nofollow">http://plato.stanford.edu/entries/type-theory</a> , which does a good job of explaining the differences. Unfortunately, while Russell and Whitehead had a great influence on logic, their actual work in Principia did not. The system they used in that book is mostly of historical interest, is not covered in any contemporary texts, and as far as I can see is not well known to contemporary mathematical logicians. </p> <p>Here's a one-paragraph summary answer, though. The things we usually call types will now be called "unramified types." Ramified type theory splits each unramified type into a whole sequence of types, so that the "ramified type" of an object depends not just on the unramified type but also on how that object is defined. </p> <p>The closest thing to this in modern logic is the stratification of sets into the cumulative hierarchy, where each set is assigned an ordinal number based on how many iterations of powerset are required to construct it from the empty set. But set theory is very different from type theory, so this is an analogy at best. </p> <p>A similar ramification issue was present in Paul Cohen's original presentation of forcing in set theory, which is now called ramified forcing ( <a href="http://en.wikipedia.org/wiki/Ramified_forcing" rel="nofollow">http://en.wikipedia.org/wiki/Ramified_forcing</a> ). However, this was quickly recast in unramified terms so that the ramified version is (again) of primarily historical interest. </p> http://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified/27880#27880 Answer by Adam for Russell and Whitehead's types: ramified and unramified Adam 2010-06-11T22:50:13Z 2010-06-13T23:47:17Z <p>Yes, this still occurs in modern type theory; in particular, you'll find it in the <a href="http://en.wikipedia.org/wiki/Calculus_of_constructions" rel="nofollow">calculus of constructions</a> employed by the <a href="http://www.lix.polytechnique.fr/coq/" rel="nofollow">Coq</a> language.</p> <p>Consider the type called <code>Prop</code>, whose inhabitants are logical propositions (which are in turn inhabited by proofs). The type <code>Prop</code> does not belong to <code>Prop</code> -- this means that <code>Prop</code> exhibits <strong>stratification</strong>:</p> <pre><code>Check Prop. Prop : Type </code></pre> <p>However, note that <code>(forall a:Prop, a)</code> <strong>does</strong> have type <code>Prop</code>. So although <code>Prop</code> does not belong to <code>Prop</code>, things which <em>quantify over all of <code>Prop</code></em> may still belong to <code>Prop</code>. So we can be more specific and say that <code>Prop</code> exhibits <strong>unramified stratification</strong>.</p> <pre><code>Check (forall a:Prop, a). forall a : Prop, a : Prop </code></pre> <p>By contrast, consider <code>Set</code>, whose inhabitants are datatypes (which are in turn inhabited by computations and the results of computations). <code>Set</code> does not belong to itself, so it too exhibits stratification:</p> <pre><code>Check Set. Set : Type </code></pre> <p>Unlike the previous example, things which <em>quantify over all of <code>Set</code></em> do not belong to <code>Set</code>. This means that <code>Set</code> exhibits <strong>ramified stratification</strong>.</p> <pre><code>Check (forall a:Set, a). forall a : Set, a : Type </code></pre> <p>So, in short, "ramification" in Russell's type hierarchy is embodied today by what Coq calls "predicative" types -- that is, all types except <code>Prop</code>. 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).</p> <p>The higher levels of the Coq universe (<code>Type</code>) are also ramified, but Coq hides the ramification indices from you unless you ask to see them:</p> <pre><code>Set Printing Universes. Check (forall a:Type, Type). Type (* Top.15 *) -&gt; Type (* Top.16 *) : Type (* max((Top.15)+1, (Top.16)+1) *) </code></pre> <p>Think of <code>Top.15</code> 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.</p> <p>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, <code>Prop</code>).</p> http://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified/27889#27889 Answer by Jacques Carette for Russell and Whitehead's types: ramified and unramified Jacques Carette 2010-06-12T00:18:00Z 2010-06-12T00:18:00Z <p>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 href="http://www.springer.com/mathematics/book/978-1-4020-2334-7" rel="nofollow">A modern perspective on type theory</a> by <a href="http://www.cedar-forest.org/fairouz/" rel="nofollow">Fairouz Kamereddine</a>, Twan Laan, and <a href="http://www.win.tue.nl/~wsinrpn/" rel="nofollow">Rob Nederpelt</a>. 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.</p> http://mathoverflow.net/questions/27793/russell-and-whiteheads-types-ramified-and-unramified/71698#71698 Answer by David Roberts for Russell and Whitehead's types: ramified and unramified David Roberts 2011-07-31T02:06:05Z 2011-07-31T02:06:05Z <p>Here is an interesting quote from Gödel about PM and ramified type theory therein that is of some relevance:</p> <blockquote> <p>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)</p> </blockquote> <p>I read this at <a href="http://www.cs.nyu.edu/pipermail/fom/2011-July/015668.html" rel="nofollow">http://www.cs.nyu.edu/pipermail/fom/2011-July/015668.html</a>, 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</p>