The point is that the behavior of H is paradoxical. We can prove that it can’t return true or false without contradiction. But if that’s provable, that also creates a contradiction, since H can prove it to.
More precisely, H will encounter a proof that the question is undecidable. It then runs into the following two if statements:
if check_if_proof_proves_x_halts(proof, x, i)
if check_if_proof_proves_x_doesnt_halt(proof, x, i)
Both return “false”, so H moves into the next iteration of the while loop. H will generate undecidability proofs, but as implemented it will merely discard them and continue searching. Since such proofs do not cause H to halt, and since there are no proofs that the program halts or does not, then H will run forever.
As people have been saying, if H can make this argument it is inconsistent and does not work properly (i.e. it does not return True or False in the correct situations.)
I did overlook the definition of H. Apologies.
More precisely, H will encounter a proof that the question is undecidable. It then runs into the following two if statements:
if check_if_proof_proves_x_halts(proof, x, i)
if check_if_proof_proves_x_doesnt_halt(proof, x, i)
Both return “false”, so H moves into the next iteration of the while loop. H will generate undecidability proofs, but as implemented it will merely discard them and continue searching. Since such proofs do not cause H to halt, and since there are no proofs that the program halts or does not, then H will run forever.
If it is undecidable, then that means no proof exists (that
Hwill or will not halt.)If no proof exists, then
Hwill loop forever searching for one.Therefore undecidability implies
Hwill run forever. You’ve just proved this.Therefore a proof exists that
Hwill run forever (that one), andHwill eventually find it.Paradox...
As people have been saying, if H can make this argument it is inconsistent and does not work properly (i.e. it does not return True or False in the correct situations.)