Alternative proof for the undecidability of $A_{TM}$ The proof of the undecidability of $A_{TM}$ in Michael Sipser's textbook* contains the definition of a Turing Machine, which accepts the encoding of a TM, if this TM doesn't accept its own encoding, and rejects it, if it does. If this TM is run on its own encoding, there is problem: it should accept if it doesn't accept and vice versa.

My problem with this proof is that it strongly resembles Russel's paradox. This paradox arises if we define a set, which contains all sets that are not members of themselves. If we ask whether this set contains itself, there is problem: it should contain itself if it doesn't contain itself and vice versa. 

Russels's paradox has been eliminated from axiomatic set theory: in ZFC, it follows from the axioms that such a property doesn't define a valid set. Interestingly enough, in the theory of computation, a similar property defines a valid TM. 

That's why I don't like the proof in Sipser's book. I'd like to emphasize that I know that this proof is perfectly valid, but I'd like to know if there is another proof which follows a different chain of thought, and doesn't define such a TM.



*Sipser, M.: Introduction to the Theory of Computation (2nd ed.), 2006, page 179. On this page, Sipser uses the term halting problem for the language $A_{TM}$. The proper name for this language is acceptance problem, see the footnote on page 188.
There is no paradox. We have made an assumption, namely that the halting problem is solved by some Turing machine, and using it reached a paradox. Hence our assumption must be wrong. In the same way, Russell's paradox is a proof that the collection of all sets not containing themselves is a proper class.

In both cases, the paradox is solved by concluding that some object cannot exist. In the case of Russell's paradox, we can give a description of the object - properties it satisfies - but it doesn't exist as a set. In the same way, the halting problem is definable, but there is no Turing machine that accepts it.

In recursion theory we can breathe life into it by making it an oracle, and consider the implications. Similarly, in set theory we can consider relativized versions of Russell's set (relativized to some set "sub-universe"), though due to the axiom of regularity the result isn't interesting.