We can also construct an example where PA⊢ϕ→ψ with a short proof and PA also proves ϕ→¬ψ, but any such proof is much longer. We only need to put a bound on the proof length in A’s proof search. Then, the argument that A()=1∧U()≠0 proves its own consistency still works, and is rather short: O(logn) as the proof length bound n increases. However, there cannot be a proof of A()=1→U()=10 within A’s proof length bound, since if it found one it would immediately take action 1. In this case PA can still prove that A()=1→U()=10 simply by running the agent, but this argument shows that any such proof must be long.
We can also construct an example where PA⊢ϕ→ψ with a short proof and PA also proves ϕ→¬ψ, but any such proof is much longer. We only need to put a bound on the proof length in A’s proof search. Then, the argument that A()=1∧U()≠0 proves its own consistency still works, and is rather short: O(logn) as the proof length bound n increases. However, there cannot be a proof of A()=1→U()=10 within A’s proof length bound, since if it found one it would immediately take action 1. In this case PA can still prove that A()=1→U()=10 simply by running the agent, but this argument shows that any such proof must be long.