4 ms·

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

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.
- bubblyworld 1y ago
  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?
  - Maxatar 1y ago
    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.
    - bubblyworld 1y ago
      [flagged]
      - Maxatar 1y ago

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.

bubblyworld 1y ago
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?
- Maxatar 1y ago
  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.
  - bubblyworld 1y ago
    [flagged]
    - Maxatar 1y ago