Benya comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All

[Benya]

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

[Eliezer Yudkowsky]

Heh. Nice!