Although I recognize this is a matter of taste, I do not find it unnatural to fix a TM. I find the proof by contradiction relatively concrete. In that proof structure, the start is: Suppose there exists, for the purposes of contradiction, a TM $T_1$ that determines if any other halts. Then we could construct a TM $T_2$ that accomplishes the impossible. So $T_1$ cannot exist. This is the proof in Hopcroft and Ullman's _[Formal Languages and their Relation to Automata][1]_, pp. 108-9. Perhaps you would find worthwhile the variant on this proof structure used in Aho and Ullman's _[Foundations of Computer Science][2]_, p. 750. Here they do not use TMs, but rather just programs, calling $T_1$ the "decider" program, reaching the conclusion that no such decider can exist via a "complementer" program. One can present a few wiring diagrams using the decider and complementer programs as black boxes to make the contradiction clear. Not-halting can be equated with infinite loops. If your utter novices are programmers, this approach can be more convincing than an indexed diagonal argument. [1]: http://dl.acm.org/citation.cfm?id=1096945 [2]: http://infolab.stanford.edu/~ullman/focs.html