blossom comments on An Introduction to Löb's Theorem in MIRI Research - Less Wrong

16 Post author: orthonormal 23 March 2015 10:22PM

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

Comments (27)

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

Comment author: efim 24 March 2015 10:32:20AM *  5 points [-]

I am stuck at part 2.2: "So in particular, if we could prove that mathematics would never prove a contradiction, then in fact mathematics would prove that contradiction"

I've spend 15 minutes on this, but still cannot see relation to löb's theorem. Even though it seems like it should be obvious to attentive reader.

Could anyone please explain or link me to an explanation?

Comment author: [deleted] 24 March 2015 11:29:49AM *  1 point [-]

Unless I have completely got something wrong, it should go like this:

  1. I can't prove a contradiction. I.e. I can't prove false statements.
  2. For all X: If I find a proof of X, X is true. I.e. For all X: L(X)
  3. or all X: X (Löb's Theorem).