This week I was working on reimplementing Benjamin Werner’s model of Z / ZF / ZFC in Coq by bringing it up to date and using the classical subset of constructive logic rather than assuming classical axioms. Benjamin’s work shows how to build a model of Z in Coq. Under some additional choice-style axioms this model can be shown to be a model of ZF or ZFC.
My work lead me to the Wikipedia article on ordinal analysis, which has shaken my belief in the consistency of Z.
As I understand, Gentzen showed that believing in the consistency of PA is equivalent to believing in the well-foundedness of ε0. This can be rephrased as a claim that a particular program, say the hydra game, terminates on all inputs. Therefore, if you believe in the well-foundness of ε0 and you believe Gentzen’s argument, which is done in PRA, then you believe PA is consistent, even if it has impredicative induction principles.
PRA has consistency strength equivalent to the well-foundness of ωω, which can be stated again as the termination of some other program on all inputs. Presumably this equivalence is proved in a still weaker system. I wonder if this process can be iterated down to the well-foundness of ω, as a sort of modified Hilbert’s program?
Looking up in the ordinal hierarchy, we see that the consistency of Martin-Löf type theory is equivalent to the well-foundedness of Γ0. I have not studied this ordinal, but it appears to have a well defined ordinal notation which would presumably convince me of its well-foundedness.
As I understand, Agda 2 is an implementation of Martin-Löf type theory, thus Benjamin’s model of Z cannot be ported to Agda 2. Indeed, the definition of the model uses the impredicativity of Coq at one point to prove that it satisfies the power set axiom.
This brings me to my main concern. According to the Wikipedia article on ordinal analysis, Most theories capable of describing the power set of the natural numbers have proof theoretic ordinals that are (as of 2008) so large that no explicit combinatorial description has yet been given.
Can we really believe in the consistency of any system whose ordinal strength we do not have a notation for? This includes ZF, Z, and yes, even Coq. Coq’s impredicative in Prop seems innocent because no information is allowed to flow from the Prop universe to the Set universe; however Prop values can witness termination of functions in Set.
Perhaps there is an inconsistency arising from the impredicativity of Prop that “proves” the termination of some non-terminating function.