Forms of types in the calculus of constructions

Question

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$.

Answer 1

On the face of it, the result you're asking for is a normalization result, as it asserts that every well-typed term of a certain form has a head-normal form (of a certain shape).

However it is legitimate to ask whether your statement is equivalent to normalization of the CC, since you are only asking for head normal forms of a certain sub-class of terms.

In general, it doesn't make sense to ask whether two true statements are equivalent, since the answer is always (trivially) yes. However in this specific case, normalization of CC must rely on powerful meta-theory, since it implies consistency of some strong form of higher-order logic! So it makes sense to ask:

In some weak meta-theory (say $\mathrm{PRA}$ or $\mathrm{PA}$) can we prove "CC is normalizing" $\Longleftrightarrow$ "Every closed term of type $*$ or $\square$ reduces to a product"?

The answer, I believe, is no.

Certainly, direction $\Longrightarrow$ holds, as you noted. But in the other direction, we have some counter-examples: in system $\mathrm{F_\omega}$, the fact that "type level" computations are normalizing is a consequence of the normalization of the simply-typed $\lambda$-calculus, and in Girard's system $U^-$, type level normalization holds, whereas it does not at the term level!

Things are a bit more complicated in the CC though, since type level terms can contain arbitrary term-level terms. The trick is that to compute head-normal forms, you don't actually need to dip into those terms to do reductions.

In PTS lingo, you only need to reduce $(*,\square, \square)$ and $(\square, \square, \square)$ redexes. But normalization of those only relies on the normalization of some variant of the simply typed $\lambda$-calculus (though I won't detail that argument right now). The hard part is showing that reducing the 2 types of redexes above must result in a head-normal form for terms of type $*$ or $\square$. You can do this by contradiction by supposing there is a head redex at that level, and showing that it must be of one of the two forms above.