Timeline for How do we construct the Gödel’s sentence in Martin-Löf type theory?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 29, 2017 at 9:42 | comment | added | Bruno Bentzen | I would say 'yes', since we can still map derivations in IHOL to terms in extensional MLTT, it is just not an one-to-one correspondence anymore. (Although I am pretty sure there is a sense in which each derivation in extensional MLTT can be seen as a derivation in IHOL.) | |
| Jun 29, 2017 at 7:49 | comment | added | Giorgio Mossa | @BrunoBentzen thank you for pointing out my mistake. Still it should be possible to interpret HOL in extensional MLTT, shouldn't it? If that's the case one can translate Rosser's theorem inside MLTT. Nevertheless I'll try to edit a little bit the answer to address directly the problem in MLTT framework. Thank you again. :) | |
| Jun 29, 2017 at 3:30 | comment | added | Bruno Bentzen | [...] 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. | |
| Jun 29, 2017 at 3:30 | comment | added | Bruno Bentzen | 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}) $). [...] | |
| Jun 28, 2017 at 16:33 | comment | added | Giorgio Mossa | @StudentType MTLL is HOL up the Curry-Howard isomorphism: types of MTLL are propositions HOL and terms are proofs. I've chosen to talk about HOL because its language is closer to the one in which the incompleteness theorems are applied but if you replace type for proposition and term for proof you should be able to see that the answer above should provide exactly what you have asked for. | |
| Jun 28, 2017 at 16:29 | comment | added | Giorgio Mossa | @godelian Does this satisfy your doubts? | |
| Jun 28, 2017 at 16:29 | comment | added | Giorgio Mossa | @godelian On the second part: HOL from a purely syntactic point of view, i.e. seen just a deductive system, has the same strength of a first-order system hence once you interpret Robinson's Arithmetic inside this system (hopefully with the help of some additional axiom) you can basically carry out the proof of Rosser's theorem inside HOL/MTLL. | |
| Jun 28, 2017 at 16:28 | comment | added | Giorgio Mossa | @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. | |
| Jun 28, 2017 at 15:40 | comment | added | StudentType | Thank you for such a detailed answer! But I am looking for something more related to MTLL and not HOIL... | |
| Jun 28, 2017 at 14:54 | comment | added | godelian | 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? | |
| Jun 28, 2017 at 13:27 | history | answered | Giorgio Mossa | CC BY-SA 3.0 |