If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.
I'm very confused about something related to the Halting Problem. I discussed this on the IRC with some people, but I couldn't get across what I meant very well. So I wrote up something a bit longer and a bit more formal.
The gist of it is, the halting problem lets us prove that, for a specific counter example, there can not exist any proof that it halts or not. A proof that it does or does not halt, causes a paradox.
But if it's true that there doesn't exist a proof that it halts, then it will run forever searching for one. Therefore I've proved that the program will not halt. Therefore a proof that it doesn't halt does exist (this one), and it will eventually find it. Creating a paradox.
Just calling the problem undecidable doesn't actually solve anything. If you can prove it's undecidable, it creates the same paradox. If no Turing machine can know whether or not a program halts, and we are also Turing machines, then we can't know either.
I guess the answer to this point is that when constructing the proof that H(FL, FL) loops forever, we assume that H can't be wrong. So we are working in an extended set of axioms: the program enumerates proofs given some set of axioms T, and the English-language proof in the tumblr post uses the axiom s... (read more)