I have a possibly-stupid question about the proof that access to an arbitration oracle can’t help the verifier. I understand why a single arbitration oracle A can be used to simulate a pair consisting of an arbitration oracle A’ and another oracle satisfying P. But as part of that simulation, the oracle A has access to all the outputs of the oracle A’, and can use them to construct a consistent model satisfying P. Isn’t this slightly different than the actual setting that A would find itself in(trying to imitate a model P), where it would be faced with a verifier using an arbitration oracle A″ it has no access to? I have the sense that this couldn’t be used to falsify that A is implementing P, since A’ and A″ can only differ on the arbitrary answers they give to queries about machines that never halt. But I don’t immediately see how to prove this.
If the falsifying Turing-computable agent has access to the oracle A’ and a different oracle A″, and A’ and A″ give different answers on some Turing machine (which must never halt if A’ and A″ are arbitration oracles), then there is some way to prove that A′≠A′′ by exhibiting this machine.
The thing I’m proving is that, given that the falsifier knows A’ is an arbitration oracle, that doesn’t help it falsify that oracle B satisfies property P. I’m not considering a case where there are two different putative arbitration oracles. In general it seems hard for 2 arbitration oracles to be more helpful than 1 but I’m not sure exactly how to prove this. Maybe it’s possible to use the fact that a single arbitration oracle can find two different arbitration oracles by creating two different models of PA?
The thing I’m proving is that, given that the falsifier knows A’ is an arbitration oracle, that doesn’t help it falsify that oracle B satisfies property P.
Hmm, let me put it this way—here’s how I would (possible incorrectly) summarize the proof: “For a given oracle O with property P, you can’t falsify that O uses only arbitration-oracle levels of hypercomputation, even with access to an arbitration oracle A’. This is because there could be a Turing machine T in the background, with access to an arbitration oracle A, which controls the output of both A’ and O, in such a way that A’ being an arbitration oracle and O having property P cannot be disproved in PA”
I’m wondering whether we can remove the condition that the background Turing machine T controls the output of A’, instead only allowing it to control the output of O, in such a way that “A’ being an arbitration oracle and O having property P” cannot be disproved in PA for all possible arbitration oracles A’. This would be a scenario where there are two possibly-distinct arbitration oracles, the oracle A’ used by the verifier and the oracle A used by the background Turing machine T.
I have a possibly-stupid question about the proof that access to an arbitration oracle can’t help the verifier. I understand why a single arbitration oracle A can be used to simulate a pair consisting of an arbitration oracle A’ and another oracle satisfying P. But as part of that simulation, the oracle A has access to all the outputs of the oracle A’, and can use them to construct a consistent model satisfying P. Isn’t this slightly different than the actual setting that A would find itself in(trying to imitate a model P), where it would be faced with a verifier using an arbitration oracle A″ it has no access to? I have the sense that this couldn’t be used to falsify that A is implementing P, since A’ and A″ can only differ on the arbitrary answers they give to queries about machines that never halt. But I don’t immediately see how to prove this.
If the falsifying Turing-computable agent has access to the oracle A’ and a different oracle A″, and A’ and A″ give different answers on some Turing machine (which must never halt if A’ and A″ are arbitration oracles), then there is some way to prove that A′≠A′′ by exhibiting this machine.
The thing I’m proving is that, given that the falsifier knows A’ is an arbitration oracle, that doesn’t help it falsify that oracle B satisfies property P. I’m not considering a case where there are two different putative arbitration oracles. In general it seems hard for 2 arbitration oracles to be more helpful than 1 but I’m not sure exactly how to prove this. Maybe it’s possible to use the fact that a single arbitration oracle can find two different arbitration oracles by creating two different models of PA?
Hmm, let me put it this way—here’s how I would (possible incorrectly) summarize the proof: “For a given oracle O with property P, you can’t falsify that O uses only arbitration-oracle levels of hypercomputation, even with access to an arbitration oracle A’. This is because there could be a Turing machine T in the background, with access to an arbitration oracle A, which controls the output of both A’ and O, in such a way that A’ being an arbitration oracle and O having property P cannot be disproved in PA”
I’m wondering whether we can remove the condition that the background Turing machine T controls the output of A’, instead only allowing it to control the output of O, in such a way that “A’ being an arbitration oracle and O having property P” cannot be disproved in PA for all possible arbitration oracles A’. This would be a scenario where there are two possibly-distinct arbitration oracles, the oracle A’ used by the verifier and the oracle A used by the background Turing machine T.