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 :-)
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 :-)