Timeline for Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 9, 2022 at 6:51 | comment | added | Hanul Jeon | 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? | |
| Apr 27, 2022 at 1:54 | comment | added | Hexirp | In my question, CIC includes an impredicative Prop. Therefore this can prove the strong normalization of System F. | |
| Apr 27, 2022 at 1:46 | vote | accept | Hexirp | ||
| Apr 2, 2022 at 22:06 | comment | added | François G. Dorais | 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. | |
| Apr 2, 2022 at 17:19 | comment | added | user21820 | @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"? | |
| Apr 1, 2022 at 23:45 | comment | added | François G. Dorais | @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. | |
| Apr 1, 2022 at 13:48 | comment | added | user21820 | @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. | |
| Apr 1, 2022 at 0:17 | comment | added | François G. Dorais | @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. | |
| Mar 31, 2022 at 17:10 | comment | added | user21820 | @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. | |
| Mar 29, 2022 at 16:56 | comment | added | user21820 | @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. | |
| Mar 14, 2022 at 13:12 | comment | added | François G. Dorais | I could only conjecture. I don't know any other model constructions for CIC. | |
| Mar 14, 2022 at 12:39 | comment | added | Tim Campion | 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)? | |
| Mar 14, 2022 at 12:25 | history | answered | François G. Dorais | CC BY-SA 4.0 |