Yeah, that sounds good! Of course, by the Kripke levels argument, it’s sufficient to consider ϕ’s of the form ¬□n⊥. And we might want to have a separate notion of ”i leads to j at level n”, which we can actually implement in a finite modal formula. This seems to suggest a version of modal UDT that tries to prove things in PA, then if that has ambiguous counterfactuals (i.e., it can’t prove Ai→Uj for any j) we try PA+1 and so on up to some finite n; then we can hope these versions of UDT approximate optimality according to your revised version of ”i leads to j” as n→∞. Worth working out!
Yeah, that sounds good! Of course, by the Kripke levels argument, it’s sufficient to consider ϕ’s of the form ¬□n⊥. And we might want to have a separate notion of ”i leads to j at level n”, which we can actually implement in a finite modal formula. This seems to suggest a version of modal UDT that tries to prove things in PA, then if that has ambiguous counterfactuals (i.e., it can’t prove Ai→Uj for any j) we try PA+1 and so on up to some finite n; then we can hope these versions of UDT approximate optimality according to your revised version of ”i leads to j” as n→∞. Worth working out!