You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

RichardKennaway comments on Open Thread - Aug 24 - Aug 30 - Less Wrong Discussion

7 Post author: Elo 24 August 2015 08:14AM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (318)
Tags: open_thread

Comments (318)

You are viewing a single comment's thread. Show more comments above.

Comment author: RichardKennaway 26 August 2015 09:40:36AM 3 points [-]

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.

Comment author: philh 27 August 2015 09:47:55AM 2 points [-]

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.

Powered by Reddit Powered by Reddit