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, pp. 108-9.

Perhaps you would find worthwhile the variant on this proof structure used in Aho and Ullman's Foundations of Computer Science, 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.

        alt text http://cs.smith.edu/%7Eorourke/MathOverflow/HaltingDiagram.jpg

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, pp. 108-9.

Perhaps you would find worthwhile the variant on this proof structure used in Aho and Ullman's Foundations of Computer Science, 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.

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, pp. 108-9.

Perhaps you would find worthwhile the variant on this proof structure used in Aho and Ullman's Foundations of Computer Science, 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.

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, pp. 108-9.

Perhaps you would find worthwhile the variant on this proof structure used in Aho and Ullman's Foundations of Computer Science, 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.

        alt text http://cs.smith.edu/%7Eorourke/MathOverflow/HaltingDiagram.jpg