How can we construct a TM with a Halt1 Oracle that decides if a TM halts on all inputs?

Question

Can we construct an explicit Turing Machine with a Halt1 oracle that decides if a standard Turing Machine halts on all inputs?

By a Halt1 oracle I mean that we have the ability to decide if Turing Machines with a Halting oracle halts or not.

Answer 1

I think that I have an answer to this, putting together my question helped me clarify things enough to come up with this idea

def X(T : TM0):
   for n = 0 and up:
      if !Halt0('T(n)')
        return

Now if we ask Halt1('X(T)') we should get an answer

• yes => T diverges on some input
• no => T halts on all inputs

Does this all make sense logically?