Timeline for The true reason for the incompleteness of formal systems
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 5 at 9:58 | comment | added | Nathan Chappell | @provocateur I've added a section on infinite types. Let me know what you think! | |
| Jun 5 at 9:58 | history | edited | Nathan Chappell | CC BY-SA 4.0 |
Stuff on infinite types.
|
| Jun 5 at 1:49 | comment | added | provocateur | Well I guess the question is whether it helps us make sense of the idea that incompleteness is a consequence of 'the fact that the formation of ever higher types can be continued into the transfinite', which was OP's question. I guess on the diagnosis you are considering incompleteness is due to the fact that the type of the diagonal lemma is inhabited. At first glance these seem to be quite different diagnoses, though I am open to being convinced otherwise. | |
| Jun 4 at 22:39 | comment | added | Nathan Chappell | @provocateur $Y$ not? | |
| Jun 4 at 22:37 | history | edited | Nathan Chappell | CC BY-SA 4.0 |
added 598 characters in body
|
| Jun 4 at 22:28 | comment | added | provocateur | Fair enough, I guess it is true that in strong typing systems, the type corresponding to the diagonalization lemma will be inhabited, while in weak systems it is not. From the Curry Howard Correspondence, this just follows fairly directly from the fact that in weak theories the diagonalization lemma is not provable, while in sufficiently strong theories it is. I guess the question is what we gain from viewing all this in terms of the Curry Howard Correspondence and type inhabitation, rather than just from the point of view of first order theories. | |
| Jun 4 at 7:50 | comment | added | Nathan Chappell | @provocateur Are you familiar with Curry-Howard? The idea of propositions as types comes from that. It's untypable in the simply typed lambda calculus (and some extensions that essentially introduce other "logical connectives" than ->). It's typable in other systems. I don't know about other's making the claim, I guess I didn't even consider it to be a claim and more of an observation. I'll put up an explanation a little later, although we're going to need to use $\beta$ reduction... | |
| Jun 4 at 7:12 | comment | added | provocateur | I'd love for this to be a precise and rigorous claim, but right now I just don't see it. I don't know what it means to say both that Y is untypeable and that its type is the diagonalization lemma. Has this claim been made in the literature by anyone? | |
| Jun 3 at 7:46 | history | edited | Nathan Chappell | CC BY-SA 4.0 |
Additional explanation, remove superflous narrative
|
| Jun 3 at 6:49 | comment | added | Nathan Chappell | @provocateur The type of the Y combinator is the diagonalization lemma, the combinator Y itself is the proof of the lemma. That's not really a claim, that's the interpretation of the Curry-Howard isomorphism... What I'm claiming is about what Goedel might have meant and showing the relationship to type theory in case it's of interest. | |
| Jun 2 at 23:24 | comment | added | provocateur | So is the claim is that there is a connection between the Y combinator and the diagonalization lemma (the theorem you quote from Kunen)? If so, what is the precise connection? For example, does using the untypeability of the Y combinator give us an easy proof of the diagonalization lemma? That is not obvious to me. Or is the connection supposed to be something else? | |
| Jun 2 at 14:12 | comment | added | Nathan Chappell | @provocateur I added a new section, please let me know if it needs to be further elaborated. | |
| Jun 2 at 14:12 | history | edited | Nathan Chappell | CC BY-SA 4.0 |
Clarify relationship of Y and Incompleteness
|
| Jun 2 at 0:22 | comment | added | provocateur | The exact connection between the untypability of Y and Godel Incompleteness is not clear to me at all. | |
| Jun 1 at 17:17 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
fixed a link to a comment
|
| Jun 1 at 17:06 | history | edited | LSpice | CC BY-SA 4.0 |
Links to comments, inclined commutative diagram, and other tidying
|
| S Jun 1 at 17:02 | review | First answers | |||
| Jun 1 at 20:15 | |||||
| S Jun 1 at 17:02 | history | edited | Nathan Chappell | CC BY-SA 4.0 |
typos
|
| S Jun 1 at 12:19 | review | First answers | |||
| Jun 1 at 12:26 | |||||
| S Jun 1 at 12:19 | history | answered | Nathan Chappell | CC BY-SA 4.0 |