Note: I may be over my head here in math logic world:
For procrastination paradox:
There seems to be a desire to formalize
T proves G ⇒ G, which messes with completeness. Why not straight up try to formalize:
T proves G at time t ⇒ T proves G at time t+1 for all t > 0
That way:
G ⇒ button gets pressed at time some time X and wasn’t pressed at X-1
However, If T proves G at X-1, it must also prove G at X, for all X > 1 therefore it won’t press the button, unless X = 1.
Basically instead of reasoning of whether proving something makes it true, reason whether proving something at some point leads to re-proving it again at another point or just formalizing the very intuition that makes us understand the paradox.
A system that generically infers “phi with t replaced by t+1” from “phi is provable” is obviously inconsistent (consider phi to be the sentence “there exists t such that t=0”).
You might be able to set something up where a system can infer this for G specifically, but I’m not sure how this is supposed to get you around the procrastination paradox: Say G is “exists t. ButtonPressedAt(t) and not ButtonPressedAt(t-1)”, and that there is a parent agent which will take the first action it considers where it can prove that taking the action implies G. Say that there is an action which creates a child using the same proof system, and that the parent considers building the child, and that it can show that the child will take actions only if they provably imply G. The parent concludes that, if it builds the child, it will either press the button or G will be provable. In the latter case, G will be true at t+1, which means that in the latter case, “exists t+1. ButtonPressedAt(t+1) and not ButtonPressedAt(t).” But this implies G (assuming we start at t=1, to allay concerns about whether t-1 exists), and so the parent procrastinates.
That said, you can indeed build a system that leverages the fact that the child is making proofs at a different timestep in order to deal with the procrastintaion paradox: this is one of the ideas behind Benja’s “parametric polymorphism” (Section 4.2 of this paper). Parametric polymorphism is only a partial solution, and it still has a number of limitations, but following the general idea (of exploiting the fact that parent and child are in different timesteps) does lead to interesting places :-)
Note: I may be over my head here in math logic world:
For procrastination paradox:
There seems to be a desire to formalize
T proves G ⇒ G, which messes with completeness. Why not straight up try to formalize:
T proves G at time t ⇒ T proves G at time t+1 for all t > 0
That way: G ⇒ button gets pressed at time some time X and wasn’t pressed at X-1
However, If T proves G at X-1, it must also prove G at X, for all X > 1 therefore it won’t press the button, unless X = 1.
Basically instead of reasoning of whether proving something makes it true, reason whether proving something at some point leads to re-proving it again at another point or just formalizing the very intuition that makes us understand the paradox.
An interesting idea :-)
A system that generically infers “phi with t replaced by t+1” from “phi is provable” is obviously inconsistent (consider phi to be the sentence “there exists t such that t=0”).
You might be able to set something up where a system can infer this for G specifically, but I’m not sure how this is supposed to get you around the procrastination paradox: Say G is “exists t. ButtonPressedAt(t) and not ButtonPressedAt(t-1)”, and that there is a parent agent which will take the first action it considers where it can prove that taking the action implies G. Say that there is an action which creates a child using the same proof system, and that the parent considers building the child, and that it can show that the child will take actions only if they provably imply G. The parent concludes that, if it builds the child, it will either press the button or G will be provable. In the latter case, G will be true at t+1, which means that in the latter case, “exists t+1. ButtonPressedAt(t+1) and not ButtonPressedAt(t).” But this implies G (assuming we start at t=1, to allay concerns about whether t-1 exists), and so the parent procrastinates.
That said, you can indeed build a system that leverages the fact that the child is making proofs at a different timestep in order to deal with the procrastintaion paradox: this is one of the ideas behind Benja’s “parametric polymorphism” (Section 4.2 of this paper). Parametric polymorphism is only a partial solution, and it still has a number of limitations, but following the general idea (of exploiting the fact that parent and child are in different timesteps) does lead to interesting places :-)