Intuitionistic type theory

Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) 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. Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) 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. 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. An interesting 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 Aimplies B} ) corresponds to the type of a function ( A → B {displaystyle A o B} ). This correspondence is called the Curry–Howard isomorphism. Previous 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. Intuitionistic type theory has 3 finite types, which are then composed using 5 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. If you are unfamiliar with type theory and know set theory, a quick summary is: Types contain terms just like sets contain elements. Terms belong to one and only one type. Terms like 2 + 2 {displaystyle 2+2} and 2 ⋅ 2 {displaystyle 2cdot 2} compute ('reduce') down to canonical terms like 4. For more, see the article on Type theory. There are 3 finite types: The 0 type contains 0 terms. The 1 type contains 1 canonical term. And the 2 type contains 2 canonical terms. Because the 0 type contains 0 terms, it is also called the empty type. It is used to represent anything that cannot exist. It is also written ⊥ {displaystyle ot } 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 eg A:=A o ot } . Likewise, the 1 type contains 1 canonical term and represents existence. It also is called the unit type. It often represents propositions that can be proven and is, therefore, sometimes written ⊤ {displaystyle op } . Finally, the 2 type contains 2 canonical terms. It represents a definite choice between two values. It is used for Boolean values but not propositions. Propositions are considered the 1 type and may be proven to never have a proof (the 0 type), or may not be proven either way. (The Law of Excluded Middle does not hold for propositions in intuitionistic type theory.)