5 ms·

Yes, I thought the article was really good until it got to that point. > a halt detector can be trivially repurposed as a program optimizer / theorem-prover /

Yes, I thought the article was really good until it got to that point. > a halt detector can be trivially repurposed as a program optimizer / theorem-prover / bcrypt cracker / chess engine. It's too powerful, so we should expect it to be impossible.) A Turing machine can be trivially repurposed as a bcrypt cracker or chess engine (for the same definition of trivial the author is using), so if it's not intuitive that a computer can do this, then your intuition is wrong. Program optimizers and theorem provers also exist, of course, but in those cases the problems really are undecidable so no Turing machine is guaranteed to work on any given program or theorem.

bubblyworld 1y ago
A solution to the Halting problem can be repurposed as a general-purpose theorem prover. The author is correct. You simply write a program that searches all possible valid proofs till it finds the one you are looking for (or maybe doesn't and runs forever). Then you check whether it halts with your Halting solution - if that returns true, you know that a proof exists, otherwise you know that one doesn't. In other words, you can use undecidability of first-order logic to prove undecidability of the Halting problem if you like, although it's a bit of a chicken-egg thing historically (I believe).
- dmurray 1y ago
  I edited the last part; I meant that the Turing machine from my second paragraph can't do those things, though the Halting machine can.
  - bubblyworld 1y ago
    Right, yeah that makes sense. But I think the author understands that very well.
    - dmurray 1y ago
      Of course he must. But the fact that we're arguing about it (and there's another thread with the same conversation) says that at least, the intent of this part wasn't clear.
- Maxatar 1y ago
  >A solution to the Halting problem can be repurposed as a general-purpose theorem prover. The author is correct. You simply write a program that searches all possible valid proofs till it finds the one you are looking for (or maybe doesn't and runs forever). The author is not correct and it's a common misconception. Simple question for you... let's say I give you a magical black box that can solve the halting problem. Now please use it to prove or disprove the continuum hypothesis (within ZFC). Hopefully you'll come back to me and say the black box shows that the continuum hypothesis can not be proved or disproved (in ZFC). Okay we agree so far, but note that we have established that having a solution to the halting problem can not actually be repurposed as a general purpose theorem prover, since no such proof exists in the first place. Okay you might counter by saying that a solution to the halting problem can be repurposed as a general purpose theorem prover for propositions that either have a proof or don't have a proof, ignore those pesky propositions that are neither provable or unprovable... But then the solution to the halting problem doesn't get you anything... if you're dealing with a proposition that either has a proof or a proof of its negation, you don't need a solution to the halting problem to find it, you are guaranteed to find it eventually by definition. The claim that a black box that solves the halting problem can be used as a general purpose theorem prover is simply untrue and confuses certain concepts together. At best you can claim it gives you a restricted theorem classifier.
  - Tainnor 1y ago
    You're mixing things up. By a "general theorem prover", we typically mean "a program which can decide for every sentence in FOL whether it's valid" (I say FOL, because the situation is even worse for HOL), i.e. a decider for the set of valid FOL sentences. The sentence ZFC -> CH (where ZFC and CH are expanded as needed) is not valid because CH doesn't follow from the ZFC axioms. Neither is ZFC -> not(CH) valid. We know both of these results from proofs specific to this problem, but a general purpose theorem prover would give us both of these results for free. If we had such a tool, mathematics would essentially be "solved" (maybe apart from deciding what questions to ask). But since FOL is undecidable, it can't exist. What you are asking for is a machine that for each pair of formulas A, B (correctly) decides that either A -> B or A -> not(B), but this is impossible for model-theoretic reasons (not all theories are complete) and that has nothing to do with decidability.

bubblyworld 1y ago

A solution to the Halting problem can be repurposed as a general-purpose theorem prover. The author is correct. You simply write a program that searches all possible valid proofs till it finds the one you are looking for (or maybe doesn't and runs forever). Then you check whether it halts with your Halting solution - if that returns true, you know that a proof exists, otherwise you know that one doesn't. In other words, you can use undecidability of first-order logic to prove undecidability of the Halting problem if you like, although it's a bit of a chicken-egg thing historically (I believe).

dmurray 1y ago
I edited the last part; I meant that the Turing machine from my second paragraph can't do those things, though the Halting machine can.
- bubblyworld 1y ago
  Right, yeah that makes sense. But I think the author understands that very well.
  - dmurray 1y ago
    Of course he must. But the fact that we're arguing about it (and there's another thread with the same conversation) says that at least, the intent of this part wasn't clear.
Maxatar 1y ago
>A solution to the Halting problem can be repurposed as a general-purpose theorem prover. The author is correct. You simply write a program that searches all possible valid proofs till it finds the one you are looking for (or maybe doesn't and runs forever). The author is not correct and it's a common misconception. Simple question for you... let's say I give you a magical black box that can solve the halting problem. Now please use it to prove or disprove the continuum hypothesis (within ZFC). Hopefully you'll come back to me and say the black box shows that the continuum hypothesis can not be proved or disproved (in ZFC). Okay we agree so far, but note that we have established that having a solution to the halting problem can not actually be repurposed as a general purpose theorem prover, since no such proof exists in the first place. Okay you might counter by saying that a solution to the halting problem can be repurposed as a general purpose theorem prover for propositions that either have a proof or don't have a proof, ignore those pesky propositions that are neither provable or unprovable... But then the solution to the halting problem doesn't get you anything... if you're dealing with a proposition that either has a proof or a proof of its negation, you don't need a solution to the halting problem to find it, you are guaranteed to find it eventually by definition. The claim that a black box that solves the halting problem can be used as a general purpose theorem prover is simply untrue and confuses certain concepts together. At best you can claim it gives you a restricted theorem classifier.
- Tainnor 1y ago
  You're mixing things up. By a "general theorem prover", we typically mean "a program which can decide for every sentence in FOL whether it's valid" (I say FOL, because the situation is even worse for HOL), i.e. a decider for the set of valid FOL sentences. The sentence ZFC -> CH (where ZFC and CH are expanded as needed) is not valid because CH doesn't follow from the ZFC axioms. Neither is ZFC -> not(CH) valid. We know both of these results from proofs specific to this problem, but a general purpose theorem prover would give us both of these results for free. If we had such a tool, mathematics would essentially be "solved" (maybe apart from deciding what questions to ask). But since FOL is undecidable, it can't exist. What you are asking for is a machine that for each pair of formulas A, B (correctly) decides that either A -> B or A -> not(B), but this is impossible for model-theoretic reasons (not all theories are complete) and that has nothing to do with decidability.