Handbook of Automated Reasoning

3 Type systems for proof checking

As we see it, there is not one ‘right’ type system. The widely used theorem provers that are based on type theory all have inductive types. But then still there are other important parameters: the choice of allowed quantification and the choice of reduction relations to be used in the type conversion rule. We have already mentioned the possibility of allowing impredicative quantification or not. Also, we mentioned the β, δ, ι and η rules as possible reduction rules. A very powerful extension of the reduction relation is obtained by adding a fixed-point-operator Y:Π. A:Set.(A→A)→A satisfying

$\text{Yƒ}{\to }_{\text{Y}}\text{ƒ}\left(\text{Yƒ}\right).$

With this addition the reduction of the type system does not satisfy strong normalization ...