Re: Linz's proofs.

On 7/03/24 17:16, Ben Bacarisse wrote:

immibis <news@immibis.com> writes:
 

On 7/03/24 12:32, Ben Bacarisse wrote:

The students I taught seemed to have no problem with this sort of case
analysis.  But the "assume H does X" argument lead to lots of "but H1
could be better" arguments.

>
They aren't satisfied with "we can do the exact same thing with H1 to prove
that H1 doesn't work either"?

 In the vast majority of cases, yes, but even then there is a logical
problem with going down that route -- there is no H so there can't be an
H1 that does better.  Once this objection is properly examined, it turns
out to be the argument I ended up preferring anyway.  H isn't a halt
decider, it's just any old TM and we show it can't be halt decider for
one reason or another.
 

Unless your students are extremely pedantic... maybe they are... I don't see what's illogical with:
"I think H is a halt decider."
"But it doesn't: see this proof."
"Oh. Well, even though H isn't a halt decider, how do we know there isn't a program H1 which is a halt decider?"
"The proof would still work for H1, or H2, or any other program you think is a halt decider."