This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as Zermelo-Fraenkel set theory.
[4] Type theory is particularly popular in conjunction with Alonzo Church's lambda calculus.
Church's theory of types[5] helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus.
Church demonstrated[d] that it could serve as a foundation of mathematics and it was referred to as a higher-order logic.
One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics.
Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Coq, Lean, and other computer proof assistants.
This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS).
It has been used in natural language processing, principally computational semantics and dialogue systems.
[12][13] Gregory Bateson introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types.
A type theory is a mathematical logic, which is to say it is a collection of rules of inference that result in judgments.
may actually consist of complex terms and types that contain many function applications, not just single symbols.
One example of a rule that does not require any inputs is one that states the type of a constant term.
Formally, type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic.
It is possible to include the law of excluded middle and double negation into a type theory, by rule or assumption.
[citation needed] Per Martin-Löf proposed his intuitionistic type theory as a foundation for constructive mathematics.
Constructive mathematics does not allow the last step of removing the double negation to conclude that
[19] Most of the type theories proposed as foundations are constructive, and this includes most of the ones used by proof assistants.
[citation needed] It is possible to add non-constructive features to a type theory, by rule or assumption.
For a variety of logics, the rules are similar to expressions in a programming language's types.
Although the initial motivation for category theory was far removed from foundationalism, the two fields turned out to have deep connections.
A number of significant results follow in this way:[21] The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.
In addition to atomic terms, most modern type theories also allow for functions.
[17] The following lambda term represents a function which doubles an input natural number.
Type theories that allow for lambda terms also include inference rules known as
The second reduction makes explicit the relationship between lambda expressions and function types: if
This allows for greater specificity and type safety: functions with vector length restrictions or length matching requirements, such as the dot product, can encode this requirement as part of the type.
The logician Henk Barendegt introduced the lambda cube as a framework for studying various restrictions and levels of dependent typing.
This arises naturally in computer science where functions may return different types of outputs based on the input.
Many types of theories are strongly normalizing, which means that any order of applying the rules will always end in the same result.
When functions are considered "exponentiation", the combinations of types can be written similarly to algebraic identities.