# Gurkenglas comments on Decision Theory

• The agent has been con­structed such that Prov­able(“5 is the best pos­si­ble ac­tion”) im­plies that 5 is the best (only!) pos­si­ble ac­tion. Then by Löb’s the­o­rem, 5 is the only pos­si­ble ac­tion. It can­not also be si­mul­ta­neously con­structed such that Prov­able(“10 is the best pos­si­ble ac­tion”) im­plies that 10 is the only pos­si­ble ac­tion, be­cause then it would also fol­low that 10 is the only pos­si­ble ac­tion. That’s not just our proof sys­tem be­ing in­con­sis­tent, that’s false!

• (There was a LaTeX er­ror in my com­ment, which made it to­tally illeg­ible. But I think you man­aged to re­solve my con­fu­sion any­way).

I see! It’s not prov­able that Prov­able() im­plies . It seems like it should be prov­able, but the ob­vi­ous ar­gu­ment re­lies on the as­sump­tion that, if * is prov­able, then it’s not also prov­able that - in other words, that the proof sys­tem is con­sis­tent! Which may be true, but is not prov­able.

The asym­me­try be­tween 5 and 10 is that, to choose 5, we only need a proof that 5 is op­ti­mal, but to choose 10, we need to not find a proof that 5 is op­ti­mal. Which seems eas­ier than find­ing a proof that 10 is op­ti­mal, but is not prov­ably eas­ier.