A note to clarify for confused readers of the proof. We started out by assuming □(cross→U=−10), and cross. We conclude □(cross→U=10)∨□(cross→U=0) by how the agent works. But the step from there to □⊥ (ie, inconsistency of PA) isn’t entirely spelled out in this post.
Pretty much, that follows from a proof by contradiction. Assume con(PA) ie ¬□⊥, and it happens to be a con(PA) theorem that the agent can’t prove in advance what it will do, ie, ¬□(¬cross). (I can spell this out in more detail if anyone wants) However, combining □(cross→U=−10) and □(cross→U=10) (or the other option) gets you □(¬cross), which, along with ¬□(¬cross), gets you ⊥. So PA isn’t consistent, ie, □⊥.
A note to clarify for confused readers of the proof. We started out by assuming □(cross→U=−10), and cross. We conclude □(cross→U=10)∨□(cross→U=0) by how the agent works. But the step from there to □⊥ (ie, inconsistency of PA) isn’t entirely spelled out in this post.
Pretty much, that follows from a proof by contradiction. Assume con(PA) ie ¬□⊥, and it happens to be a con(PA) theorem that the agent can’t prove in advance what it will do, ie, ¬□(¬cross). (I can spell this out in more detail if anyone wants) However, combining □(cross→U=−10) and □(cross→U=10) (or the other option) gets you □(¬cross), which, along with ¬□(¬cross), gets you ⊥. So PA isn’t consistent, ie, □⊥.