15
$\begingroup$

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 fibrations, 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)?

Improve this question
$\endgroup$
1
  • 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
    Commented Apr 15, 2014 at 15:17

1 Answer 1

Reset to default
34
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 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
    Commented Apr 16, 2014 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
    Commented Apr 16, 2014 at 7:22
  • $\begingroup$ @AndrejBauer Is there a paper with technical details, such as the method of assigning Gödel numbers? $\endgroup$
    – simple jack
    Commented Jun 15, 2021 at 2:26
  • $\begingroup$ There are a number of logic textbooks that explain Gödel numbering. Are you asking for a particular title? $\endgroup$
    – Andrej Bauer
    Commented Jun 15, 2021 at 6:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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