28
$\begingroup$

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!

$\endgroup$
13
  • 5
    $\begingroup$ The overall question — “how can we transfer Gödel incompleteness from FOL to MLTT” — is I think excellent; I’ve wondered about it myself, and never done a thorough literature search for it, but it’s at least something I’m surprised there isn’t a very well-known account of. However re the second paragraph — “ 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!” — I think this a fairly standard qualm about incompleteness, that is really no stranger in type theory than in FOL. [cont’d] $\endgroup$ Jun 25, 2017 at 16:57
  • 5
    $\begingroup$ The point is just that “…a type/proposition G that is true…” doesn’t without context mean anything. What’s usually implicit is “…a type/proposition that is true in some model…” and in particular “…in the standard model”, i.e. using the sets of the ambient meta-theory, usually e.g. ZFC. But with that made explicit, it’s not so surprising that the meta-theory — being a stronger theory — can prove stronger theorems than the object theory, e.g. MLTT/PA. It can be helpful to consider an example like the Paris-Harrington theorem. It’s not provable in PA; but… [cont’d] $\endgroup$ Jun 25, 2017 at 17:01
  • 5
    $\begingroup$ …but it’s “true” in the sense that it holds in $\mathbb{N}$. But what we really mean by that is: we have proved in ZFC that it holds in $\mathbb{N}$. But then, again, all this is saying is that ZFC is a stronger theory than PA — more precisely, that the standard translation of PA into ZFC is not conservative. Which is not so shocking, in the end. (I am leaving these as comments not answers since they are only addressing a side question, not your main question.) $\endgroup$ Jun 25, 2017 at 17:03
  • 4
    $\begingroup$ For (1), is the situation different than any other theory that interprets arithmetic well enough to satisfy the requirements of the incompleteness theorem? The Gödel sentence $G(T)$ for an effective theory $T$ is, first and foremost, a sentence in the language of arithmetic, regardless of the theory $T$. Then we just use a sufficiently sound interpretation of the language of arithmetic into $T$. Is there a particular aspect of Martin-Löf type theory that makes this different than, say, IZF? $\endgroup$ Jun 27, 2017 at 0:14
  • 5
    $\begingroup$ @BrunoBentzen : I do not really understand MLTT, but surely if the set of theorems of MLTT is computably enumerable, then we're done, aren't we? The essence of incompleteness is that the set of arithmetical truths is not computably enumerable. For a slightly more detailed explanation see cs.nyu.edu/pipermail/fom/2004-August/008429.html and cs.nyu.edu/pipermail/fom/2004-August/008426.html $\endgroup$ Jul 2, 2017 at 22:45

5 Answers 5

30
$\begingroup$

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

$\endgroup$
2
  • 19
    $\begingroup$ Welcome to MathOverflow, professor Scott! $\endgroup$
    – Asaf Karagila
    Jun 27, 2017 at 19:20
  • 3
    $\begingroup$ Reading through the comments by Peter LeFanu Lumsdaine and Bruno Bentzen, I gather that one of the concerns is that the line between "axiom" and "theorem" in MLTT isn't as simple as in classical FOL, so that in particular axiomhood might not be decidable. But I gather that it's still true that the set of theorems is computably enumerable, so as you say, it should still be straightforward to formulate the assertion that 1=0 is not among the set of theorems. $\endgroup$ Jul 2, 2017 at 22:57
21
$\begingroup$

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.

  1. 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 ⟧ᵀ.

  1. 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 ‘⊤’ ()
$\endgroup$
13
$\begingroup$

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.

$\endgroup$
1
9
$\begingroup$

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.

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

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

$\endgroup$
10
  • 2
    $\begingroup$ What Rosser's theorem does is to reduce the hypothesis of $\omega$-consistency to that of mere consistency for the incompleteness to apply. But it's clear from Gödel's original paper that his results are valid with his hypothesis to a variety of systems interpreting enough arithmetic. However, as Peter explained in the comments, these systems are based in FOL, while MLTT is not. What do you mean by MLTT being equivalent to HOL? In which sense? How can this allow to transfer Gödel/Rosser arguments? $\endgroup$
    – godelian
    Jun 28, 2017 at 14:54
  • $\begingroup$ Thank you for such a detailed answer! But I am looking for something more related to MTLL and not HOIL... $\endgroup$ Jun 28, 2017 at 15:40
  • $\begingroup$ @godelian MLTT is equivalent to HOL via the generalized Curry-Howard isomorphism: the one that isomorphically associates dependent types to predicates and terms to proof (of course this holds for intutiontistic HOL, but we could add an axiom that allows to use the excluded middle). I hope this answer the first part of the question. $\endgroup$ Jun 28, 2017 at 16:28
  • 2
    $\begingroup$ If I understand you correctly, the “equivalence” you have in mind is that the types and terms of MLTT are respectively the sentences and derivations of IHOL. One element that breaks this parallel is that the former has inductive types whereas IHOL has no similar counterpart. Now, I don’t know which version of MLTT, the intensional or extensional, the OP has in mind, but, in the case of the latter, there are terms don’t correspond to derivations in IHOL (e.g. $ \lambda x. 1 : Id_{\mathbb{N}}(0,1) \to (\mathbb{N} \to \mathbb{N}) $). [...] $\endgroup$ Jun 29, 2017 at 3:30
  • 2
    $\begingroup$ [...] In either case, we certainly want a general type-theoretic approach to the incompleteness theorems that can work for any type-theoretic framework has no obvious correspondence to a HOL. $\endgroup$ Jun 29, 2017 at 3:30
4
$\begingroup$

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.

$\endgroup$
2
  • 4
    $\begingroup$ Welcome to MathOverflow! $\endgroup$ Jul 8, 2017 at 16:20
  • $\begingroup$ +1 Thanks for pointing out this very nice article of yours, professor Sundholm! I have a question: With respect to your answer to Q2, if my understanding is correct, you are suggesting that MLTT has a derivation of the judgment $t : G$ for an arbitrary term $t$ whose construction will necessarily invoke constructors other than the arithmetical ones, $\mathtt{zero}$ and $\mathtt{succ}$. If this is the case, what I can't comprehend is: in what sense can we still say that MLTT is incomplete? $\endgroup$ Jul 30, 2017 at 7:54

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.