The proofs in question say it is impossible to algorithmically arrive at a Yes-or-No answer to the generalized question, “Does algorithm X have non-trivial property Y for input Z?”, for any specific property Y. Poorly written proof at the bottom. It critically doesn’t say that you can’t have a Yes-or-No-or-Undecidable answer to that question. Introduce an uncertainty factor and the issue falls apart. Thus, you -can- write a Halting Oracle, so long as you’re satisfied that sometimes it won’t be able to say.
For purposes of AI Friendliness—which is certainly a non-trivial property—Rice’s Theorem says we can’t algorithmically prove that an AI—which is an algorithm—is, or is not, friendly, once we manage to define what friendly even is. We can theoretically, however, prove that AI is friendly, not friendly, or undecidably friendly. For our purposes, “not friendly” and “undecidably friendly” are probably equivalent.
For purposes of everything else, nothing at all says that it’s impossible to prove whether or not a specific program will halt given a specific input. “But what about the program in Turing’s diagonalization proof? Does it halt or not?” The input in that case (the Halting Oracle) can’t exist in the first place, as the proof demonstrates.
“But what about this neat program I wrote that halts 25% of the time?” What did you use to generate a random number? Not being aware of your hidden inputs isn’t the same as not having an input. For a given set of inputs, your algorithm halts 100%, or 0%, of the time.
A Halting Oracle that only says “Yes”, “No”, or “Provably Undecidable” hasn’t (to my knowledge and research) been proven to be impossible—and a “Yes”, “No”, or “Maybe” Halting Oracle is quite trivial, as you can throw all cases you can’t figure out an algorithm for into the “Maybe” pile. The proofs do not demonstrate that there are any algorithms which are nondeterministically halting for a given input, nor do they demonstrate that we can’t prove that any given algorithm will or will not halt, nor do they even demonstrate that an algorithm can’t prove that other algorithms will or will not halt—they demonstrate one thing and one thing only, and that is that there is no single algorithm which gives a “Yes” or “No” answer will work on all algorithms for all inputs.
An equivalent-to-Rice’s-Theorem-for-our-very-limited-purposes-proof written like the halting problem proof. A trivial property in this case means it -can- vary by algorithm and input.
Suppose Algorithm Zed determines whether or not Algorithm X has non-trivial property Y for the input Z, returning a boolean value. Take Algorithm ScrewZed, with an input of AlgorithmZed, which has the non-trivial property Y iff its evaluation of AlgorithmZed, given the input of Algorithm ScrewZed with the input of AlgorithmZed, says it doesn’t have non-trivial property Y. Paradox ensues, provided I wrote all this correctly.
A Halting Oracle that only says “Yes”, “No”, or “Provably Undecidable” hasn’t (to my knowledge and research) been proven to be impossible
I think I just proved this. If you can prove something is undecidable, it creates a paradox.
nor do they demonstrate that we can’t prove that any given algorithm will or will not halt
If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases. There are some programs which do not halt, but which it’s impossible to prove they will not halt.
nor do they even demonstrate that an algorithm can’t prove that other algorithms will or will not halt
“If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases.”
That is only true if your proofs work from the same one set of axioms. But in reality you can choose different sets of axioms as needed. So it may be possible to prove of each and every algorithm that it will halt or not, but you cannot make a halt-detection machine that works in all cases, because your proofs use different sets of axioms.
Okay, an attempt to clear up the Halting Problem:
The proofs in question say it is impossible to algorithmically arrive at a Yes-or-No answer to the generalized question, “Does algorithm X have non-trivial property Y for input Z?”, for any specific property Y. Poorly written proof at the bottom. It critically doesn’t say that you can’t have a Yes-or-No-or-Undecidable answer to that question. Introduce an uncertainty factor and the issue falls apart. Thus, you -can- write a Halting Oracle, so long as you’re satisfied that sometimes it won’t be able to say.
For purposes of AI Friendliness—which is certainly a non-trivial property—Rice’s Theorem says we can’t algorithmically prove that an AI—which is an algorithm—is, or is not, friendly, once we manage to define what friendly even is. We can theoretically, however, prove that AI is friendly, not friendly, or undecidably friendly. For our purposes, “not friendly” and “undecidably friendly” are probably equivalent.
For purposes of everything else, nothing at all says that it’s impossible to prove whether or not a specific program will halt given a specific input. “But what about the program in Turing’s diagonalization proof? Does it halt or not?” The input in that case (the Halting Oracle) can’t exist in the first place, as the proof demonstrates.
“But what about this neat program I wrote that halts 25% of the time?” What did you use to generate a random number? Not being aware of your hidden inputs isn’t the same as not having an input. For a given set of inputs, your algorithm halts 100%, or 0%, of the time.
A Halting Oracle that only says “Yes”, “No”, or “Provably Undecidable” hasn’t (to my knowledge and research) been proven to be impossible—and a “Yes”, “No”, or “Maybe” Halting Oracle is quite trivial, as you can throw all cases you can’t figure out an algorithm for into the “Maybe” pile. The proofs do not demonstrate that there are any algorithms which are nondeterministically halting for a given input, nor do they demonstrate that we can’t prove that any given algorithm will or will not halt, nor do they even demonstrate that an algorithm can’t prove that other algorithms will or will not halt—they demonstrate one thing and one thing only, and that is that there is no single algorithm which gives a “Yes” or “No” answer will work on all algorithms for all inputs.
An equivalent-to-Rice’s-Theorem-for-our-very-limited-purposes-proof written like the halting problem proof. A trivial property in this case means it -can- vary by algorithm and input.
Suppose Algorithm Zed determines whether or not Algorithm X has non-trivial property Y for the input Z, returning a boolean value. Take Algorithm ScrewZed, with an input of AlgorithmZed, which has the non-trivial property Y iff its evaluation of AlgorithmZed, given the input of Algorithm ScrewZed with the input of AlgorithmZed, says it doesn’t have non-trivial property Y. Paradox ensues, provided I wrote all this correctly.
I think I just proved this. If you can prove something is undecidable, it creates a paradox.
If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases. There are some programs which do not halt, but which it’s impossible to prove they will not halt.
But not for all cases, see above.
“If you could prove any algorithm will halt or not halt, then you can easily make a halt-detection machine that works in all cases.”
That is only true if your proofs work from the same one set of axioms. But in reality you can choose different sets of axioms as needed. So it may be possible to prove of each and every algorithm that it will halt or not, but you cannot make a halt-detection machine that works in all cases, because your proofs use different sets of axioms.