Skip to main content
MathOverflow

Return to Question

formatting
Source Link
YCor
YCor
  • 63.9k
  • 5
  • 187
  • 285

Are we sure the Calculuscalculus of Inductive Constructionsinductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?

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""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""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?

Are we sure the Calculus of Inductive Constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?

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?

Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?

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?

Source Link
Hexirp
Hexirp
  • 325
  • 2
  • 10

Are we sure the Calculus of Inductive Constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?

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?