History of type theory

Last updated May 15, 2024

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.

1900–1927

Origin of Russell's theory of types

In a letter to Gottlob Frege (1902), Bertrand Russell announced his discovery of the paradox in Frege's Begriffsschrift.^[1] 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 (subject). Therefore I would prefer to say "a concept is predicated of its own extension".^[2]

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 (1903) one finds his "tentative" theory of types. The matter plagued Russell for about five years.^[3]

Willard Quine ^[4] 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 (1905), Russell proposed in turn three theories:

the zigzag theory
theory of limitation of size,
the no-class theory (1905–1906) and then,
readopting the theory of types (1908ff)

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 ('apparent') variable of universal quantification, which ranges over a type, and 'any' is expressed by the free ('real') 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".^[5]

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 (or in its expression), in case these exceed the types of the arguments".^[5] Stephen Kleene in his 1952 Introduction to Metamathematics describes the ramified theory of types this way:

The primary objects or individuals (i.e. the given things not being subjected to logical analysis) are assigned to one type (say type 0), the properties of individuals to type 1, properties of properties of individuals to type 2, etc.; and no properties are admitted which do not fall into one of these logical types (e.g. this puts the properties 'predicable' and 'impredicable' ... outside the pale of logic). A more detailed account would describe the admitted types for other objects as relations and classes. Then to exclude impredicative definitions within a type, the types above type 0 are further separated into orders. Thus for type 1, properties defined without mentioning any totality belong to order 0, and properties defined using the totality of properties of a given order belong to the next higher order. ... But this separation into orders makes it impossible to construct the familiar analysis, which we saw above contains impredicative definitions. To escape this outcome, Russell postulated his axiom of reducibility , which asserts that to any property belonging to an order above the lowest, there is a coextensive property (i.e. one possessed by exactly the same objects) of order 0. If only definable properties are considered to exist, then the axiom means that to every impredicative definition within a given type there is an equivalent predicative one (Kleene 1952:44–45).

The axiom of reducibility and the notion of "matrix"

But because the stipulations of the ramified theory would prove (to quote Quine) "onerous", Russell in his 1908 Mathematical logic as based on the theory of types^[6] 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 — (i) generalization from a matrix to a function (by using apparent variables) and (ii) 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.^[7]

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 "Introduction" (1921): "Whereas the complete theory [of Whitehead and Russell (1910, 1912, 1913)] 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".^[8]

At about the same time Ludwig Wittgenstein developed similar ideas in his 1922 work Tractatus Logico-Philosophicus:

3.331 From this observation we get a further view – into Russell's Theory of Types. Russell's error is shown by the fact that in drawing up his symbolic rules he has to speak of the meanings of his signs.
3.332 No proposition can say anything about itself, because the propositional sign cannot be contained in itself (that is the whole "theory of types").
3.333 A function cannot be its own argument, because the functional sign already contains the prototype of its own argument and it cannot contain itself...

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 (5.101).

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"^[9]

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".^[10]

Russell abandons the axiom of reducibility: In the second edition of Principia Mathematica (1927) he acknowledges Wittgenstein's argument.^[11] 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...".^[12] Now he fully embraces the matrix notion and declares "A function can only appear in a matrix through its values" (but demurs in a footnote: "It takes the place (not quite adequately) of the axiom of reducibility"^[13]). Furthermore, he introduces a new (abbreviated, generalized) notion of "matrix", that of a "logical matrix . . . one that contains no constants. Thus p|q is a logical matrix".^[14] Thus Russell has virtually abandoned the axiom of reducibility,^[15] 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".^[16]

Theory of simple types

In the 1920s, Leon Chwistek ^[17] and Frank P. Ramsey ^[18] 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^[19] or, perhaps more commonly, simple type theory.^[20] 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 (re)formulated it as simply typed lambda calculus.^[21] and examined by Gödel in 1944. A survey of these developments is found in Collins (2012).^[22]

1940s–present

Gödel 1944

Kurt Gödel in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote:

By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: " a has the property φ ", " b bears the relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399).".^[23]

