Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic".

Homotopy Type Theory provides an alternative foundation for mathematics, a univalent foundation based on higher inductive types and the univalence axiom. The HoTT book explains that types are higher groupoids, functions are functors, type families are ﬁbrations, etc.

The recent article "Formally Verified Mathematics" in CACM by Jeremy Avigad and John Harrison discusses HoTT with respect to formally verified mathematics and automatic theorem proving.

Do Gödel's incompleteness theorems apply to HoTT?

And if they do,

is homotopy type theory impaired by Gödel's incompleteness theorem (within the context of formally verified mathematics)?

  • 8
    $\begingroup$ Interesting question. Was there something you read that suggested to you that HTT doesn't suffer from Godel Incompleteness? (Note that previous attempts at foundations - such as set theory - also suffer from Godel Incompleteness...) $\endgroup$ – Joshua Grochow Apr 15 '14 at 15:17

HoTT "suffers" from Gödel incompleteness, of course, since it has a computably enumerable language and rules of inference, and we can formalize arithmetic in it. The authors of the HoTT book were perfectly aware of its incompletness. (In fact, this is quite obvious, especially when half of the authors are logicians of some sort).

But does incompleteness "impair" HoTT? No more than it does any other formal system, and I think the whole issue is a bit misguided. Let me try an analogy. Suppose you have a car which can't take you everywhere on the planet. For instance, it can't climb vertically up a wall. Is the car "impaired"? Of course, it can't get you to the top of the Empire State building. Is the car useless? Far from it, it can take you too many other interesting places. Not to mention that the Empire State building has elevators.

| cite | improve this answer | |
  • 3
    $\begingroup$ I don' think the car analogy quite works as the question isn't so much "Is the car useless?" but "Can the car serve as the foundation transportation?" But, in any case, the fundamental point stands that any system that is going to be a foundation of mathematics is necessarily incomplete. $\endgroup$ – David Richerby Apr 16 '14 at 7:17
  • 7
    $\begingroup$ My point was that people do not expect a perfect transportation machine to exist, and neither do they worry that there isn't one, but somehow they worry about the fact that no (reasonable) foundation of mathematics is complete. $\endgroup$ – Andrej Bauer Apr 16 '14 at 7:22

Your Answer

