History of type theory
The type theory was initially created to avoid paradoxes in a variety of formal logics and rewrite systems. Later, type theory referred to a class of formal systems, some of which can serve as alternatives to naive set theory as a foundation for all mathematics.
It has been tied to formal mathematics since Principia Mathematica to today's proof assistants.
1900–1927
Origin of Russell's theory of types
In a letter to Gottlob Frege, Bertrand Russell announced his discovery of the paradox in Frege's Begriffsschrift. Frege promptly responded, acknowledging the problem and proposing a solution in a technical discussion of "levels". To quote Frege:Incidentally, it seems to me that the expression "a predicate is predicated of itself" is not exact. A predicate is as a rule a first-level function, and this function requires an object as argument and cannot have itself as argument. Therefore I would prefer to say "a concept is predicated of its own extension".
He goes about showing how this might work but seems to pull back from it. As a consequence of what has become known as Russell's paradox both Frege and Russell had to quickly amend works that they had at the printers. In an Appendix B that Russell tacked onto his The Principles of Mathematics one finds his "tentative" theory of types. The matter plagued Russell for about five years.
Willard Quine presents a historical synopsis of the origin of the theory of types and the "ramified" theory of types: after considering abandoning the theory of types, Russell proposed in turn three theories:
Quine observes that Russell's introduction of the notion of "apparent variable" had the following result:
the distinction between 'all' and 'any': 'all' is expressed by the bound variable of universal quantification, which ranges over a type, and 'any' is expressed by the free variable which refers schematically to any unspecified thing irrespective of type.
Quine dismisses this notion of "bound variable" as "pointless apart from a certain aspect of the theory of types".
The 1908 "ramified" theory of types
Quine explains the ramified theory as follows: "It has been so called because the type of a function depends both on the types of its arguments and on the types of the apparent variables contained in it, in case these exceed the types of the arguments". Stephen Kleene in his 1952 Introduction to Metamathematics describes the ramified theory of types this way:The axiom of reducibility and the notion of "matrix"
But because the stipulations of the ramified theory would prove "onerous", Russell in his 1908 Mathematical logic as based on the theory of types also would propose his axiom of reducibility. By 1910 Whitehead and Russell in their Principia Mathematica would further augment this axiom with the notion of a matrix — a fully extensional specification of a function. From its matrix a function could be derived by the process of "generalization" and vice versa, i.e. the two processes are reversible — generalization from a matrix to a function and the reverse process of reduction of type by courses-of-values substitution of arguments for the apparent variable. By this method impredicativity could be avoided.Truth tables
In 1921, Emil Post would develop a theory of "truth functions" and their truth tables, which replace the notion of apparent versus real variables. From his 1921 his "Introduction": "Whereas the complete theory requires for the enunciation of its propositions real and apparent variables, which represent both individuals and propositional functions of different kinds, and as a result necessitates the cumbersome theory of types, this subtheory uses only real variables, and these real variables represent but one kind of entity, which the authors have chosen to call elementary propositions".At about the same time Ludwig Wittgenstein developed similar ideas in his 1922 work Tractatus Logico-Philosophicus:
Wittgenstein proposed the truth-table method as well. In his 4.3 through 5.101, Wittgenstein adopts an unbounded Sheffer stroke as his fundamental logical entity and then lists all 16 functions of two variables.
The notion of matrix-as-truth-table appears as late as the 1940–1950s in the work of Tarski, e.g. his 1946 indexes "Matrix, see: Truth table"
Russell's doubts
Russell in his 1920 Introduction to Mathematical Philosophy devotes an entire chapter to "The axiom of Infinity and logical types" wherein he states his concerns: "Now the theory of types emphatically does not belong to the finished and certain part of our subject: much of this theory is still inchoate, confused, and obscure. But the need of some doctrine of types is less doubtful than the precise form the doctrine should take; and in connection with the axiom of infinity it is particularly easy to see the necessity of some such doctrine".Russell abandons the axiom of reducibility: In the second edition of Principia Mathematica he acknowledges Wittgenstein's argument. At the outset of his Introduction he declares "there can be no doubt... that there is no need of the distinction between real and apparent variables...". Now he fully embraces the matrix notion and declares "A function can only appear in a matrix through its values". Furthermore, he introduces a new notion of "matrix", that of a "logical matrix... one that contains no constants. Thus p|q is a logical matrix". Thus Russell has virtually abandoned the axiom of reducibility, but in his last paragraphs he states that from "our present primitive propositions" he cannot derive "Dedekindian relations and well-ordered relations" and observes that if there is a new axiom to replace the axiom of reducibility "it remains to be discovered".
Theory of simple types
In the 1920s, Leon Chwistek and Frank P. Ramsey noticed that, if one is willing to give up the vicious circle principle,the hierarchy of levels of types in the "ramified theory of types" can be collapsed.
The resulting restricted logic is called the theory of simple types or, perhaps more commonly, simple type theory. Detailed formulations of simple type theory were published in the late 1920s and early 1930s
by R. Carnap, F. Ramsey, W.V.O. Quine, and A. Tarski. In 1940 Alonzo Church formulated it as simply typed lambda calculus. and examined by Gödel in 1944. A survey of these developments is found in Collins.
1940s–present
Gödel 1944
in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote:He concluded the theory of simple types and axiomatic set theory, "permit the derivation of modern mathematics and at the same time avoid all known paradoxes" ; furthermore, the theory of simple types "is the system of the first Principia in an appropriate interpretation.... any symptoms show only too clearly, however, that the primitive concepts need further elucidation".
Curry–Howard correspondence, 1934–1969
The Curry–Howard correspondence is the interpretation of proofs-as-programs and formulae-as-types. The idea starting in 1934 with Haskell Curry and finalized in 1969 with William Alvin Howard. It connected the "computational component" of many type theories to the derivations in logics.Howard showed that the typed lambda calculus corresponded to intuitionistic natural deduction. The connection between types and logic lead to a lot of subsequent research to find new type theories for existing logics and new logics for existing type theories.
de Bruijn's AUTOMATH, 1967–2003
created the type theory Automath as a mathematical foundation for the Automath system, which could verify the correctness of proofs. The system developed and added features over time as type theory developed.Martin-Löf's Intuitionistic type theory, 1971–1984
found a type theory that corresponded to predicate logic by introducing dependent types, which became known as intuitionistic type theory or Martin-Löf type theory.Martin-Löf's theory uses inductive types to represent unbounded data structures, such as natural numbers.