He concluded the (1) theory of simple types and (2) axiomatic set theory, "permit the derivation of modern mathematics and at the same time avoid all known paradoxes" (Gödel 1944:126); furthermore, the theory of simple types "is the system of the first Principia [Principia Mathematica] in an appropriate interpretation. . . . [M]any symptoms show only too clearly, however, that the primitive concepts need further elucidation" (Gödel 1944:126).

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 (that is, natural deduction without the Law of excluded middle). 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

Nicolaas Govert de Bruijn 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

Per Martin-Löf 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.

Martin-Löf's presentation of his theory using rules of inference and judgments becomes the standard for presenting future theories.

Coquand and Huet's Calculus of Constructions, 1986

Thierry Coquand and Gérard Huet created the Calculus of Constructions,^[24] a dependent type theory for functions. With inductive types, it would be called "the Calculus of Inductive Constructions" and become the basis for Coq and Lean.

Barendregt's lambda cube, 1991

The lambda cube was not a new type theory but a categorization of existing type theories. The eight corners of the cube included some existing theories with simply typed lambda calculus at the lowest corner and the calculus of constructions at the highest.

Identity Proofs are Not Unique, 1994

Prior to 1994, many type theorists thought all terms of the same identity type were the same. That is, that everything was reflexivity. But Martin Hofmann and Thomas Streicher showed that that was not required by the rules of the identity type. In their paper, "The Groupoid Model Refutes Uniqueness of Identity Proofs",^[25] they showed that equality terms could be modeled as a group where the zero element was "reflexitivity", addition was "transitivity" and negation was "symmetry".

This opened up a new area of research, homotopy type theory, where category theory was applied to the identity type.

Related Research Articles

In logic, the law of excluded middle or the principle of excluded middle states that for every proposition, either this proposition or its negation is true. It is one of the three laws of thought, along with the law of noncontradiction, and the law of identity; however, no system of logic is built on just these laws, and none of these laws provides inference rules, such as modus ponens or De Morgan's laws. The law is also known as the law / principleof the excluded third, in Latin principium tertii exclusi. Another Latin designation for this law is tertium non datur or "no third [possibility] is given". In classical logic, the law is a tautology.

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

The Principia Mathematica is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. In 1925–1927, it appeared in a second edition with an important Introduction to the Second Edition, an Appendix A that replaced ✱9 and all-new Appendix B and Appendix C. PM was conceived as a sequel to Russell's 1903 The Principles of Mathematics, but as PM states, this became an unworkable suggestion for practical and philosophical reasons: "The present work was originally intended by us to be comprised in a second volume of Principles of Mathematics... But as we advanced, it became increasingly evident that the subject is a very much larger one than we had supposed; moreover on many fundamental questions which had been left obscure and doubtful in the former work, we have now arrived at what we believe to be satisfactory solutions."

In mathematical logic, Russell's paradox is a set-theoretic paradox published by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains an unrestricted comprehension principle leads to contradictions. The paradox had already been discovered independently in 1899 by the German mathematician Ernst Zermelo. However, Zermelo did not publish the idea, which remained known only to David Hilbert, Edmund Husserl, and other academics at the University of Göttingen. At the end of the 1890s, Georg Cantor – considered the founder of modern set theory – had already realized that his theory would lead to a contradiction, as he told Hilbert and Richard Dedekind by letter.

Friedrich Ludwig Gottlob Frege was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic philosophy, concentrating on the philosophy of language, logic, and mathematics. Though he was largely ignored during his lifetime, Giuseppe Peano (1858–1932), Bertrand Russell (1872–1970), and, to some extent, Ludwig Wittgenstein (1889–1951) introduced his work to later generations of philosophers. Frege is widely considered to be the greatest logician since Aristotle, and one of the most profound philosophers of mathematics ever.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

The history of logic deals with the study of the development of the science of valid inference (logic). Formal logics developed in ancient times in India, China, and Greece. Greek methods, particularly Aristotelian logic as found in the Organon, found wide application and acceptance in Western science and mathematics for millennia. The Stoics, especially Chrysippus, began the development of predicate logic.

