4 ms·
With today's knowledge, Gödel's theorem should be regarded as a corollary of the impossibility to solve the halting problem. In my opinion, this is also how it
by dhy 6y ago
With today's knowledge, Gödel's theorem should be regarded as a corollary of the impossibility to solve the halting problem.
In my opinion, this is also how it should be taught in order to convey the explanation for its truth in the most straightforward way.
After that, one may of course also note that in the old days, without a good theory of computation, one had to resort to such hacks as Gödel numbers.
A good explanation including all the finer points can be found here: https://www.scottaaronson.com/blog/?p=710 https://www.scottaaronson.com/blog/?p=710
- ProfHewitt 6y agoYes, this is the way to correctly prove "incompleteness", i.e that there are preferentially undecidable propositions in powerful theories of computer science. See the following for a proof: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- ProfHewitt 6y agoOf course, I meant to say "inferentially undecidable" instead of "preferentially undecidable". Being inferentially undecidable means that it is not the case that for every proposition, there is either a proof of the proposition or its negation. Inferential undecidablity implies "incompleteness" in the sense that it is not the case that every true proposition can be proved.
- ProfHewitt 6y agoScott Aaronson's post is very interesting. Unfortunately, Scott's proofs in the above blog post do not work for strongly-typed foundations of Computer Science. For more information, see the following: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003