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

Question

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!

Answer 1

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'.

Answer 2

There is a generalization of Gödel's incompleteness theorem that is more naturally applicable to MLTT: Löb's theorem says that to prove $P$, it suffices to prove that $P$ is true whenever $P$ is provable. Symbolically, using $\square P$ to mean "$P$ is provable", this is $$\square(\square P \to P)\to \square P$$

If you instantiate $P$ with a contradiction (say, $1=0$ or $\bot$), you get Gödel's incompleteness theorem: $$\square(\square \bot \to \bot)\to \square \bot$$ or, using the fact that $\neg A$ is $A\to \bot$, $$\square(\neg\square \bot)\to \square \bot$$ If your theory is consistent, i.e., if $\square P \to P$, then this becomes $$\neg\square(\neg\square \bot)$$ or "you cannot prove that there is no proof of false". In the standard phrasing of Gödel's incompleteness theorem, this would be "the statement 'there is no proof of false' is true, but unprovable".

While formalizing theorems and proofs using natural numbers is standard in set theory, in MLTT, it's much more natural to formulate provability by giving an inductive type of theorems (also called types), and an inductive type of proofs (also called terms).

---

A standard presentation of simply typed lambda calculus in HOAS might define (using Agda notation)

open import Agda.Builtin.Unit

infixr 1 _‘→’_

data ⊥ : Set where

data Type : Set where
  _‘→’_ : Type → Type → Type
  ‘⊤’ : Type
  ‘⊥’ : Type

⟦_⟧ᵀ : Type → Set
⟦ A ‘→’ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
⟦ ‘⊤’ ⟧ᵀ = ⊤
⟦ ‘⊥’ ⟧ᵀ = ⊥

data Term : Type → Set where
  lam : ∀ {A B} → ( ⟦ A ⟧ᵀ → Term B ) → Term (A ‘→’ B)
  app : ∀ {A B} → Term (A ‘→’ B) → Term A → Term B
  ‘tt’ :  Term ‘⊤’

⟦_⟧ᵗ : ∀ {T} → Term T → ⟦ T ⟧ᵀ
⟦ lam f ⟧ᵗ = λ a → ⟦ f a ⟧ᵗ
⟦ app f a ⟧ᵗ = ⟦ f  ⟧ᵗ ⟦ a ⟧ᵗ
⟦ ‘tt’ ⟧ᵗ = tt

Our interpretation function, ⟦_⟧ᵗ, proves that this theory is consistent relative to Agda. Said another way, we can use ⟦_⟧ᵗ to prove that no Term inhabits the empty type, ‘⊥’:

¬_ : Set → Set
¬ A = A → ⊥

□ = Term

consistent : ¬ □ ‘⊥’
consistent = ⟦_⟧ᵗ

Now, here is a neat trick you can play to get most of the power of Löb's theorem when your formalization is not HOAS: given any formalization of type theory (or lambda calculus) with a sufficiently nice proof of consistency relative to Agda (i.e., an interpretation function that is simple or local enough that the theory can be extended without needing to modify the interpretation of existing constructs), you can add a term for Löb's theorem, and give it an interpretation.

We extend the definition of Types with a type of theorems (named ‘□’), and we extend the type of Terms with a proof of Löb's theorem. To satisfy the positivity checker, we index terms over a context, rather than using HOAS.