In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model, i.e., there exists an interpretation under which all formulas in the theory are true. This is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states a theory $is consistent if there is no formula such that both and its negation are elements of the set of consequences of . Let be a set of closed sentences and the set of closed sentences provable from under some formal deductive system. The set of axioms is consistent when there is no formula such that and .$

Metamathematics is the study of mathematics itself using mathematical methods. This study produces metatheories, which are mathematical theories about other mathematical theories. Emphasis on metamathematics owes itself to David Hilbert's attempt to secure the foundations of mathematics in the early part of the 20th century. Metamathematics provides "a rigorous mathematical technique for investigating a great variety of foundation problems for mathematics and logic". An important feature of metamathematics is its emphasis on differentiating between reasoning from inside a system and from outside a system. An informal illustration of this is categorizing the proposition "2+2=4" as belonging to mathematics while categorizing the proposition "'2+2=4' is valid" as belonging to metamathematics.

In the philosophy of mathematics, logicism is a programme comprising one or more of the theses that – for some coherent meaning of 'logic' – mathematics is an extension of logic, some or all of mathematics is reducible to logic, or some or all of mathematics may be modelled in logic. Bertrand Russell and Alfred North Whitehead championed this programme, initiated by Gottlob Frege and subsequently developed by Richard Dedekind and Giuseppe Peano.

Begriffsschrift is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book.

The laws of thought are fundamental axiomatic rules upon which rational discourse itself is often considered to be based. The formulation and clarification of such rules have a long tradition in the history of philosophy and logic. Generally they are taken as laws that guide and underlie everyone's thinking, thoughts, expressions, discussions, etc. However, such classical ideas are often questioned or rejected in more recent developments, such as intuitionistic logic, dialetheism and fuzzy logic.

"Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I" is a paper in mathematical logic by Kurt Gödel. Submitted November 17, 1930, it was originally published in German in the 1931 volume of Monatshefte für Mathematik und Physik. Several English translations have appeared in print, and the paper has been included in two collections of classic mathematical logic papers. The paper contains Gödel's incompleteness theorems, now fundamental results in logic that have many implications for consistency proofs in mathematics. The paper is also known for introducing new techniques that Gödel invented to prove the incompleteness theorems.

In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value. A propositional formula may also be called a propositional expression, a sentence, or a sentential formula.

In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes the set being defined, or another set that contains the thing being defined. There is no generally accepted precise definition of what it means to be predicative or impredicative. Authors have given different but related definitions.

Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.

In mathematical logic, algebraic logic is the reasoning obtained by manipulating equations with free variables.

The axiom of reducibility was introduced by Bertrand Russell in the early 20th century as part of his ramified theory of types. Russell devised and introduced the axiom in an attempt to manage the contradictions he had discovered in his analysis of set theory.

The mathematical concept of a function dates from the 17th century in connection with the development of the calculus; for example, the slope $of a graph at a point was regarded as a function of the x -coordinate of the point. Functions were not explicitly considered in antiquity, but some precursors of the concept can perhaps be seen in the work of medieval philosophers and mathematicians such as Oresme.$

References

