Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory (MLTT)) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.
Design Martin-Löf designed the type theory on the principles of mathematical constructivism. Constructivism requires any existence proof to contain a "witness". So, any proof of "there exists a prime greater than 1000" must identify a specific number that is both prime and greater than 1000. Intuitionistic type theory accomplished this design goal by internalizing the BHK interpretation. A useful consequence is that proofs become mathematical objects that can be examined, compared, and manipulated. Intuitionistic type theory's type constructors were built to follow a one-to-one correspondence with logical connectives. For example, the logical connective called implication ( A ⟹ B {\displaystyle A\implies B} ) corresponds to the type of a function ( A → B {\displaystyle A\to B} ). This correspondence is called the Curry–Howard isomorphism. Prior type theories had also followed this isomorphism, but Martin-Löf's was the first to extend it to predicate logic by introducing dependent types.
Type theory
A type theory is a kind of mathematical ontology, or foundation, describing the fundamental objects that exist. In the standard foundation, set theory combined with mathematical logic, the fundamental object is the set, which is a container that contains elements. In type theory, the fundamental object is the term, each of which belongs to one and only one type. Intuitionistic type theory has three finite types, which are then composed using five different type constructors. Unlike set theories, type theories are not built on top of a logic like Frege's. So, each feature of the type theory does double duty as a feature of both math and logic.
0 type, 1 type and 2 type There are three finite types: The 0 type contains no terms. The 1 type contains one canonical term. The 2 type contains two canonical terms. Because the 0 type contains no terms, it is also called the empty type. It is used to represent anything that cannot exist. It is also written ⊥ {\displaystyle \bot } and represents anything unprovable (that is, a proof of it cannot exist). As a result, negation is defined as a function to it: ¬ A := A → ⊥ {\displaystyle \neg A:=A\to \bot } . Likewise, the 1 type contains one canonical term and represents existence. It also is called the unit type. Finally, the 2 type contains two canonical terms. It represents a definite choice between two values. It is used for Boolean values but not propositions. Propositions are instead represented by particular types. For instance, a true proposition can be represented by the 1 type, while a false proposition can be represented by the 0 type. But we cannot assert that these are the only propositions, i.e. the law of excluded middle does not hold for propositions in intuitionistic type theory.
Σ type constructor Σ-types contain ordered pairs. As with typical ordered pair (or 2-tuple) types, a Σ-type can describe the Cartesian product, A × B {\displaystyle A\times B} , of two other types, A {\displaystyle A} and B {\displaystyle B} . Logically, such an ordered pair would hold a proof of A {\displaystyle A} and a proof of B {\displaystyle B} , so one may see such a type written as A ∧ B {\displaystyle A\wedge B} . Σ-types are more powerful than typical ordered pair types because of dependent typing. In the ordered pair, the type of the second term can depend on the value of the first term. For example, the first term of the pair might be a natural number and the second term's type might be a sequence of reals of length equal to the first term. Such a type would be written:
∑ n : N Vec ( R , n ) {\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}
Using set-theory terminology, this is similar to an indexed disjoint union of sets. In the case of the usual cartesian product, the type of the second term does not depend on the value of the first term. Thus the type describing the cartesian product N × R {\displaystyle {\mathbb {N} }\times {\mathbb {R} }} is written:
∑ n : N R {\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }}
… excerpt ends here. Continue reading the full article.
