I've read the definition for Rice's Theorem, here's the one from Wikipedia:
In computability theory, Rice's theorem states that all non-trivial, semantic properties of programs are undecidable.
However, I have a problem with this proof, made clear (hopefully) in the paragraphs following.
This proof goes like this:
if we had an oracle for deciding these properties of program behavior, we would be able to use it to solve the Halting Problem, but the Halting Problem is undecidable, so an oracle for deciding these properties cannot exist either.
However, as far as I know, the impossibility of the Halting Program only occurs if the program checking whether something halts or not is trying to prove the hypothetical
does_it_halt(a, i) wrong by using self-referencing tricks. But, in this proof, the oracle that is trying to decide the property is not trying to do that. So, it should be able to do its job without solving the Halting Problem.
I had some hope at the beginning that this proof may be wrong, but since it is apparently the "classical" proof for proving Rice's Theorem, I must be missing something. What is it that I am missing ?