4 ms·

Sure, we can choose to work in a set of axioms that says that there exists an oracle that can solve the Halting problem. But the fact that such systems don't c

by btilly 1y ago

Sure, we can choose to work in a set of axioms that says that there exists an oracle that can solve the Halting problem. But the fact that such systems don't create contradictions emphatically *DOES NOT* demonstrate the constructive existence of such an oracle. Doubly not given that in various usual constructivist systems, it is easily provable that nothing that exists can serve as such an oracle.

zozbot234 1y ago
> emphatically DOES NOT demonstrate the constructive existence of such an oracle Of course, but it shows that you can assume that such an oracle exists whenever you are working under additional conditions where the existence of such a "special case" oracle makes sense to you, even though you can't show its existence in the general case. This outlook generalizes to all non-constructive existence statements (and disjunctive statements, as appropriate). It's emphatically not the same as constructive existence, but it can nonetheless be useful.
- btilly 1y ago
  That's like asserting the existence of a bank account in my name with a billion dollars in it that I know nothing about. I won't ever be able to find a contradiction from that claim, because I have no way to find that bank account if it exists. But that argument also won't convince me that the bank account exists.
  - zozbot234 1y ago
    That argument ought to convince you that there's a mere "possible world" where that bank account turns out to exist. Sometimes we are implicitly interested in these special-cased "possible worlds", even though they'll involve conditions that we aren't quite sure about. Non-constructive existence is nothing more than a handy way of talking about such things, compared to the constructively correct "it's not the case that the existence of X is always falsified".
    - btilly 1y ago
      It would be weird for a constructivist to be interested in a possible world that they don't believe exists. Theoretically possible? Sure. But the kinds of questions that lead you there are generally in opposition to the kinds of principles that lead someone to prefer constructivism.
drdeca 1y ago
If such a system proved that the answer to some decidable question was x, when the actual answer was y, then the system would prove a contradiction. If the system doesn’t prove a contradiction, then that situation doesn’t happen, so you can trust its answers to decidable questions. If the only questions you accept as meaningful are the decidable ones, then you can trust its answers for all the questions you accept as meaningful and for which it has answers. Also, “provable that nothing that exists can serve as such an oracle” seems pretty presumptive about what things can exist? Shouldn’t that be more like, “nothing which can be given in such-and-such way (essentially, no computable procedure) can be such an oracle”? Why treat it as axiomatic that nothing that isn’t Turing-computable can exist? It seems unlikely that any finite physical object can compute any deterministic non-Turing-computable function (because it seems like state spaces for bounded regions of space have bounded dimension), but that’s not something that should be a priori, I think. I guess it wouldn’t really be verifiable if such a machine did exist, because we would have no way to confirm that it never errs? Ah, wait, no, maybe using the MIP* = RE result, maybe we could in principle use that to test it?
- btilly 1y ago
  You're literally talking about how I should regard the hypothetical answers that might be produced by something that I think doesn't exist. There's a pretty clear case of putting the cart before the horse here. On being presumptive about what things can exist, that's the whole point of constructivism. Things only exist when you can construct them. We start with things that everyone accepts, like the natural numbers. We add to that all of the mathematical entities that can be constructed from those things. This provides us with a closed and countable universe of possible mathematical entities. We have a pretty clear notion of what it means for something in this universe to exist. We cannot be convinced of the existence of anything that is outside of the universe without making extra philosophical assumptions. Philosophical assumptions of exactly the kind that constructivists do not like. This constructible universe includes a model of computation that fits Turing machines. But it does not contain the ability to describe or run any procedure that can't fit onto a Turing machine. Therefore an oracle to decide the Halting problem does not exist within the constructible universe. And so your ability to imagine such an oracle, won't convince a constructivist to accept its existence.

by btilly 1y ago

zozbot234 1y ago

> emphatically DOES NOT demonstrate the constructive existence of such an oracle Of course, but it shows that you can assume that such an oracle exists whenever you are working under additional conditions where the existence of such a "special case" oracle makes sense to you, even though you can't show its existence in the general case. This outlook generalizes to all non-constructive existence statements (and disjunctive statements, as appropriate). It's emphatically not the same as constructive existence, but it can nonetheless be useful.

btilly 1y ago
That's like asserting the existence of a bank account in my name with a billion dollars in it that I know nothing about. I won't ever be able to find a contradiction from that claim, because I have no way to find that bank account if it exists. But that argument also won't convince me that the bank account exists.
- zozbot234 1y ago
  That argument ought to convince you that there's a mere "possible world" where that bank account turns out to exist. Sometimes we are implicitly interested in these special-cased "possible worlds", even though they'll involve conditions that we aren't quite sure about. Non-constructive existence is nothing more than a handy way of talking about such things, compared to the constructively correct "it's not the case that the existence of X is always falsified".
  - btilly 1y ago
    It would be weird for a constructivist to be interested in a possible world that they don't believe exists. Theoretically possible? Sure. But the kinds of questions that lead you there are generally in opposition to the kinds of principles that lead someone to prefer constructivism.

drdeca 1y ago

If such a system proved that the answer to some decidable question was x, when the actual answer was y, then the system would prove a contradiction. If the system doesn’t prove a contradiction, then that situation doesn’t happen, so you can trust its answers to decidable questions. If the only questions you accept as meaningful are the decidable ones, then you can trust its answers for all the questions you accept as meaningful and for which it has answers. Also, “provable that nothing that exists can serve as such an oracle” seems pretty presumptive about what things can exist? Shouldn’t that be more like, “nothing which can be given in such-and-such way (essentially, no computable procedure) can be such an oracle”? Why treat it as axiomatic that nothing that isn’t Turing-computable can exist? It seems unlikely that any finite physical object can compute any deterministic non-Turing-computable function (because it seems like state spaces for bounded regions of space have bounded dimension), but that’s not something that should be a priori, I think. I guess it wouldn’t really be verifiable if such a machine did exist, because we would have no way to confirm that it never errs? Ah, wait, no, maybe using the MIP* = RE result, maybe we could in principle use that to test it?

btilly 1y ago
You're literally talking about how I should regard the hypothetical answers that might be produced by something that I think doesn't exist. There's a pretty clear case of putting the cart before the horse here. On being presumptive about what things can exist, that's the whole point of constructivism. Things only exist when you can construct them. We start with things that everyone accepts, like the natural numbers. We add to that all of the mathematical entities that can be constructed from those things. This provides us with a closed and countable universe of possible mathematical entities. We have a pretty clear notion of what it means for something in this universe to exist. We cannot be convinced of the existence of anything that is outside of the universe without making extra philosophical assumptions. Philosophical assumptions of exactly the kind that constructivists do not like. This constructible universe includes a model of computation that fits Turing machines. But it does not contain the ability to describe or run any procedure that can't fit onto a Turing machine. Therefore an oracle to decide the Halting problem does not exist within the constructible universe. And so your ability to imagine such an oracle, won't convince a constructivist to accept its existence.