3 ms·
Not entirely sure, but it seems if you had a type system that describes every system you may be on your way to disproving the first incompleteness theorem. http
by poof131 12y ago
Not entirely sure, but it seems if you had a type system that describes every system you may be on your way to disproving the first incompleteness theorem. http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_the...
- steveklabnik 12y agoHmmmmmm yes. I can see that. This is why I need to move from 'amateur type theorist' to 'intermediate type theorist.' :)
- dllthomas 12y agoThat certainly tells us that there is no single type system that can describe every correct program, which seems to be the stronger version of Steve's thesis that he was supporting in the immediate parent. A weaker version of his thesis, which could still support his original phrasing in the GGP, would be "for any correct program, there exists a type system in which it can be typed [though we might not be able to find it]." That doesn't seem to be ruled out, and sounds plausible, though I don't know of any specific results on it.