# Could someone prove they had a halting oracle?

Suppose someone comes to you and claims to have a halting oracle. Is there any way for you to verify the truth or falsity of their claim in finite time? If so, what constraints on the proof process are there? Does the verification have to be interactive? Can you only prove it to a given probabilistic bound?

Update: Henning, below, suggested an oracle $A_F$ that will say "Halt" unless the TM in question can be proved to have infinite run-time by some formal system $F$. He then claimed that one cannot tell this oracle from a true halting oracle. I am not certain of this; I suspect there may be some sequence of questions one can ask this oracle to trip it up in a lie. Can anyone prove or disprove this statement?

-
@anon, it's not an oracle that halts. It's an oracle that (immediately) answers instances of the Halting Problem. – Henning Makholm Sep 12 '11 at 19:22
I expect the answer to this problem to be "no," so a follow-up question: how efficiently can you verify that the halting oracle is correct for programs of length up to $n$ in terms of $n$? – Qiaochu Yuan Sep 12 '11 at 19:41

It's clear that you cannot possibly hope for more than a probabilistic result -- any testing procedure that can pass a true halting oracle after asking it $n$ questions will also pass a random oracle with probability at least $2^{-n}$.
@Peter: +1 for that. But the trouble is, the TM that you construct may take a very long time to run if the number of steps is very large. So what you could do instead, given a number of steps $n$, is to construct a TM which halts if and only if the original TM halts in $n$ steps or fewer. Then just feed this new TM to the oracle. – TonyK Sep 21 '11 at 14:29