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