今日は \( \mathrm{CoC} \) と \( \mathrm{pCIC} \) の無矛盾性の強さについて情報を書いておきます。
\( \mathrm{CoC} \) の無矛盾性の強さはどうでしょうか。
2010年12月に Chris Casinghino により Strong Normalization for the Calculus of Constructions という論文が出ています。これは \( \mathrm{CoC} \) の強正規化性の証明を三つ紹介しています。
このように \( \mathrm{CoC} \) の強正規化性は証明されていています。それは \( \mathrm{CoC} \) の無矛盾性を導きます。証明は普通の集合論で行われているように見えるので \( \mathrm{ZFC} \vdash \mathrm{Con} ( \mathrm{CoC} ) \) だということだと思います。ならば、下側から無矛盾性の強さを測る文献を探したのですが全く見つけられませんでした。ただし、特筆すべきこととして CoC は System Fω と無矛盾性が等しいです。
\( \mathrm{CIC} \) の無矛盾性の強さはどうでしょうか。
https://mathoverflow.net/questions/69229/proof-strength-of-calculus-of-inductive-constructions の Neel Krishnaswami による答えは \( \mathrm{CIC} \) が \( \mathrm{ZFC} + \textrm{“There are countably many inaccessible cardinals”} \) と equi-interpretable だとしています。
https://coq.discourse.group/t/proof-on-normalization-of-cic-and-its-consistency/444 には \( \mathrm{CIC} \) の無矛盾性の強さは \( \mathrm{ZFC} + \textrm{“There are countably many inaccessible cardinals”} \) が上限であると書いてあります。これは
どちらも Sets in Types, Types in Sets を根拠としているようですが、この状況はいささか不気味です。後者が正しいのであれば私は誤った情報を広げていたことになるので、がっくりします。
一応、公式のウィキの記述には "The theory of Coq version 8.9 is generally admitted to be consistent wrt Zermelo-Fraenkel set theory + inaccessible cardinals. Proofs of consistency of subsystems of the theory of Coq can be found in the literature." とあるようですが……。
なお、 \( \mathrm{CIC} \) と \( \mathrm{pCIC} \) は厳密には違いますが、その違いは Set という本質ではない特殊な用途に設けられたソートが predicative になっているかどうかだけであり、重要なソートである Type における違いは存在しないので無矛盾性の強さは同じだと思われます。
余談[]
ローダー数は超越整数との比較が知られていないそうです。ですが、少なくとも CoC の無矛盾性の強さは ZFC よりも小さいのでローダー数よりも超越整数の方が大きそうです。私が定義をきちんと理解していないので、確実なことは言えないのですが。