<p>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).</p>

<p>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.</p>

CC BY-SA 3.0
2014-04-16T07:17:32.973Z
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.
David Richerby
CC BY-SA 3.0
2014-04-16T07:22:22.377Z
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.
Andrej Bauer
CC BY-SA 4.0
2021-06-15T02:26:03.610Z
@AndrejBauer Is there a paper with technical details, such as the method of assigning Gödel numbers?
simple jack
CC BY-SA 4.0
2021-06-15T06:44:22.033Z
There are a number of logic textbooks that explain Gödel numbering. Are you asking for a particular title?
Andrej Bauer
CC BY-SA 3.0
2014-04-16T06:25:09.087Z
2014-04-16T06:25:09.087Z
Andrej Bauer
<p><a href="http://en.wikipedia.org/wiki/Kurt_G%C3%B6del" rel="noreferrer">Kurt Gödel</a>'s <a href="http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems" rel="noreferrer">incompleteness theorems</a>  establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic". </p>

<p><a href="https://en.wikipedia.org/wiki/Homotopy_type_theory" rel="noreferrer">Homotopy Type Theory</a> provides an alternative foundation for mathematics, a <em>univalent</em> foundation based on <a href="https://en.wikipedia.org/wiki/Inductive_type#Higher_Inductive_Types" rel="noreferrer">higher inductive types</a> and the <a href="https://en.wikipedia.org/wiki/Univalence_axiom" rel="noreferrer">univalence axiom</a>. 
The <a href="http://homotopytypetheory.org/book/" rel="noreferrer">HoTT book</a> explains that types are higher groupoids, functions are functors, type families are ﬁbrations, etc. </p>

<p>The recent article <a href="http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext" rel="noreferrer">"Formally Verified Mathematics"</a> in CACM 
by Jeremy Avigad and John Harrison 
discusses HoTT with respect to 
formally verified mathematics and automatic theorem proving. </p>

<blockquote>
  <p>Do Gödel's incompleteness theorems apply to HoTT?</p>
</blockquote>

<p>And if they do,</p>

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

CC BY-SA 3.0
2014-04-15T15:17:11.977Z
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...)
Joshua Grochow
<lo.logic><type-systems><homotopy-type-theory>
Homotopy type theory and Gödel's incompleteness theorems
hawkeye
# Homotopy type theory and Gödel's incompleteness theorems

(Asked by: username_0 on 2014-04-15)

[Kurt Gödel](http://en.wikipedia.org/wiki/Kurt_G%C3%B6del)'s [incompleteness theorems](http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems) establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic".

[Homotopy Type Theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) provides an alternative foundation for mathematics, a *univalent* foundation based on [higher inductive types](https://en.wikipedia.org/wiki/Inductive_type#Higher_Inductive_Types) and the [univalence axiom](https://en.wikipedia.org/wiki/Univalence_axiom).
The [HoTT book](http://homotopytypetheory.org/book/) explains that types are higher groupoids, functions are functors, type families are ﬁbrations, etc.

The recent article ["Formally Verified Mathematics"](http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext) 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)?

**Tags:** lo.logic, type-systems, homotopy-type-theory

> **Comments:**
> **username_1**: 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...)  

---

## 1 answers

### Answer by username_2 on 2014-04-16. Score: 34 | Accepted answer

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.

> **Comments:**
> **username_3**: 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.  
> **username_2**: 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.  
> **username_4**: @AndrejBauer Is there a paper with technical details, such as the method of assigning Gödel numbers?  
> **username_2**: There are a number of logic textbooks that explain Gödel numbering. Are you asking for a particular title?  

---

