Thanks for this comment! The idea that only a single Uy can be provable, otherwise we get a contradiction and hence we can prove an arbitrarily high utility has greatly clarified this post for me. I still haven’t quite figured out why the agent can’t use the above proof that those are the only two provable and the fact that agent()==1 gives a higher value to prove that agent()!=2 and then create a contradiction.
Edit: Actually, I think I now understand this. After finding those two proofs, the agent can only conclude that there aren’t any more proofs of the form “agent()=_ implies world()=_”if its reasoning (say PA) is consistent. But it can’t actually prove this!
Thanks for this comment! The idea that only a single Uy can be provable, otherwise we get a contradiction and hence we can prove an arbitrarily high utility has greatly clarified this post for me. I still haven’t quite figured out why the agent can’t use the above proof that those are the only two provable and the fact that agent()==1 gives a higher value to prove that agent()!=2 and then create a contradiction.
Edit: Actually, I think I now understand this. After finding those two proofs, the agent can only conclude that there aren’t any more proofs of the form “agent()=_ implies world()=_”if its reasoning (say PA) is consistent. But it can’t actually prove this!