Type Checking Undecidable in Extensional Type Theory

Question

What is the difference between intensional vs extensional type theories and how come the type checking is undecidable for extensional type theory? Also, how does it affect the expressiveness of theorem provers?

Answer 1

Extensional type theory is characterized by the reflection rule, which says that if the identity type ${\rm Id}(a,b)$ is inhabited, then $a\equiv b$ ($a$ and $b$ are judgmentally equal). It is called extensional type theory because this means that the judgmental equality coincides with the identity type, and the latter is extensional (or, at least, more extensional than the judgmental equality would be in the absence of the reflection rule --- just how extensional it is depends on whether you have principles like function extensionality and univalence). Intensional type theory is so-called because its judgmental equality is intensional, whereas its identity types can be even more extensional than those in extensional type theory (because the reflection rule is incompatible with the "strongest extensionality principle", namely univalence).

In a dependent type theory, type-checking is complicated because of the conversion rule that if $a:A$ and $A\equiv B$ then $a:B$. This essentially requires that a type-checking algorithm must include an algorithm for checking judgmental equality. When combined with the reflection rule, this means a type-checking algorithm would have to include an algorithm for checking inhabitation of a type (namely the identity type). But inhabitation of types can be used to encode the truth of arbitrary mathematical statements, so (e.g. by the halting problem) it is impossible to have a terminating algorithm for checking inhabitation of types, and hence impossible to have a terminating type-checking algorithm for extensional type theory.

There is a theorem, due I believe to Martin Hofmann (Conservativity of Equality Reflection over Intensional Type Theory), that extensional type theory is conservative over intensional type theory extended by axioms of uniqueness-of-identity-proofs and function extensionality. Thus, there is no difference in the "expressiveness" of these theories. Given the undecidability of type-checking for extensional type theory, therefore, very few proof assistants have tried to implement it.