My question is:
Is there a simple construction similar to Turing's 'liar' program that shows that Turing machines plus a halting oracle cannot decide if a given Turing machine halts on all inputs.
When I talk about the liar program I am referring to the standard proof that a Turing machine can't determine the halting of all other Turing machines, since case analysis on the following leads to contradictions
def Liar(T): if Halts('T(T)'): loop() else: return
I can see that having a Halting oracle would allow me to determine if a Turing machine halts on any finite set of inputs (We would just run it all in order).
If we call regular Turing machines level 0, we can call Turing machines plus the halting oracle level 1. I have seen that the proof using the Liar program works just the same to show that level 1 machines have their own Halting problem which is undecidable for them.