19

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?

YCor
  • 60,149
Hexirp
  • 335
  • I just skimmed through Werner's paper, but it seems that it at least implies the consistency of $n$-inaccessible cardinals for all $n$. – Asaf Karagila Jan 06 '21 at 15:47
  • 5
    @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}$. – Hanul Jeon Jan 06 '21 at 17:17
  • 2
    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. – Hanul Jeon Jan 06 '21 at 17:19
  • @Hanul: Thanks for the clarification! – Asaf Karagila Jan 06 '21 at 17:23
  • 2
    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. – Timothy Chow Jan 06 '21 at 23:48
  • @TimothyChow Excluded middle distracts the strength of $\mathsf{MLU}$ or its extensions: $\mathsf{MLW}$ with universes is no stronger than extensions of $\mathsf{KP}$. (See Theorem 4.1 of your linked paper. Also, note that $\mathsf{CZF}$ with large set axioms have at most stronger than extensions of $\mathsf{KP}$. My recent question might be relevant.) – Hanul Jeon Jan 07 '21 at 10:31
  • The same phenomenon happens at $\mathsf{CZF}$. $\mathsf{CZF}$ is dramatically weaker than $\mathsf{ZF}$, but if we add the law of excluded middle, then we have $\mathsf{ZF}$. – Hanul Jeon Jan 07 '21 at 10:32
  • @HanulJeon : I'm confused by your comment. We're talking about choice, not excluded middle, right? – Timothy Chow Jan 07 '21 at 13:41
  • @TimothyChow I am also a bit confused. Is not the topic about the axiom of choice over type theories? However, your quoted sentence by Aczel (the bottom of page 18) apparently talks about the axiom of global choice over $\mathsf{ZF}$, not over type theories. – Hanul Jeon Jan 07 '21 at 14:00
  • @TimothyChow (I agree that my previous answer is out of topic. There was a misunderstanding because $\mathsf{MLW}$ proves an intentional form of the axiom of choice, so I guessed choice should not be the main issue.) – Hanul Jeon Jan 07 '21 at 14:05
  • Ah, yes, I see now that Aczel does not directly discuss choice for type theories. – Timothy Chow Jan 07 '21 at 17:34
  • I am not sure the relation between MLTT and CIC, but I guess the system $\mathsf{MLV_P}$ (defined in Rathjen's paper Power Set, and the Calculus of Constructions) is interpretable within $\mathsf{CIC}$. Thus I guess the proof-theoretic strength of $\mathsf{CIC}$ is at least that of $\mathsf{KP}^\mathcal{P}$. – Hanul Jeon Jan 07 '21 at 21:02
  • I found out that Une Théorie des Constructions Inductives seems to prove the strong normalization of the Calculus of Inductive Constructions. If this is a result of work on ZFC, it gives the answer to my question. – Hexirp Jan 12 '21 at 07:48
  • I think your question is not answered long while. How about to cross-post your question on Theoretical CS.SE or CS.SE? – Hanul Jeon Jan 19 '21 at 15:18
  • 3
    The paper https://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. – Andrej Bauer Mar 09 '22 at 10:38

2 Answers2

9

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.

François G. Dorais
  • 43,723
  • 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)? – Tim Campion Mar 14 '22 at 12:39
  • I could only conjecture. I don't know any other model constructions for CIC. – François G. Dorais Mar 14 '22 at 13:12
  • 1
    @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. – user21820 Mar 29 '22 at 16:56
  • 1
    @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. – user21820 Mar 31 '22 at 17:10
  • 2
    @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. – François G. Dorais Apr 01 '22 at 00:17
  • @FrançoisG.Dorais: It seems that most people use "CIC" to refer to the calculus of inductive constructions with an infinite hierarchy of universes and impredicative Prop, in which case it is way above MLTT. In other words, MLTT is not that strong because it only has a single impredicative notion via W-types, something like how Π[1,1]-CA0 is essentially ATR0 plus a single impredicative notion of closure under monotonic operators. In contrast, CIC with the impredicative Prop far outstrips this kind of impredicativity because it is truly impredicative; we cannot even approach it from below. – user21820 Apr 01 '22 at 13:48
  • @user21820 I'm well aware. But I don't buy the impredicative Prop argument at all. Most of the interpretation arguments I've seen basically give an impredicative Prop for free. (Usually at the cost of one universe level to allow quantification.) I think impredicative Prop is more like stamina than muscle, it can't do anything on its own but it really helps other things working harder. – François G. Dorais Apr 01 '22 at 23:45
  • @FrançoisG.Dorais: Are you saying that the linked post is wrong about the strength of CIC being above Z set theory? If not, why did you say that a weak subsystem of Z2 "is the right ballpark"? – user21820 Apr 02 '22 at 17:19
  • Like I said, I don't know. However, the theory I mentioned is not "weak subsystem of Z2", it is not even a "subsystem of Z2"! It's not because something is formulated in the context of second-order arithmetic that it is provable in Z2. For example, Friedman famously showed that Borel determinacy is much stronger than Zermelo set theory and well beyond Z2 even though Borel determinacy can be stated in the language of second-order arithmetic. – François G. Dorais Apr 02 '22 at 22:06
  • In my question, CIC includes an impredicative Prop. Therefore this can prove the strong normalization of System F. – Hexirp Apr 27 '22 at 01:54
  • Dorais, do you think your argument with nonstandard models shows CIC with excluded middle and choice and ZFC with $k$ many inaccessibles (for each meta-natural $k$) have the same arithmetic (or, $\Pi^0_2$) consequences? – Hanul Jeon Nov 09 '22 at 06:51
2

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.

Hexirp
  • 335
  • 5
    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. – Peter LeFanu Lumsdaine Mar 09 '22 at 12:03