record _×_ (A : Set) (B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

data Type : Set where
  _‘→’_ : Type → Type → Type
  ‘⊤’ : Type
  ‘⊥’ : Type
  ‘□’ : Type → Type

Now we have an inductive type of Contexts, which is a list of Types which can be accessed via variables:

data Context : Set where
  ε : Context
  _▻_ : (Γ : Context) → Type → Context

data Term : Context → Type → Set where
  lam : ∀ {Γ A B} → Term (Γ ▻ A) B → Term Γ (A ‘→’ B)
  app : ∀ {Γ A B} → Term Γ (A ‘→’ B) → Term Γ A → Term Γ B
  var₀ : ∀ {Γ A} → Term (Γ ▻ A) A
  varₙ : ∀ {Γ A B} → Term Γ A → Term (Γ ▻ B) A
  ‘tt’ : ∀ {Γ} → Term Γ ‘⊤’
  Löb : ∀ {P} → Term ε (‘□’ P ‘→’ P) → Term ε P

Note that we only add a constructor for Löb's theorem in the empty context.

We can again define interpretation functions, proving that this theory is consistent relative to Agda:

□ = Term ε

⟦_⟧ᵀ : Type → Set
⟦ A ‘→’ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
⟦ ‘⊤’ ⟧ᵀ = ⊤
⟦ ‘⊥’ ⟧ᵀ = ⊥
⟦ ‘□’ P ⟧ᵀ = □ P

⟦_⟧ᶜ : Context → Set
⟦ ε ⟧ᶜ = ⊤
⟦ Γ ▻ A ⟧ᶜ = ⟦ Γ ⟧ᶜ × ⟦ A ⟧ᵀ

⟦_⟧ᵗ : ∀ {Γ T} → Term Γ T → ⟦ Γ ⟧ᶜ → ⟦ T ⟧ᵀ
⟦ lam f ⟧ᵗ Γᵥ = λ a → ⟦ f ⟧ᵗ (Γᵥ , a)
⟦ app f a ⟧ᵗ Γᵥ = ⟦ f ⟧ᵗ Γᵥ (⟦ a ⟧ᵗ Γᵥ)
⟦ var₀ ⟧ᵗ (Γᵥ , a) = a
⟦ varₙ v ⟧ᵗ (Γᵥ , a) = ⟦ v ⟧ᵗ Γᵥ
⟦ ‘tt’ ⟧ᵗ Γᵥ = tt
⟦ Löb interp ⟧ᵗ tt = ⟦ interp ⟧ᵗ tt (Löb interp)

Note the interpretation of Löb's theorem: the premise of Löb's theorem, across the Curry-Howard isomorphism, is (syntax for) a compiler or an interpreter: it is a thing that takes in syntax for a term of type $P$ and spits out an actual term of type $P$. Since our interpretation function is nicely local, we can use this interpreter to interpret Löb's theorem! Note that this is very similar to the proof that the Halting Problem is undecidable; there, you take a putative decider, and run it on a slight modification of itself, causing it go awry; here you take a putative interpreter, and run it on a wrapped version of itself, causing it to loop.

Finally, we can get consistency and incompleteness of this theory:

¬_ : Set → Set
¬ A = A → ⊥

‘¬’_ : Type → Type
‘¬’ P = P ‘→’ ‘⊥’

consistent : ¬ □ ‘⊥’
consistent absurd = ⟦ absurd ⟧ᵗ tt

incomplete : ¬ □ (‘¬’ (‘□’ ‘⊥’))
incomplete interp = ⟦ Löb interp ⟧ᵗ tt

---

This argument does not show that Löb's theorem is provable in MLTT; it merely argues that Löb's theorem is admissible as an axiom in MLTT (and hence is true as a metatheorem of MLTT). If you are interested in actually constructing the Löbian sentence in a formalization of MLTT based on simpler primitives, I refer you to this blog post by Neelakantan Krishnaswami on how Löb's theorem is basically the same thing as the Y combinator, or to this unpublished paper that I wrote about a formalization similar to the one described here, or to this repo where I have a number of stabs at formalizing variants of Löb's theorem.

---

To answer your questions more directly:

1. How can we construct the Gödel’s sentence $G$ in MLTT?

You can axiomatize it as part of your formalization of MLTT (and show that doing so doesn't break consistency); or you can construct it in a way analogous to the Y combinator.

3. What interpretation are we referring when we say that $G$ is true?

As I understand it, when you define syntax for a theory, you should also define a standard model, and an interpretation function into that model. In the formalization I gave above, the standard model is Agda, and the interpretation function is ⟦_⟧ᵀ for theorems and ⟦_⟧ᵗ for proofs. To say that something is "true" is to say that it is true in the model, i.e., is provable of the model. Hence a proof of "P is true in the standard model" is an inhabitant of ⟦ P ⟧ᵀ.

2. How come there is no contradiction if $G$ is true but it is not inhabited?

The better question is, what would the contradiction be? Inhabitation talks about syntax trees, while truth talks about inhabitation of the interpretation of a type. It is very simple to have a syntactic type with no syntactic term of that type, but to say that the interpretation of that type is $\top$. To make this more concrete, here is a formalization of a theory where every sentence is true but unprovable:

data Type : Set where
  ‘⊤’ : Type

data Term : Type → Set where

⟦_⟧ᵀ : Type → Set
⟦ ‘⊤’ ⟧ᵀ = ⊤

⟦_⟧ᵗ : ∀ {T} → Term T → Set
⟦ () ⟧ᵗ

¬_ : Set → Set
¬ A = A → ⊥

true : (T : Type) → ⟦ T ⟧ᵀ
true ‘⊤’ = tt

unprovable : (T : Type) → ¬ Term T
unprovable ‘⊤’ ()

Answer 3

Maria Emilia Maietti starts her http://www.sciencedirect.com/science/article/pii/S1571066104805693 by saying that "André Joyal constructed arithmetic universes to provide a categorical proof of Gödel incompleteness results." and she goes on to connect Joyal's universes with MLTT, so I think you could start by reading her work.

Answer 4

I am a little bit rusty on the subject so I hope whatever I am going to say is correct (otherwise someone else will possibly correct me and I'll learn something :) ).

Before I start allow me to stress that Gödel's incompleteness theorems deal with PA (Peano Arithmetic) while it's Rosser's theorem that generalizes the incompleteness result to formal systems capable of interpreting arithmetic. In particular Rosser's theorem states that

For every formal system $T$, capable of interpreting (Robinson's) arithmetic, if $T$ is consistent then it's incomplete: i.e. there is a formula $\varphi$ such that neither $T \vdash \varphi$ nor $T \vdash \neg \varphi$.

In particular note that this theorem has nothing to due with truth of a formula, but I'll get back to this later.

If I've understood correctly your line of argument go like this: we have that MLTT is equivalent to HOL (intuitionstic Higher-Order Logic) hence we can interpret arithmetic in such system (providing some axioms to MLTT that allows to build the types/predicates required to interpret arithmetic), hence Rosser's theorem applies.

In this case

1. How can we construct the Gödel’s sentence $G$ in MLTT?

we basically follows the steps for the proof on Rosser's theorem to find the wished formula $G$ using the Rosser's trick.

Using the encoding of arithmetic in MLTT we can build a predicate/type $\text{Proof}(x,y)$ such that for every $n$ and $m$, terms representing natural numbers, $\text{Proof}(n,m)$ is provable in MLTT if and only if $n$ an encoding for a proof of the proposition encoded by $m$.

Then we can consider the formula/type

$$\text{Proof}^R(x,y) \equiv \text{Proof}(x,y) \land \neg \exists z \leq x \text{Proof}(z,\neg x)$$ (here by $\neg x$ we mean the encoding of the negation of the formula encoded by $x$).

Using the diagonal lemma there is a formula $G$ such that MLTT prove that $$G \leftrightarrow \neg\exists x\text{Proof}^R(x,\lceil G \rceil)$$ (where $\lceil G\rceil$ denotes the natural number encoding $G$).

From this one can prove that clearly $G$ cannot be proved or disproved (i.e. its negation cannot be proved either) from MLTT.

What is this formula $G$? Well to find out you should unravel the proof of diagonal lemma and find out how to build the formula $G$, though I strongly suggest not to do that.

I hope this fully address the first point of the question.

2. How come there is no contradiction if $G$ is true but it is not inhabited?

The problem here lies in what do you mean by being true.

As I told you before Rosser's theorem deals with provability not with truth and there is a reason why I stressed this in the begging.

If you limit yourself to consider only first-order theories, with Tarski's semantics, then you have Gödel's completeness theorem which states that

$T \models \varphi$, that is $\varphi$ is true (in the Tarskian sense) in every models of $T$, then $T \vdash \varphi$, that is $T$ proves $\varphi$.

In this, very specific, case where for every model $M$ of $T$ either $\varphi$ is true in $M$ or $\neg \varphi$ is true in $T$, you can rephrase Rosser's theorem in the following way:

If $T$ is first-order theory which is capable to interpret arithmetic then if $T$ is consistent there is a formula $\varphi$ that is true in some models of $T$ but it's not provable from $T$.

In particular if by $T$ you take PA and consider the model of natural numbers $\mathbb N$ you get that there is formula $\varphi$ which is true in $\mathbb N$ (this formula is either the $G$ build before or $\neg G$) but it's not provable from PA.

So after this very long introduction what's the problem here?

Well for start we are working in MLTT which as I stated before we are regarding as HOL and there is no completeness theorem for HOL (at least if you are using the Tarskian semantics), so cannot rephrase Rosser's theorem in a semantic form (as we did for first-order logic).

Second of all you are using an entirely different kind of semantics: when you say that a formula/type $P$ is true if and only if there is a term $t$ such that $t : P$ you are using a provability semantics, meaning that you are using a semantics that states that a proposition is true only when you can build a proof for it (this is what the formulas-as-type paradigm does).

Since the semantics you are using is not Tarski's semantics the semantics form of Gödel/Rosser's theorem does not hold here, because you mean something different by true.

3. What interpretation are we referring when we say that $G$ is true?

Well I guess I've already addressed this point of the question above.

I hope this helps.

If you need any additional clarification, please let me know in the comments below.

Answer 5

In CTT truth of a proposition, indeed, is expressed as the instantiation of its set of proofs:

$$ A \text{ is true } = \mathsf{Proof}(A) \text{ exists} \tag{1} $$

where the existence is the Brouwer-Weyl constrcutive notion of existence, defined by the assertion condition:

$$a \text{ is an } \alpha \implies \alpha \text{ exists} $$

Consider now what we may call the "arithmetical fragment" of CTT, given in the language that comprises the connectives and quantifiers, and the natural numbers, plus the appropriate constructors, with the usual introdcution and elimination rules for the connectives and quantifiers, and the definition by recursion as elimination rule for the set $\mathbb{N}$.

Question 1: Gödel's theorem then takes the form: there is an an arithmetical proposition $G$, for which we can construct a proof-object, but this cannot be done using just the constructors pertaining only to the arithmetical fragment. This takes care of question 1.

Question 2: The set $\mathsf{Proof}(G)$ is instantiated by a proof-object $t$, but this cannot be given just by using the "arithmetical constructors".

Question 3: the standard CTT notion of propositional truth given by $(1)$. I have dealt with these matters in some detail in my 'Antirealism and the Roles of Truth' in the Handbook of Epistemology. The article can be found here and §8, pp. 456-459, spells out the Gödel issues for CTT.