↑ Russell's (1902) Letter to Frege appears, with commentary, in van Heijenoort 1967:124–125.
↑ Frege (1902) Letter to Russell appears, with commentary, in van Heijenoort 1967:126–128.
↑ cf. Quine's commentary before Russell (1908) Mathematical Logic as based on the theory of types in van Heijenoort 1967:150
↑ cf. commentary by W. V. O. Quine before Russell's (1908) Mathematical logic as based on the theory of types in van Hiejenoort 1967:150–153
1 2 Quine's commentary before Russell (1908) Mathematical logic as based on the theory of types in van Heijenoort 1967:151
↑ Russell (1908) Mathematical Logic as based on the theory of types in van Heijenoort 1967:153–182
↑ cf. in particular p. 51 in Chapter II The theory of Logical Types and *12 The Hierarchy of Types and the Axiom of Reducibility pp. 162–167. Whitehead and Russell (1910–1913, 1927 2nd edition) Principia Mathematica
↑ Post (1921) Introduction to a general theory of elementary propositions in van Heijenoort 1967:264–283
↑ Tarski 1946, Introduction to Logic and to the Methodology of Deductive Sciences, Dover republication 1995
↑ Russell 1920:135
↑ cf. "Introduction" to 2nd edition, Russell 1927:xiv and Appendix C
↑ cf. "Introduction" to 2nd edition, Russell 1927:i
↑ cf. "Introduction" to 2nd edition, Russell 1927:xxix
↑ The vertical bar " | " is the Sheffer stroke; cf. "Introduction" to 2nd edition, Russell 1927:xxxi
↑ "The theory of classes is at once simplified in one direction and complicated in another by the assumption that functions only occur through their values and by the abandonment of the axiom of reducibility"; cf. "Introduction" to 2nd edition, Russell 1927:xxxix
↑ These quotes from "Introduction" to 2nd edition, Russell 1927:xliv–xlv.
↑ L. Chwistek, Antynomje logikiformalnej, Przeglad Filozoficzny 24 (1921) 164–171
↑ F. P. Ramsey, The foundations of mathematics, Proceedings of the London Mathematical Society, Series 2 25 (1926) 338–384.
↑ Gödel 1944, pages 126 and 136–138, footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938–1974, Oxford University Press, New York NY, ISBN 978-0-19-514721-6(v.2.pbk).
↑ This does not mean the theory is "simple", it means that the theory is restricted: types of different orders are not to be mixed: "Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded." Gödel 1944, pages 127, footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938–1974, Oxford University Press, New York NY, ISBN 978-0-19-514721-6(v.2.pbk).
↑ A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic 5 (1940) 56–68.
↑ J. Collins, A History of the Theory of Types: Developments after the Second Edition of 'Principia Mathematica'. LAP Lambert Academic Publishing (2012). ISBN 978-3-8473-2963-3, esp. chs. 4–6.
↑ Gödel 1944:126 footnote 17: "Russell's mathematical logic" appearing in Kurt Gödel: Collected Works: Volume II Publications 1938–1974, Oxford University Press, New York NY, ISBN 978-0-19-514721-6(v.2.pbk).
↑ Coqquand, Thierry; Huet, Gerard. "The Calculus of Constructions" (PDF). INRIA.
↑ Hofmann, Martin; Streicher, Thomas (July 1994). "The groupoid model refutes uniqueness of identity proofs". Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science. pp. 208–212. doi:10.1109/LICS.1994.316071. ISBN 0-8186-6310-3. S2CID 19496198.

Sources

Bertrand Russell (1903), The Principles of Mathematics: Vol. 1, Cambridge at the University Press, Cambridge, UK.
Bertrand Russell (1920), Introduction to Mathematical Philosophy (second edition), Dover Publishing Inc., New York NY, ISBN 0-486-27724-0 (in particular chapters XIII and XVII).
Alfred Tarski (1946), Introduction to Logic and to the Methodology of Deductive Sciences, republished 1995 by Dover Publications, Inc., New York, NY ISBN 0-486-28462-X
Jean van Heijenoort (1967, 3rd printing 1976), From Frege to Godel: A Source Book in Mathematical Logic, 1879–1931, Harvard University Press, Cambridge, MA, ISBN 0-674-32449-8 (pbk)
- Bertrand Russell (1902), Letter to Frege with commentary by van Heijenoort, pages 124–125. Wherein Russell announces his discovery of a "paradox" in Frege's work.
- Gottlob Frege (1902), Letter to Russell with commentary by van Heijenoort, pages 126–128.
- Bertrand Russell (1908), Mathematical logic as based on the theory of types, with commentary by Willard Quine, pages 150–182.
- Emil Post (1921), Introduction to a general theory of elementary propositions, with commentary by van Heijenoort, pages 264–283.
Alfred North Whitehead and Bertrand Russell (1910–1913, 1927 2nd edition reprinted 1962), Principia Mathematica to *56, Cambridge at the University Press, London UK, no ISBN or US card catalog number.
Ludwig Wittgenstein (republished 2009), Major Works: Selected Philosophical Writings, HarperCollins, New York. ISBN 978-0-06-155024-9. Wittgenstein's (1921 in English), Tractatus Logico-Philosophicus, pages 1–82.