Interesting! Looking quickly over the argument, what it seems to be saying is this (someone please correct me if I’m misunderstanding it):
We already know that anyone with a solution to an NP problem can convince us of this in P time. (This is obvious for some NP problems e.g. propositional satisfiability, but surprising for others e.g. traveling salesman.)
Surprisingly, a variant of this extends to all PSPACE problems, if the verification procedure is allowed to be an interactive dialogue and if we are satisfied with an exponentially small probability of error. This applies even to problems like chess, via the application of nontrivial (but still polynomial time) transformations.
But it’s not jumping out at me how to extend something like this to incomputable problems. Do you have an approach in mind?
… but surprising for others e.g. traveling salesman.
A “yes” answer to the decision version of TSP (“is there a path shorter than x?”) is straightforwardly demonstrable: just specify the path. A “no” answer is not demonstrable (short of interactive provers): TSP is in NP, not coNP. And an answer to the optimization version of TSP (“find the shortest path”) is also not demonstrable (short of interactive provers): it’s FP^NP-complete, which is stronger than NP. So I don’t see any surprises there.
Alas, no. Perhaps it is impossible for someone who has a halting oracle to convince someone without a halting oracle that they have a halting oracle, even in universes whose physics allows halting oracles.
Interesting! Looking quickly over the argument, what it seems to be saying is this (someone please correct me if I’m misunderstanding it):
We already know that anyone with a solution to an NP problem can convince us of this in P time. (This is obvious for some NP problems e.g. propositional satisfiability, but surprising for others e.g. traveling salesman.)
Surprisingly, a variant of this extends to all PSPACE problems, if the verification procedure is allowed to be an interactive dialogue and if we are satisfied with an exponentially small probability of error. This applies even to problems like chess, via the application of nontrivial (but still polynomial time) transformations.
But it’s not jumping out at me how to extend something like this to incomputable problems. Do you have an approach in mind?
A “yes” answer to the decision version of TSP (“is there a path shorter than x?”) is straightforwardly demonstrable: just specify the path. A “no” answer is not demonstrable (short of interactive provers): TSP is in NP, not coNP. And an answer to the optimization version of TSP (“find the shortest path”) is also not demonstrable (short of interactive provers): it’s FP^NP-complete, which is stronger than NP. So I don’t see any surprises there.
Alas, no. Perhaps it is impossible for someone who has a halting oracle to convince someone without a halting oracle that they have a halting oracle, even in universes whose physics allows halting oracles.