efim comments on An Introduction to Löb's Theorem in MIRI Research - LessWrong

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.

Article Navigation

Comments (27)
Tags: math decision_theory udt

Comments (27)

You are viewing a single comment's thread.

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: Kutta 24 March 2015 05:02:07PM *  7 points [-]

Suppose "mathemathics would never prove a contradiction". We can write it out as ¬Provable(⊥). This is logically equivalent to Provable(⊥) → ⊥, and it also implies Provable(Provable(⊥) → ⊥) by the rules of provability. But Löb's theorem expresses ∀ A (Provable(Provable(A) → A) → Provable(A)), which we can instantiate to Provable(Provable(⊥) → ⊥)→ Provable(⊥), and now we can apply modus ponens and our assumption to get a Provable(⊥).

Comment author: Quill_McGee 24 March 2015 05:11:04PM 5 points [-]

Wasn't Löb's theorem ∀ A (Provable(Provable(A) → A) → Provable(A))? So you get Provable(⊥) directly, rather than passing through ⊥ first. This is good, as, of course, ⊥ is always false, even if it is provable.

Comment author: Kutta 24 March 2015 05:14:48PM *  2 points [-]

You're right, I mixed it up. Edited the comment.

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.

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).
Powered by Reddit Powered by Reddit