Timeline for How do we construct the Gödel’s sentence in Martin-Löf type theory?
Current License: CC BY-SA 3.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 8, 2017 at 15:29 | answer | added | Göran Sundholm | timeline score: 4 | |
| Jul 8, 2017 at 3:38 | answer | added | Jason Gross | timeline score: 21 | |
| Jul 4, 2017 at 2:38 | comment | added | fhyve | This question might be relevant cstheory.stackexchange.com/a/37016/13296 | |
| Jul 3, 2017 at 16:35 | comment | added | Emil Jeřábek | @MateoCarmona Please do not swamp the main page with lots of small edits. See meta.mathoverflow.net/questions/599 . | |
| S Jul 3, 2017 at 16:20 | history | suggested | Matthieu FG |
added cat log tag
|
|
| Jul 3, 2017 at 15:56 | review | Suggested edits | |||
| S Jul 3, 2017 at 16:20 | |||||
| Jul 3, 2017 at 0:13 | comment | added | Bruno Bentzen | @TimothyChow Yes, sure. The point I tried to emphasize with my comments is that there are some subtleties specifically concerning the incompleteness theorems for MLTT. So I think that seeing a proof from the type-theoretic perspective would be probably shed light in many aspects of it. Thank you for the links :) | |
| Jul 2, 2017 at 22:45 | comment | added | Timothy Chow | @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 | |
| Jun 28, 2017 at 13:27 | answer | added | Giorgio Mossa | timeline score: 9 | |
| Jun 28, 2017 at 8:37 | comment | added | Peter LeFanu Lumsdaine | @BrunoBentzen: I don’t think open-ended inductive schemas are a big problem — types can still be coded as a set of words over a finite alphabet. But (unlike with the codes of propositions of FOL) this set is a priori only semi-decidable, not decidable. I doubt this would cause any serious problem, but it shows that a direct account of Gödel incompleteness for type theory has to be at least a little different from the standard account for theories of FOL. | |
| Jun 28, 2017 at 6:53 | comment | added | Bruno Bentzen | @CarlMummert Complementing Peter Lumsdaine’s nice comment, I think there are many other complications. MLTT supports the notion of an inductive type, and so its language is “open-ended” in the sense that we can always define new types along with new constants and functions. Consequently, it is not so obvious how to define Gödel numbering for MLTT since its set of well-formed types (propositions) is never finished. I am sure there must exist such a numbering, though. Its formulation is just more involved than in the case of FOL. | |
| Jun 28, 2017 at 6:42 | comment | added | Bruno Bentzen | @PeterLeFanuLumsdaine On the one hand, the fact that MLTT proves (under the proposition-as-types) all theorems of Robinson Arithmetic is a reasonable step forward to a precise notion of “the requirements of the incompleteness theorem” for MLTT. On the other hand, I think one difficulty is to express what exactly “effective axiomatization” means for MLTT: we could certainly recursively enumerate the set of theorems of MLTT, but I can’t see how we could define a Gödel numbering for type theory with inductive types (see my comment to Carl Mummert). | |
| Jun 28, 2017 at 2:22 | answer | added | Valeria | timeline score: 13 | |
| Jun 27, 2017 at 21:17 | comment | added | Peter LeFanu Lumsdaine | @CarlMummert: the essential difference between IZF and MLTT, for this question, is that IZF is a theory in first-order logic, while MLTT is not. There are well-known precise statements of “the requirements of the incompleteness theorem” for theories in FOL. Can you point me to anywhere in the literature that does this for some more general notion of “theory” or “formal system” that covers MLTT? | |
| Jun 27, 2017 at 20:47 | comment | added | მამუკა ჯიბლაძე | Such things easily happen in, say, toposes - e. g. in local homeomorphisms over the circle, the nontrivial double covering is inhabited - in the sense of having global support - but does not have any globally defined elements. I believe one has such situations in various type systems, particularly in HoTT | |
| Jun 27, 2017 at 19:19 | answer | added | Dana S Scott | timeline score: 30 | |
| Jun 27, 2017 at 0:14 | comment | added | Carl Mummert | 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? | |
| Jun 25, 2017 at 17:03 | comment | added | Peter LeFanu Lumsdaine | …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.) | |
| Jun 25, 2017 at 17:01 | comment | added | Peter LeFanu Lumsdaine | 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] | |
| Jun 25, 2017 at 16:57 | comment | added | Peter LeFanu Lumsdaine | 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] | |
| Jun 25, 2017 at 7:44 | history | asked | StudentType | CC BY-SA 3.0 |