Benja comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All - Less Wrong

23 Post author: orthonormal 06 September 2012 04:23PM

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

Comments (45)

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

Comment author: orthonormal 06 September 2012 05:07:00PM *  3 points [-]

Proof that a Löbian cycle works out (hat tip, Eliezer and co.):

|- □A -> B

|- □B -> A

then

|- □(□A->B)

|- □□A->□B

|- □□A->A

|- □(□□A->A)

|- □□□A->□A

|- □A->□□A

|- □□□A->□□A

(apply Löb)

|- □□A

|- A

Comment author: Benja 06 September 2012 10:01:09PM *  10 points [-]

How about just,

(simple facts about PA:)

|- □(A ∧ B) -> (□A ∧ □B)

(apply the assumptions:)

|- □(A ∧ B) -> (B ∧ A)

|- □(A ∧ B) -> (A ∧ B)

(apply Löb:)

|- A ∧ B

Comment author: Eliezer_Yudkowsky 06 September 2012 10:46:25PM 2 points [-]

Heh. Nice!