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.
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.