[Math] How do we construct the Gödel’s sentence in Martin-Löf type theory

categorical-logiclo.logictype-theory

In Martin-Löf dependent type theory (MLTT), under the proposition-as-types correspondence, we sometimes say that a proposition $A$ is true if the type $A$ is inhabited. However, there is no doubt that MLTT meets the minimum criteria of expressiveness of arithmetic required by Gödel’s first incompleteness theorem to apply, which then would imply the existence of "true but improvable propositions".

I am aware that the first, intuitionistic, notion of 'provability' (the one inherent to MLTT under the proposition-as-types) refers to provability in general and that the term 'improvable' in the incompleteness theorems refers to non-derivability in a given formal system.

Even so, I find this all very confusing. Especially because if there are true but improvable propositions in MLTT, then there is a type $G$ that is true, but the judgment $g : G$ is not derivable within the system for any term $g$!

My doubts are further aggravated by the fact that most material on Gödel's incompleteness theorems that can be found on the internet typically only cover first-order logical systems. To be precise, I am looking for type theory what has been done for category theory in this proof (§2) in this nLab entry on the incompleteness theorems
(I am also looking for something slightly more accessible, even though I have a basic understanding of category theory).

In any case, I will be very glad if anyone could shed some light in these issues. In particular:

  1. How can we construct the Gödel’s sentence $G$ in MLTT?
  2. How come there is no contradiction if $G$ is true but it is not inhabited?
  3. What interpretation are we referring when we say that $G$ is true?

Any help is highly appreciated!

Best Answer

I think we can assume MLTT is a formal system of the usual kind. Therefore, in formal arithmetic using Gödel numbering we can formulate the arithemetic statement con(MLTT), stating the consistency of the system. Surely we all believe this to be a "true" statement. Yes? So, cannot we guess -- invoking the ghost of Gödel -- that this statement is not going to be provable? Just askin'.

Related Question