orthonormal 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: orthonormal 24 March 2015 05:20:10PM 1 point [-]

Thanks for asking! I should add another sentence in that paragraph; the key step, as Kutta and Quill noted, is that "not A" is logically equivalent to "if A, then False", and in particular the statement "2+2=5 is not provable" is logically equivalent to "if 2+2=5 were provable, then 2+2=5", and then we can then run Löb's Theorem.