My main question, which I didn’t see an answer to on my first read, is: If the agent proves that action a leads to the goal G being achieved, are there any conditions under which this implies that the goal actually is achieved? The procrastination paradox shows that this isn’t true in general. Is there a class of sentences (e.g., all Π1 sentences, though I don’t expect that to be true in this case) such that if PA⋆⊢φ then N⊨φ? In other words, do we have some guarantee that we do better at actually achieving G than an agent which uses the system BAD:=PA+Con(BAD)?
A more technical point: Given that you claim that Theorem 3.2 (reflectively coherent quantified belief) follows “trivially” from Theorem 2.4, you presumably mean Theorem 2.4 to state that PA⋆⊢∀x.□┌φ(¯¯¯x)┐→φ(x), rather than PA⋆⊢∀x.□┌φ┐→φ. (Even if you consider φ to implicitly contain an occurrence of x, it is essential that in □┌φ(¯¯¯x)┐ the free variable is replaced by the numeral corresponding to the outer value of x.)
This is very interesting!
My main question, which I didn’t see an answer to on my first read, is: If the agent proves that action a leads to the goal G being achieved, are there any conditions under which this implies that the goal actually is achieved? The procrastination paradox shows that this isn’t true in general. Is there a class of sentences (e.g., all Π1 sentences, though I don’t expect that to be true in this case) such that if PA⋆⊢φ then N⊨φ? In other words, do we have some guarantee that we do better at actually achieving G than an agent which uses the system BAD:=PA+Con(BAD)?
A more technical point: Given that you claim that Theorem 3.2 (reflectively coherent quantified belief) follows “trivially” from Theorem 2.4, you presumably mean Theorem 2.4 to state that PA⋆⊢∀x.□┌φ(¯¯¯x)┐→φ(x), rather than PA⋆⊢∀x.□┌φ┐→φ. (Even if you consider φ to implicitly contain an occurrence of x, it is essential that in □┌φ(¯¯¯x)┐ the free variable is replaced by the numeral corresponding to the outer value of x.)