Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)

Question

There are some proofs around to prove the strong normalization of the calculus of constructions (i.e. that all type systems in the lambda cube are strongly normalizing). I have analyzed the proof available from Herman Geuvers which is not an easy read, but understandable.

I am interested in proof of strong normalization of calculi like CC which have cumulative universes i.e. which have sorts $$ \text{sort} ::= * \mid \Box_i \quad 0 \le i, $$ allow subtyping $$ \begin{array}{c} \Gamma \vdash t : T \\ T \le U \\ \hline \Gamma \vdash t : U \end{array} $$ where $\le$ is based on the ordering of sorts $$ * < \Box_0 < \Box_1 \ldots$$

and the typing rules are practically the same as for pure type systems where $*$ is impredicative and all $\Box_i$ are predicative.

A simple generalization of the proof of Herman Geuvers does not work because it heavily depends on a distinction between kinds and types and objects and type constructors (based on having only two sorts $*$ and $\Box$ and no cumulativity).

I have searched a lot but I cannot find a comprehensible proof of strong normalization. This is strange because this type system is a subset of the type system of Coq which is in use for several decades now and supposedly strongly normalizing.

Can anybody give hints to understandable proofs of such type systems?

Thanks for any hint.

Addendum:

From the first comment of Cody I conclude that there might be no easier to grasp proofs than the proof in Zhaohui Luo's Phd thesis which I already have but it is a big bullet to bite.

I don't need the full power of cumulative universes, but the calculus of constructions is not sufficient for me, because I have to make a Coq like split between propositions and "normal" types. Is there a way to generalize the proof of strong normalization of CoC to such a type system?

Furthermore a proof of strong normalization would be nice, but a proof of weak normalization would be sufficient at least to make type checking decidable. Is there a simpler proof for weak normalization for systems with cumulative universes?. But, of course, this does not prove that the system is sound (i.e. free of contradictions) which is a major drawback.

Answer 1

I guess this is just an extension of my comment, but I've heard Luo cite Goguen's paper The metatheory of UTT which uses typed operational semantics. I'm afraid I can't find a free online version though, and typed operational semantics doesn't exactly take all the sting from the technical hassles.

A completely different, and IMO under-appreciated paper is Sacchini & Gregoire's On Strong Normalization of the Calculus of Constructions with Type-Based Termination, which treats a system with Prop + 1 universe and natural numbers. Already a feat!

Addressing your other concerns: Weak normalization does imply consistency! I don't think it's significantly easier to prove than strong normalization, though, so usually people will go for gold and try to prove SN directly. It's a well-known conjecture that weak normalization implies strong normalization in "reasonable" theories anyways.

If you're only interested in consistency, you might try building a model of your theory directly! This seems to be quite a bit easier than normalization, and might be seen as a stepping stone if you're going to try to build a proof yourself. One reference I enjoy is Werner and Lee Proof-irrelevant model of CC with predicative induction and judgmental equality . I think this easily generalizes to cumulative universes. And if you think their construction is technical, imagine the full normalization proof!