This is a linkpost for https://www.overleaf.com/read/dnbvdxmxzcjv
I would like to expand this paper to include how the theory MP + \kappa > n handles the procrastination paradox and similar Lobian tests. Are the results of these tests known for theories PA + n?
I may be misinterpreting the question, but the Lobstacle doesn't apply to an agent using PA+N+1 building an agent that will use PA+N, and you can't make the procrastination paradox with that finite descending chain of formal systems. Is that what you meant?