Relating Modal Polymorphism to PA with soundness

post by IAFF-User-169 (Imported-IAFF-User-169) · 2015-08-01T14:57:34.000Z · LW · GW · 2 comments

This is a link post for https://www.overleaf.com/read/dnbvdxmxzcjv

2 comments

Comments sorted by top scores.

comment by IAFF-User-169 (Imported-IAFF-User-169) · 2015-08-09T14:29:44.000Z · LW(p) · GW(p)

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?

Replies from: orthonormal
↑ comment by orthonormal · 2015-08-20T04:13:25.000Z · LW(p) · GW(p)

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?