If I am allowed to use only exponentially more computing power than you (are far cry from a halting oracle), then I can produce outputs that you cannot distinguish from a halting oracle.
Consider the following program: Take some program P as input, and search over all proofs of length at most N, in some formal system that can describe the behaviour of arbitrary programs (ie first order PA) for a proof that P either does or does not halt. If you find a proof one way or the other, return that answer. Otherwise, return HALT.
This will return the correct answer for all programs of which halt in less than (some constant multiple of) N, since actually running the program until it halts provides a proof of halting. But it also gives the correct answer for a lot of other cases: for example there is a very short proof that “While true print 1”.
Now, if I am allowed exponentially more computing power than you, then I can run this program with N equal to the number of computations that you are allowed to expend. In particular, any program that you query me on, I will either answer correctly, or give a false answer that you won’t be able to call me out on.
The Kolmogorov complexity of an uncomputable sequence is infinite, so Solomonoff induction assigns it a probability of zero, but there’s always a computable number with less than epsilon error, so would this ever actually matter?
Can you re-phrase this please? I don’t understand what you are asking.
What if I give you a program that enumerates all proofs under PA and halts if it ever finds proof for a contradiction? There is no proof under PA that this program doesn’t halt, so your fake oracle will return HALT, and then I will have reasonable belief that your oracle is fake. Also, in this part:
This will return the correct answer for all programs of length less than (some constant multiple of) N, since actually running the program until it halts provides a proof of halting.
Did you mean to write “for all programs that halt in less than (some constant multiple of) N steps”, because what you wrote doesn’t make sense.
Did you mean to write “for all programs that halt in less than (some constant multiple of) N steps”, because what you wrote doesn’t make sense.
Yes. Edited.
What if I give you a program that enumerates all proofs under PA and halts if it ever finds proof for a contradiction? There is no proof under PA that this program doesn’t halt, so your fake oracle will return HALT, and then I will have reasonable belief that your oracle is fake.
That’s cool. Can you do something similar if I change my program to output NOT-HALT when it doesn’t find a proof?
Can you do something similar if I change my program to output NOT-HALT when it doesn’t find a proof?
Consider a program that enumerates all proofs under PA of length up to N^c for some c. If it finds a contradiction, it loops forever, otherwise it halts. I have reasonable belief that it halts, but your fake oracle can’t prove that it does using a proof of length at most N, if c is sufficiently large (see
On the length of proofs of finitistic consistency statements in first order theories).
Or here’s another way that doesn’t depend on that result. Define program A as follows: Enumerate all proofs under PA up to length N. If it finds a proof for “program A halts”, then it loops forever, otherwise it halts. If PA is consistent, then it must be that A halts but there’s no proof for it under PA of length N or less.
If I am allowed to use only exponentially more computing power than you (are far cry from a halting oracle), then I can produce outputs that you cannot distinguish from a halting oracle.
Consider the following program: Take some program P as input, and search over all proofs of length at most N, in some formal system that can describe the behaviour of arbitrary programs (ie first order PA) for a proof that P either does or does not halt. If you find a proof one way or the other, return that answer. Otherwise, return HALT.
This will return the correct answer for all programs of which halt in less than (some constant multiple of) N, since actually running the program until it halts provides a proof of halting. But it also gives the correct answer for a lot of other cases: for example there is a very short proof that “While true print 1”.
Now, if I am allowed exponentially more computing power than you, then I can run this program with N equal to the number of computations that you are allowed to expend. In particular, any program that you query me on, I will either answer correctly, or give a false answer that you won’t be able to call me out on.
Can you re-phrase this please? I don’t understand what you are asking.
What if I give you a program that enumerates all proofs under PA and halts if it ever finds proof for a contradiction? There is no proof under PA that this program doesn’t halt, so your fake oracle will return HALT, and then I will have reasonable belief that your oracle is fake. Also, in this part:
Did you mean to write “for all programs that halt in less than (some constant multiple of) N steps”, because what you wrote doesn’t make sense.
Yes. Edited.
That’s cool. Can you do something similar if I change my program to output NOT-HALT when it doesn’t find a proof?
Consider a program that enumerates all proofs under PA of length up to N^c for some c. If it finds a contradiction, it loops forever, otherwise it halts. I have reasonable belief that it halts, but your fake oracle can’t prove that it does using a proof of length at most N, if c is sufficiently large (see On the length of proofs of finitistic consistency statements in first order theories).
Or here’s another way that doesn’t depend on that result. Define program A as follows: Enumerate all proofs under PA up to length N. If it finds a proof for “program A halts”, then it loops forever, otherwise it halts. If PA is consistent, then it must be that A halts but there’s no proof for it under PA of length N or less.
Okay, I concede. I recognize when I’ve been diagonalized.