5 ms·

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 syst

by 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.
- zozbot234 1y ago
  You can think that something doesn't exist in the general case, while still allowing that it might exist in unspecified narrow cases where additional constraints could apply. For example, there might be algorithms that can decide the halting problem for some non-Turing complete class of programs. Being able to talk in full generality about how such special cases might work is the whole point of non-constructive reasoning. It's "non-constructive" in that it states "I'm not going to construct this just yet".
  - btilly 1y ago
    Well yes. We can certainly make a function that acts something like that oracle in some special cases. But my point was to give an example of something that cannot be constructively created. The oracle that I described cannot exist within the universe of constructable things.
- drdeca 1y ago
  > Things only exist when you can construct them. This is exactly what I’m saying is presumptive! If constructivism is to earn the merit of being less presumptive by virtue of not assuming the existence of various things, it should also not assume the non-existence of those things. Which, I think many visions of constructivism do earn this merit, but not your description of it.
  - btilly 1y ago
    So having a different philosophy from you makes me presumptive? What makes you presume that you have any business telling someone with different beliefs from you, what is OK to believe? You may believe in the existence of whatever you like. Whether that be numbers that cannot be specified, or invisible pink unicorns. I'll be over in the corner saying that your belief does not compel me to agree with you on the question of what exists. Not when your belief follows from formalism, which explicitly abandons any pretense of meaningfulness to its abstract symbol manipulation.
    - 1y ago

by drdeca 1y ago

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.

zozbot234 1y ago
You can think that something doesn't exist in the general case, while still allowing that it might exist in unspecified narrow cases where additional constraints could apply. For example, there might be algorithms that can decide the halting problem for some non-Turing complete class of programs. Being able to talk in full generality about how such special cases might work is the whole point of non-constructive reasoning. It's "non-constructive" in that it states "I'm not going to construct this just yet".
- btilly 1y ago
  Well yes. We can certainly make a function that acts something like that oracle in some special cases. But my point was to give an example of something that cannot be constructively created. The oracle that I described cannot exist within the universe of constructable things.
drdeca 1y ago
> Things only exist when you can construct them. This is exactly what I’m saying is presumptive! If constructivism is to earn the merit of being less presumptive by virtue of not assuming the existence of various things, it should also not assume the non-existence of those things. Which, I think many visions of constructivism do earn this merit, but not your description of it.
- btilly 1y ago
  So having a different philosophy from you makes me presumptive? What makes you presume that you have any business telling someone with different beliefs from you, what is OK to believe? You may believe in the existence of whatever you like. Whether that be numbers that cannot be specified, or invisible pink unicorns. I'll be over in the corner saying that your belief does not compel me to agree with you on the question of what exists. Not when your belief follows from formalism, which explicitly abandons any pretense of meaningfulness to its abstract symbol manipulation.
  - 1y ago