Type theory
|
This article requires expansion. Please help.
Though not a stub by pure word count, this article lacks depth of content. |
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 led 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)[note 1][1][2], 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 [note 2][3]
Is the man who loves all men who do not love themselves self-hating? Self-loving?[4] 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.[note 3] If 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, and so on; a mixing of which is essential to Russell's paradox in its abstract form.[note 4] 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.[note 5] Sets that contain these objects have type 1.[note 6] 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 its own type.[note 7] 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 instead evolved with time. The above explanation is adapted from a simplification used by Kurt Gödel during the proof of the [note 8] 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]
Notes[edit]
- ↑ The idea of a universal language is one conception of language and logic: as a Universal Medium vs the conception of language and logic: as Calculi
- ↑ Technically Russell's Paradox is an antinomy: the paradox is neither veridical: a paradox whose conclusion is true despite its air of absurdity, nor is it falsidical: a paradox whose conclusion not only appears absurd but is also false, there being a fallacy in the proof. There is no way, presently, to becloud antinomies either by convincing us that there conclusion is true or by finding the fallacious step in the argument.
- ↑ 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 them.
- ↑ There is here, at least, the empty set.
- ↑ More indirect forms of self-reference are still possible and still have deep effects on mathematics.
- ↑ Gödel's incompleteness theorems
- ↑ Logic as Calculus and Logic as Language originally published in Synthese (1967): p.324-330. Van Heijenoort, Jean
- ↑ Calculus Ratiocinator vs Characteristica Universalis? The two traditions in Logic, Revisited, (1997). Hintikka, Jaacko
- ↑ (Secondary Source(Review of: Quine, New Foundations, and the Philosophy of Set Theory by Sean Morris)) published in the Journal for the History of Analytical Philosophy, Vol 8, No.9, page 4. Wagner, Henri (2020)
- ↑ This particular variation is taken from Jaakko Hintikka's "On Gödel."