4 ms·

>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 p

>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
Tainnor has basically already said what I would have (independence phenomena is an orthogonal concern, general purpose theorem prover does not mean "can prove X or not-X for any first-order sentence X"). > 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. You don't know what situation you are in ahead of time, this is the point (my proposed algorithm terminates on all inputs, including independent statements). If you had a black box machine that could tell you whether a statement was independent or not then that would be just as useful, yes. But that's also an undecidable problem. Yet a halting oracle can be used to compute it! The author is correct, you are simply misusing or misunderstanding standard terminology =)
- Maxatar 1y ago
  Terminology isn't the most important detail here and there's no real point dwelling on it, what's important are the actual fundamental concepts at play. An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independent of ZFC and that's true and something I explicitly pointed out in my reply to you, but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC). ZFC is not the end-all be-all of first order logic and it's certainly not even a particularly good choice of formal model for dealing with Turing Machines. Your halting oracle will not be able to do the same kind of theorem classification for other formal theories, namely those that do not have a recursively enumerable set of axioms. The most obvious example of such theories are second order theories, but even if you restrict yourself to first order theories, you have examples of such theories like True Arithmetic where your halting oracle won't be able to classify propositions since even though it's a first order theory proofs can't be enumerated in the same way that proofs can be enumerated in ZFC (or other first order theories with recursively enumerable axioms): https://en.wikipedia.org/wiki/True_arithmetic https://en.wikipedia.org/wiki/True_arithmetic In general if the basis of your argument depends on nitpicking terminology, then that's a good sign you might not actually understand the fundamental concepts at play and are instead just regurgitating terms that you've heard from other people which is what I suspect you're doing here.

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

Tainnor has basically already said what I would have (independence phenomena is an orthogonal concern, general purpose theorem prover does not mean "can prove X or not-X for any first-order sentence X"). > 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. You don't know what situation you are in ahead of time, this is the point (my proposed algorithm terminates on all inputs, including independent statements). If you had a black box machine that could tell you whether a statement was independent or not then that would be just as useful, yes. But that's also an undecidable problem. Yet a halting oracle can be used to compute it! The author is correct, you are simply misusing or misunderstanding standard terminology =)

Maxatar 1y ago
Terminology isn't the most important detail here and there's no real point dwelling on it, what's important are the actual fundamental concepts at play. An oracle for the halting problem can not be used to prove or disprove the Continuum Hypothesis within ZFC. No amount of bickering over terminology can change that fact. You can claim that such an oracle can be used to show that the Continuum Hypothesis is independent of ZFC and that's true and something I explicitly pointed out in my reply to you, but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC). ZFC is not the end-all be-all of first order logic and it's certainly not even a particularly good choice of formal model for dealing with Turing Machines. Your halting oracle will not be able to do the same kind of theorem classification for other formal theories, namely those that do not have a recursively enumerable set of axioms. The most obvious example of such theories are second order theories, but even if you restrict yourself to first order theories, you have examples of such theories like True Arithmetic where your halting oracle won't be able to classify propositions since even though it's a first order theory proofs can't be enumerated in the same way that proofs can be enumerated in ZFC (or other first order theories with recursively enumerable axioms): https://en.wikipedia.org/wiki/True_arithmetic https://en.wikipedia.org/wiki/True_arithmetic In general if the basis of your argument depends on nitpicking terminology, then that's a good sign you might not actually understand the fundamental concepts at play and are instead just regurgitating terms that you've heard from other people which is what I suspect you're doing here.