In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result:every closed term A such that $\Gamma \vdash A:\kappa$ (where $\kappa$ is a kind) reduces to a product, namely $A \rightsquigarrow^* \forall x^C.D$.The easy proof relies on the size of the longuest path from $A$ to its normal form, namely on strong normalization of CC (lexicographic induction on the length of the longuest path to normal form, and height of the derivation).In Benthem Jutting, Typing in Pure Type Systems, 1993, Information and computation there is the following result for all pure type systems:if $a \in T_S$ and $\Gamma \vdash a:A$ then $A \rightsquigarrow^* \forall x_1^{C_1}\ldots\forall x_n^{C_n}.s$ where $s$ is a sort and $T_S$ is almost the set of types.We can think prove first statement using the second: if $\Gamma \vdash A:\kappa$ then $\Gamma, x:A \vdash x:A$ and then $A$ reduces to a product. Unfortunately $T_S$ does not contain the variables.The question is: is there a proof of the first statement not relying on the strong normalization of CC ?My guess is that the answer is no: $A$ can $\beta$-reduces to an application, that can reduces to an application, ... The only way to know if it eventually reduces to a product is to effectively $\beta$-reduce it, and in the worst case to normalize $A$.
Forms of types in the calculus of constructions
lo.logic;type theory;type systems;calculus of constructions