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).
>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.
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.
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 =)
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
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.
Look, I have a masters in mathematical logic (but bailed from my PhD, to my discredit). I know what I'm talking about. You are the one who started all this bickering about what counts as a theorem prover - personally I don't really care what you call it!
As for the stuff about CH, yes, there's nothing we disagree about there. And on non-recursive theories and logics without a sound/complete/effective proof theory, sure, a halting oracle isn't enough.
Do I really have to spell out every edge-case?
No one is asking you to spell out the edge cases, but when you claim that a halting oracle can be used as a general-purpose theorem prover and I point out the edge cases where that won't work, it's pretty egregious to then say that I'm mixing things up, I am misusing standard terminology, etc...
If you claimed every prime number is odd, and I point out that 2 is an even prime number, you don't get to turn around, pull out your credentials, claim I'm mixing things up and bickering around because I am pointing out an exception to your generalization.
The fact is a halting oracle cannot be used as a general-purpose theorem prover. At best it can be used as a way to classify theorems in specific first order theories with recursively enumerable axioms and I even admitted that much in my original response to you.
That some first order theories do not have recursively enumerable axioms and for these theories even an oracle for the halting problem is insufficient to either prove, refute, or classify as independent particular propositions is actually a fascinating topic in and of itself which could have led to a much more engaging conversation than the one you decided to go with by talking about your failed academic career and claiming I'm misinformed, but alas that ship has sailed and at this point and with that I don't think there is much further to discuss here.
Goodness man, go touch some grass. It's just the internet =)
[flagged]
Random ad-hominems don't do much for me, friend, I'm autistic (you'll have to kill my dog or something). Hit me with more logic - despite your odd character attacks I have enjoyed this exchange. Thinking about Turing degrees and nonstandard logics again has been refreshing.
I think I wounded your pride? That wasn't really my intention. I hope you recover soon.
> but that's not a general theorem prover at that point, that's a theorem classifier for a specific formal theory (namely ZFC).
huh, no, it will work just as well for any FOL theory with a recursively enumerable set of axioms, there's nothing specific to ZFC to it.
And even works for some non-recursive theories like the first-order theory of true arithmetic.
The basic idea is that you can determine whether a sentence X is in the theory or not by searching every natural number for counter-examples, and then using your halting oracle to check whether that search terminates or not.
No it won't. You must first fix a specific theory to apply your solver to. It won't work for every arbitrary choice of theory even with recursively enumerable axioms.
Yes it will? This works for any first-order theory with a recursive set of axioms. You are simply searching for proofs of implications from the axioms and using the halting oracle to tell if the search terminates or not. By the compactness theorem this is guaranteed to work.
Of course you have to input the axioms, how would a theorem prover work otherwise?
> By the compactness theorem this is guaranteed to work.
I think you mean completeness, but essentially yes.
In this case I meant compactness - if a statement follows from your (possibly infinite set of) axioms then it follows from a finite subset of them. But you can skin the cat in many ways, yeah (proof theory vs model theory way of looking at it I guess).
First of all, I should have written "recursively enumerable theory" or "theory with decidable axioms". But I think it's clear that I'm referring to things like ZFC, first-order PA or any other similar system.
With that out of the way, it's pretty easy to write a general theorem prover for such theories if you can solve the halting problem.
First define a TM G that takes as input 1. the description of another TM A that decides whether a particular sentence is an axiom of some theory T and 2. a sentence P. We enumerate all syntactically valid proofs with P as the conclusion and check whether all axioms are valid according to A and all inferences are sound. If we find a valid proof, we stop. (G can obviously be built.)
Then define H such that it takes the same inputs as G, and then (using the halting oracle) determines whether G would halt given A and P. If yes, return true, otherwise false.
Then H would be a decider for the language consisting of all pairs T |= P, where T is some recursively enumerable theory.
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.
Right, yeah that makes sense. But I think the author understands that very well.
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.