That works if you can guess S, or some S' that is more powerful than S. But might there be a formal system that couldn't be guessed this way? My first thought was to construct a parameterized system somehow, S(x) where S(x) can prove that S(y) halts when a trick like this is used; but that can be defeated by simply iterating over systems, if you figure out the parameterization. But suppose you tried a bunch of formal logics this way, and the oracle passed them all; how could you ever be sure you hadn't missed one? What about a proof system plus a tricky corner case detection heuristic that happens to cover all your programs?