Proof on normalization of CIC and its consistency


Can anyone give me a link to a proof of strongly or weakly normalization of Calculus of Inductive Constructions (CIC) and a proof of consistency strength of CIC?

I use the word “CIC” as the system presented in “Inductively defined types” by Coquand, Paulin in 1990.

Similar questions are at

According to them, Werner proved strong normalization of “λP2 + Inductive Types” in 1994. Altenkirch proved but did not cover general inductive types. Werner proved the upper bound of consistency strength of CIC is ZFC+ω inaccessible cardinals in 1997. Miquel proved the lower bound is Z + ω Zermelo universes.

Is there a proof on strongly or weakly normalization of Coquand’s CIC? Are there tighter bounds of its consistency strength?

Thanks for any hint.

1 Like

Have you already looked into Why is Coq consistent? What is the intended semantics? ?

No, I have not. Thank you.

But I couldn’t find a SN proof nor tighter bounds of consistency strength of CIC in your link.

I think that the question of tight consistency bounds for CIC is mostly open.

Somewhat relatedly, a few weeks ago, Alexandre Miquel presented tight bounds for weaker systems at CASS 2020 and I am fairly sure I had never seen those results before, let alone in written publications.

Consistency and normalisation of CIC are also treated by Bruno Barras with a lot of pointers to prior work.

We have elaborated on the “Sets in Coq” half mostly addressing the extensionality, choice-like assumptions, and height of Aczel’s model construction.