AF - The consistent guessing problem is easier than the halting problem by Jessica Taylor

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: The consistent guessing problem is easier than the halting problem, published by Jessica Taylor on May 20, 2024 on The AI Alignment Forum.
The halting problem is the problem of taking as input a Turing machine M, returning true if it halts, false if it doesn't halt. This is known to be uncomputable. The consistent guessing problem (named by Scott Aaronson) is the problem of taking as input a Turing machine M (which either returns a Boolean or never halts), and returning true or false; if M ever returns true, the oracle's answer must be true, and likewise for false. This is also known to be uncomputable.
Scott Aaronson inquires as to whether the consistent guessing problem is strictly easier than the halting problem. This would mean there is no Turing machine that, when given access to a consistent guessing oracle, solves the halting problem, no matter which consistent guessing oracle (of which there are many) it has access too. As prior work, Andrew Drucker has written a paper describing a proof of this, although I find the proof hard to understand and have not checked it independently.
In this post, I will prove this fact in a way that I at least find easier to understand. (Note that the other direction, that a Turing machine with access to a halting oracle can be a consistent guessing oracle, is trivial.)
First I will show that a Turing machine with access to a halting oracle cannot in general determine whether another machine with access to a halting oracle will halt. Suppose M(O, N) is a Turing machine that returns true if N(O) halts, false otherwise, when O is a halting oracle. Let T(O) be a machine that runs M(O, T), halting if it returns false, running forever if it returns true. Now M(O, T) must be its own negation, a contradiction.
In particular, this implies that the problem of deciding whether a Turing machine with access to a halting oracle halts cannot be a Σ01 statement in the arithmetic hierarchy, since these statements can be decided by a machine with access to a halting oracle.
Now consider the problem of deciding whether a Turing machine with access to a consistent guessing oracle halts for all possible consistent guessing oracles. If this is a Σ01 statement, then consistent guessing oracles must be strictly weaker than halting oracles.
Since, if there were a reliable way to derive a halting oracle from a consistent guessing oracle, then any machine with access to a halting oracle can be translated to one making use of a consistent guessing oracle, that halts for all consistent guessing oracles if and only if the original halts when given access to a halting oracle. That would make the problem of deciding whether a Turing machine with access to a halting oracle halts a Σ01 statement, which we have shown to be impossible.
What remains to be shown is that the problem of deciding whether a Turing machine with access to a consistent guessing oracle halts for all consistent guessing oracles, is a Σ01 statement.
To do this, I will construct a recursively enumerable propositional theory T that depends on the Turing machine. Let M be a Turing machine that takes an oracle as input (where an oracle maps encodings of Turing machines to Booleans). Add to the T the following propositional variables:
ON for each Turing machine encoding N, representing the oracle's answer about this machine.
H, representing that M(O) halts.
Rs for each possible state s of the Turing machine, where the state includes the head state and the state of the tape, representing that s is reached by the machine's execution.
Clearly, these variables are recursively enumerable and can be computably mapped to the natural numbers.
We introduce the following axiom schemas:
(a) For any machine N that halts and returns true, ON.
(b) For any machine N that halts and returns false, ON.
(c) For any ...