User:CTrombley/Draft of Type Theory
Type theory (presumably, as opposed to type practice) is a part of metamathematics that distinguishes an object and the set to which it belongs, in a formal way. Type theory was first developed by Bertrand Russell as his solution to a foundational crisis in mathematics that he started.
Motivation in Detail[edit]
In 1874, Georg Cantor proved that the cardinality of a power set is always greater than that of the original set. In other words, you can always make a set bigger than any set you care to name even if that set is infinite. This lead to the creation of modern set theory, and many mathematicians were worried that the freedom created by this new theory would lead to contradictions. In order to lay this worry to rest (and in the service of a pedantic Kantian-Leibnizian idea of a universal language), Gottlob Frege formalized the theory in 1879 and more extensively in 1884. In spite of Frege's accomplishments, a devastating blow was dealt to the formalization by Bertrand Russell's self-reference paradoxes.
Is the man who loves all men who do not love themselves self-hating? Self-loving?[1] Though the great skeptic Russell never brought it up, the old theological question of whether God can lift a stone so heavy he can't lift it is another variation on Russell's paradox.
To put it into a form more directly useful for skepticism, consider if God (or any omnipotent being) can create something so wonderful that He cannot create it.[2] If not he cannot he is not omnipotent (by definition), and if he can then there is something he cannot create and He is not omnipotent. Unlike omnipotence, mathematics can be rescued from paradox by many tactics.
Already in Frege's work there is a distinction between objects, predicates and predicates of predicates, etc a mixing of which is essential to Russell's paradox in it's abstract form[3]. If Frege had been more pedantic in this distinction, as he was in the distinction between sense and reference, then perhaps we never would have found these paradoxes. As it stands, Russell had to create type theory in order to separate the wheat from the chaff and strengthen the foundation of mathematics.
How Does Type Theory Deal With The Paradox?[edit]
By definition, the primitive objects have type 0. [4] Sets that contain these objects have type 1.[5] Sets that contain sets of type 1 have type 2. Ordered pairs, for instance, are of this type. Sets that contain objects of type 2 have type 3. And so on and so on, as far beyond the small infinities as we can take. Thus one cannot ask about a set that contains itself, for this set would have to be higher than it's own type.[6] There is no person who loves everyone who doesn't love themselves and no being that can do everything that it cannot do.
Other Uses[edit]
Like all real science, type theory did not burst from the head of one man fully grown, but has evolved with time. The above explanation is adapted from a simplification used by Gödel during the proof of the incompleteness theorems, and was improved by Alonzo Church while working on the Decision Problem. Per Martin-Löf began the exploration of type theories in non-classical logics, and both his and Church's work are important in the theory of functional programming.
See Also[edit]
Footnotes[edit]
- ↑ This particular variation is taken from Hintika's "On Gödel."
- ↑ Creation is not special and virtually anything can be substituted for it.
- ↑ Or at least the abstract form in Frege's formalization.
- ↑ It is not necessary that there are any such objects for there to be a type for it.
- ↑ There is here, at least, the empty set.
- ↑ More indirect forms of self-reference are still possible and still have deep effects on mathematics.