https://github.com/coq/coq/wiki/Presentation claims that Coq version 8.9 is generally admitted to be consistent wrt Zermelo-Fraenkel set theory + inaccessible cardinals. And a report by Lee and Werner in https://arxiv.org/abs/1111.0123 shows that ZF + infinite inaccessible cardinals implies consistency of CC with predicative induction, which can be regarded as an introduction to the base theory of the proof assistant Coq.
However, at the Model Construction section in https://github.com/coq/coq/wiki/TheoryBehindCoq, there is a report by Sozeau and Timany https://arxiv.org/abs/1710.03912. According to this report, the proof by Lee and Werner is unsuitable because it assumes the normalization property which already implies soundness of their system. And using axiom of choice can avoid this assumption.
I doubt the truth of Sozeau and Timany’s report because I couldn’t find such an assumption in Lee and Werner’s one. I want to know whether Lee and Werner assumed normalization property and whether consistency of Coq or its base theory was proven with ZF + inaccessible cardinals without axiom of choice.
Having taken a quick look, I think I understand in part the concern by Sozeau and Timany, but I’m not fully convinced; indeed, as it is normal, neither proof fully covers Coq termination checking.
And according to them, the use of choice is unrelated to this point: they avoid the issue with Lee and Werner by proving consistency of a different system.
Sozeau and Timany assumes that source programs are written using eliminators (that is, recursion is expressed by calling functions similar to Coq’s generated induction principles). However, Coq programs are written using recursive functions — as they point out, Coq programs need to be translated to use eliminators.
Lee and Werner assume they can perform termination checking by inspecting bodies of recursive functions. However, their rules are not applicable to Coq as-is: Coq normalizes function bodies before performing termination checking. If it didn’t, many Coq programs would be rejected and would have to be modified. Lee and Werner do not discuss this normalization step, and Sozeau and Timany appear to consider it unavoidable — and they demand proof that it terminates.
However, that seems debatable for various reasons.
Other termination checkers, like Agda’s, do not normalize functions before termination checking (however, this choice is a real problem in some cases, even tho Agda’s termination checker is more flexible in other ways).
If one relies on Lee and Werner and has the typechecker normalize functions before termination checking and strong normalization fails, the worst case seems a loop during typechecking, which does not endanger consistency. At worst, the user will interrupt typechecking and modify the program — which is often necessary anyway when using Coq.
Last, Sozeau and Timany assume Coq programs have already been translated to use eliminators. Can that be done without the problematic normalization? How?
Here’s the key paragraph from Timany and Sozeau (emphasis mine):
On the other hand, the occurrences of recursive calls in recursive functions are may be hidden under some computations. That is, in order to obtain the position and arguments of recursive calls, which are crucial for constructing the model of recursive functions, in general requires normalizing the body of the recursive function. It so appears that the intention of Lee and Werner [2011] is to construct a set theoretic model for Coq, assuming the normalization property which already implies soundness of their system.
I’m sorry for my poor understanding. Can I consider that ZF + countably infinite inaccessible cardinals is enough to prove consistency of Coq? Does Lee and Werner’s proof show such an axiom (without choice and assuming normalization property) implies consistency of CC with predicative induction?
I’m not sure; Timany’s PhD thesis also discusses the same topic, and it says (in Sec. 4.5) that it’s unclear how Lee and Werner avoid the use of choice, and I’m certain I cannot comment on that.
Furthermore, we work in ZFC set theory and use the axiom of choice only to show that the interpretation of inductive types constructed through fixpoints does indeed belong to the interpretation of the sort of the inductive type. Lee and Werner (2011) work in ZF (with suitable cardinals, similarly to what we have assumed below) but we were not able to find a proof of this aspect of correctness of their interpretation of inductive types. See Appendix B for details of why and how we use the axiom of choice.