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:
- How can we construct the Gödel’s sentence $G$ in MLTT?
- How come there is no contradiction if $G$ is true but it is not inhabited?
- What interpretation are we referring when we say that $G$ is true?
Any help is highly appreciated!