# History of Type Theory > The fundamental idea behind type theory is the ability to distinguish between different types of objects. Before the introduction of formalization to math and logic in the end of XIX, the types were present in mathematics and logic but implicit, given only informally or taken for granted, since no formal representations of types existed. Discovery of new paradoxes inspired the development of type theory, especially the paradox that Bernard Russell found in relation to Cantor's set theory, in Frege's *Begriffsschrift*, which became known as the Russell's paradox. Although paradoxes have always existed, the importance of Russell's paradox is that it was applicable to many theories that were forming at the time, like Cantor's, Frege's and Peano's formal systems. Being at the very basis of logic, Russell's paradox couldn't be disregarded and a solution had to be found. ## Ramified Type Theory Russell introduced types, in 1908 edition of his and Whitehead's *Principia Metematica*, in hope of avoiding paradoxes, especially the Russell paradox that occurs in face of impredicativity. Something that is **impredicative** contains reserences to itself, it is a self-referencing definition. Roughly speaking, a definition is impredicative if it mentions (or quantifies over) the set being defined, or, more commonly, another set that contains the thing being defined. Russell's paradox is an example of an impredicative construction - namely the set of all sets that do not contain themselves. The paradox is that such a set cannot exist, because if it did, the question becomes whether it contains itself or not: if it does, then by definition it should not, and if it doesn't, then by definition it should. On the other hand, **predicativity** entails building **stratified** (or ramified) theories with quantification over lower levels of entities that results in variables of some new type, distinguished from the lower types that the variable ranges over. An example is intuitionistic type theory, which retains stratification (ramification) in order to avoid impredicativity. Therefore, Russell's plan was to avoid impredicativity by applying the vicious circle principle: "*Whatever involves all of a collection must not be one of the collection*". Types in **Ramified Type Theory** (RTT) of *Principia* have a double hierarchy: one of simple types and one of orders. The notion of a general set was replaced with the hierarchy of sets of different types - a set of a certain type is only allowed to contain sets of strictly lower types. The primary objects are assigned to type 0, the properties of individuals to type 1, properties of properties of individuals to type 2, and so on, and no properties which do not fall into one of these logical types are allowed. In *Principia*, Whitehead and Russell attempted to found mathematics on logic, the approach that is known as **logicism**. The result was a very formal and accurate build-up of mathematics, avoiding the logical paradoxes, however, the description of RTT, though extensive, was still informal. ## Simple type theory In 1920s, Chwistek and Ramsey noticed that, if one is willing to give up the vicious circle principle, the hierarchy of levels of types in the RTT can be collapsed. The **vicious circle principle** states that no object or property may be introduced by a definition that depends on that object or property itself. This resulted in the theory of simple types, commonly called, simple type theory (STT). In 1940 Alonzo Church reformulated it as **simply typed lambda calculus**. The adjective "simple" in STT doesn't mean the theory is simple, but restricted: types of different orders are not allowed to mix. Mixed types, such as classes containing individuals and classes as elements, and also transfinite types, such as the class of all classes of finite types, are excluded. In 1944, in his book *Russell's mathematical logic*, Kurt Gödel mentioned the STT writing that it does avoid all known paradoxes thus enabling the derivation of all mathematics, but that it needs further development and elucidation. *** in 1967, de Bruijn created the **Automath type theory** as a mathematical foundation for the Automath system which could verify the correctness of proofs. It allowed expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. The system developed and added features over time as type theory developed. In 1972, Per Martin-Löf founded a type theory that corresponded to predicate logic by introducing dependent types, which became known as **intuitionistic type theory** (ITT) or **Martin-Löf type theory** (MTT). One of its key features is that it unifies set theory and logic. In 1991, Barendregt introduced the **lambda cube**, which wasn't a 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. In 2006, Awodey and Warren, and Voevodsky, discovered that intuitionistic type theory has homotopical models which led to the development of **category type theory**. --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://mandober.gitbook.io/math-debrief/350-type-theory/type-theory-general/type-theory-history.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.