There is a model of ZFC in homotopy type theory

Does exist a model of homotopy type theory in ZFC?

Is there a proof of "equal logical expressivity" of these theories?

p.s. I use word "model" in common sense, because I don't know model theory


Yes, as long as by "ZFC" you include its extension with some inaccessible cardinals, or (perhaps) are willing to play games with natural models. In other words, the only difference in consistency strength is that "ZFC" by default doesn't include any universes, while "HoTT" by default includes countably many.

  • 2
    $\begingroup$ I'm confused - doesn't this require 2 inaccessibles? (Or am I not parsing it right?) $\endgroup$ – Noah Schweber Dec 25 '15 at 22:06
  • 3
    $\begingroup$ The correct answer is "No", Mike, and your link indicates that. You may want to clarify what you mean. (Of course, the answer is "yes" if $\mathsf{ZFC}$ is replaced with one of its standard extensions via large cardinals, but that seems to be precisely the point of the question.) $\endgroup$ – Andrés E. Caicedo Dec 25 '15 at 22:37
  • 1
    $\begingroup$ It was not at all obvious to me that that is the point of the question, but I'll edit to clarify. $\endgroup$ – Mike Shulman Dec 26 '15 at 22:48
  • $\begingroup$ Countably many with only two inaccessible cardinals? $\endgroup$ – Asaf Karagila Dec 27 '15 at 5:18
  • $\begingroup$ @AsafKaragila The universes here are not Grothendieck universes. The model is built starting from two Grothendieck universes. It has strength beyond $\mathsf{ZFC}$ because you can interpret set theory inside. $\endgroup$ – Andrés E. Caicedo Dec 27 '15 at 14:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.