# simple-type-theory section : math subsection : Type Theory title : Simple Type Theory filename : simple-type-theory.md parent : 90-type-theory path : 90-type-theory/simple-type-theory.md link : [Simple Type Theory](https://github.com/mandober/debrief.math/tree/22d3b35bdafab8f414b8c4da51d1fb13b55aa733/350-type-theory/terms/90-type-theory/simple-type-theory.md) ## 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 This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com. ## 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-theories/simple-type-theory.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.