EXTREME THEORY

---

The Two Roots of Typing - Thomas Forster

Tuesday - 20.11.2007

There are two radically different kinds of type distinction. Type theory (\'a la Russell and Whitehead) was devised as a way of avoiding the paradoxes. Type distinctions of the kind familiar to CS people have a completely different origin and purpose. Russell & Whitehead of course intended PM to be a basis for the whole of mathematics so their type distinction is (at least in principle) in play everywhere. Furthermore, those of us who think that mathematics is strongly typed will see CS-style type-distinctions everywhere. In principle, therefore, there is lots of scope for comparing the lessons taught us by the two kinds of typing (tho' not so much in practice it must be said). What is striking is how often the two approaches give the same answer. Is there perhaps an **Underlying Unity**?!?! I shall illustrate this with a discussion of the Burali-Forti paradox.