New Comment
2 comments, sorted by Click to highlight new comments since: Today at 7:59 AM

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?