Therefore a proof that it doesn’t halt does exist (this one), and it will eventually find it.
Gödel’s incompleteness bites here. What theory is your halt-testing machine H searching for a proof within? H can only find termination proofs that are derivable from the axioms of that theory. What theory is your proof that H(FL,FL) does not terminate expressed in? I believe it will necessarily not be the same one.
To expand on this - check_if_proof_proves_x_halts will be working using a certain set of axioms and derivation rules. When you prove that H(FL, FL) doesn’t halt, you also use the assumption that check_if_proof_proves_x_halts will definitely return the true answer, which is an assumption that check_if_proof_proves_x_halts doesn’t have as an axiom and can’t prove. (And the same for ..._x_doesnt_halt.) So H can’t use your proof. When it calls check_if_proof_proves_x_doesnt_halt on your proof, that function returns “false” because your proof uses an axiom that that function doesn’t believe in.
I’m not super confident about this stuff, but I think this is broadly what’s going on.
Gödel’s incompleteness bites here. What theory is your halt-testing machine H searching for a proof within? H can only find termination proofs that are derivable from the axioms of that theory. What theory is your proof that H(FL,FL) does not terminate expressed in? I believe it will necessarily not be the same one.
To expand on this -
check_if_proof_proves_x_haltswill be working using a certain set of axioms and derivation rules. When you prove thatH(FL, FL)doesn’t halt, you also use the assumption thatcheck_if_proof_proves_x_haltswill definitely return the true answer, which is an assumption thatcheck_if_proof_proves_x_haltsdoesn’t have as an axiom and can’t prove. (And the same for..._x_doesnt_halt.) SoHcan’t use your proof. When it callscheck_if_proof_proves_x_doesnt_halton your proof, that function returns “false” because your proof uses an axiom that that function doesn’t believe in.I’m not super confident about this stuff, but I think this is broadly what’s going on.