Thanks, I read the proof [1] again a lot more carefully last night, and really failed to formalize my point.
I tried to reason about it in different ways. Such as, for case 1, considering Z(Z) halts. I don't think it's unreasonable to say that H(Z,Z) could in fact return true. It could read the code for Z, determine that Z(Z) will loop since H(Z,Z) would return false, return true, and then Z(Z) would halt since H(Z,Z) returned true. No immediate contradiction.
Problem is that doesn't completely eliminate the contradiction, it just introduces another one. Even if Z(Z) halts and H(Z,Z) returns false, you could argue backwards and say that the only way for Z(Z) to halt is if H(Z,Z) returns true, but H(Z,Z) can't return two different results.
Part of me still doesn't like the negator program. Too many contradictions. Apparently there are constructive proofs for the halting problem too, which I don't understand yet, so the rabbit hole continues.
> Such as, for case 1, considering Z(Z) halts. I don't think it's unreasonable to say that H(Z,Z) could in fact return true. It could read the code for Z, determine that Z(Z) will loop since H(Z,Z) would return false, return true, and then Z(Z) would halt since H(Z,Z) returned true. No immediate contradiction.
This doesn't make sense. You said in the same case both that "Z(Z) halts" and "Z(Z) will loop" and then "Z(Z) would halt". So there is a contradiction here.
One assumption that you may not realize without the necessary background is that (a) "Z" is fixed in any particular case, we don't consider counterfactual "Z"; and similarly (b) "Z(Z)" must either always halt or always not halt, by the relevant definition of "program".
Thanks for the response. I was trying to illustrate why my argument doesn't work, but you did a much better job at that.
I may have found what I've been looking for in a related topic called Oracle machines for the halting problem. Part of its definition is that it can't solve problem for machines equivalent to itself, which, I believe, would exclude Z-type programs from the domain.
To put my plea into some formal jargon, "Just because the halting problem is undecidable doesn't mean oracles Turing machines for the halting problem don't exist." Kind of a simple and obvious point in hindsight, but I'm happy with it.
I tried to reason about it in different ways. Such as, for case 1, considering Z(Z) halts. I don't think it's unreasonable to say that H(Z,Z) could in fact return true. It could read the code for Z, determine that Z(Z) will loop since H(Z,Z) would return false, return true, and then Z(Z) would halt since H(Z,Z) returned true. No immediate contradiction.
Problem is that doesn't completely eliminate the contradiction, it just introduces another one. Even if Z(Z) halts and H(Z,Z) returns false, you could argue backwards and say that the only way for Z(Z) to halt is if H(Z,Z) returns true, but H(Z,Z) can't return two different results.
Part of me still doesn't like the negator program. Too many contradictions. Apparently there are constructive proofs for the halting problem too, which I don't understand yet, so the rabbit hole continues.
Thanks again for engaging.
[1]: https://www.comp.nus.edu.sg/~cs5234/FAQ/halt.html