Wei_Dai comments on Decision Theories, Part 3.75: Hang On, I Think This Works After All - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (45)
I think that works too. Call these proof systems PA+ and PA- and the FairBots using them FB+ and FB-. PA can prove that any theorem of PA is also a theorem of PA+ and PA-. So PA can prove:
and similarly for the other half of the Löbian circle. So FB+(FB-)=C and FB-(FB+)=C are theorems of PA and hence theorems of PA- and PA+.