18
$\begingroup$

This answer says,

IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles — see Benjamin Werner's "Sets in types, types in sets". (This is because of the presence of a universe hierarchy in the CIC.)

But, I read "Sets in types, types in sets" and discovered that the book does not prove this statement. It only conjectures the strength of CIC.

Has "CIC and ZFC + countably many inaccessible cardinals are equiconsistent" been proven or disproven?

$\endgroup$
15
  • $\begingroup$ I just skimmed through Werner's paper, but it seems that it at least implies the consistency of $n$-inaccessible cardinals for all $n$. $\endgroup$
    – Asaf Karagila
    Commented Jan 6, 2021 at 15:47
  • 5
    $\begingroup$ @Asaf I also checked the paper, but the paper assumes the additional axioms like excluded middle or Type-theoretical Description Axiom $\mathsf{TTDA}_i$ (Definition 12) to interpret axioms of $\mathsf{ZF}$. I am not sure that these axioms do not increase the proof-theoretic strength of $\mathsf{CIC}$. Although the author mentioned we may rely on a weaker axiom, it does not mean we can interpret $\mathsf{ZF}$ within the mere $\mathsf{CIC}$. $\endgroup$
    – Hanul Jeon
    Commented Jan 6, 2021 at 17:17
  • 2
    $\begingroup$ Even worse, the author said that the justification of $\mathsf{TTDA}_i$ (maybe over the interpretation of $\mathsf{TTDA}_i$ over $\mathsf{ZFC}$) uses the axiom of choice, which is deemed to be highly non-constructive. $\endgroup$
    – Hanul Jeon
    Commented Jan 6, 2021 at 17:19
  • 2
    $\begingroup$ There's a related paper by Aczel, On relating type theories and set theories, which says that (in a closely related though not identical setting), the choice axiom does not affect the proof-theoretic strength. See the bottom of page 18. But I am not sure if that carries over to your setting. $\endgroup$ Commented Jan 6, 2021 at 23:48
  • 3
    $\begingroup$ The paper arxiv.org/abs/1111.0123 by Lee and Werner is newer and might be somewhat relevant. It treats Calculus of constructions (not CIC) but it also discusses induction and recursion. $\endgroup$ Commented Mar 9, 2022 at 10:38

2 Answers 2

8
$\begingroup$

The situation is a bit subtle. One can interpret CIC in any model of ZFC with infinitely many inacessibles. However, interpreting ZFC in CIC is more subtle. First one needs to assume the law of excluded middle and choice in CIC (and perhaps quotient types depending on how smooth we want things to work). These are very strong assumptions and they increase the consistency strength over plain CIC, which appears to be much weaker.

Once excluded middle and choice are assumed, within each universe level $\mathcal{U}_1,\mathcal{U}_2,\ldots$ of CIC we can construct a model of ZFC. This constructs a chain $V_1 \subseteq V_2 \subseteq \cdots$ of models of ZFC where each is an end extension of the previous, up to canonical isomorphism. Thus, $V_2$ has at least one inaccessible, $V_3$ has at least two inaccessibles, and so on. Thus CIC with choice proves the consistency of ZFC + there are $k$ inaccessibles for any standard $k$. Note that I've been careful not to associate universe levels with natural numbers. Indeed, models of CIC and ZFC can have nonstandard natural numbers. However, universe levels are syntactic objects and therefore always standard.

So, the consistency of CIC with choice and excluded middle implies the $\Pi_1$ statement $$\forall k\,\operatorname{Con}(ZFC + k\text{-many inaccessibles})\tag{*}.$$ This is strictly weaker than the consistency of ZFC with infinitely many inaccessibles. However, $(*)$ is actually enough to construct a full model of CIC! By compactness, we can construct a model $V$ of ZFC with $k$ inaccessibles, where $k$ is nonstandard. In this model, we can list the first standardly many inaccessibles as $\kappa_1 < \kappa_2 < \cdots$. This hierarchy allows us to construct a corresponding sequence of universes for a model of CIC. Note that this is not an interpretation per se since we can only witness externally that $k$ is nonstandard.

Nevertheless, from the above it follows that the consistency strength of CIC with excluded middle and choice is exactly $(*)$ and therefore strictly weaker than ZFC with infinitely many inaccessibles.

$\endgroup$
11
  • $\begingroup$ Just to clarify -- am I right in assuming that CIC without choice or excluded middle is vastly, vastly weaker than ZFC? Probably closer in strength to something like PA (as an extremely rough estimate)? $\endgroup$ Commented Mar 14, 2022 at 12:39
  • $\begingroup$ I could only conjecture. I don't know any other model constructions for CIC. $\endgroup$ Commented Mar 14, 2022 at 13:12
  • 1
    $\begingroup$ @TimCampion: I am also interested in this question, but don't have the expertise to help. Does this article by Rathjen and this post imply that CIC is stronger than MLTT which is stronger than Σ[1,2]-CA+BI? If so, then CIC would be well into impredicativity, far above ATR0. $\endgroup$
    – user21820
    Commented Mar 29, 2022 at 16:56
  • 1
    $\begingroup$ @TimCampion: Pending clarification of what exactly "CIC" means there, this answer asserts that even without LEM and Choice, CIC is already way stronger than Z, though still weaker than ZFC. $\endgroup$
    – user21820
    Commented Mar 31, 2022 at 17:10
  • 2
    $\begingroup$ @user21820 Yes, I've read Rathjen's paper but it is not immediately clear where CIC fits in. It does seem that $\forall n$Con($\Sigma^1_2$-AC + BI + Beta$(n)$) is the right ballpark but there's a lot of fine detail to check. $\endgroup$ Commented Apr 1, 2022 at 0:17
2
$\begingroup$

I think "Une Théorie des Constructions Inductives" (Benjamin Werner) implies that "CIC and ZFC + countably many inaccessible cardinals are equiconsistent" is wrong. The paper proves the consistency of CIC on ZFC + countably many inaccessible cardinals.

$\endgroup$
1
  • 5
    $\begingroup$ Please could you give a bit more information in this answer — at least a reference to the specific result/section within the thesis, and (ideally) a short summary of how it disproves the conjecture? That’s always good practice, but especially in this case, it’s a 160-page thesis, in French, and the copies I can find are not text-searchable — so it’s quite difficult for most readers to skim through in search of relevant results. $\endgroup$ Commented Mar 9, 2022 at 12:03

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .