Given that we’re using PA+n to defeat evil problems, the true modal definition of “action i leads to outcome j” might be something like “there exists a closed formula ϕ such that N⊨ϕ, GL ⊢ϕ→(Ai→Uj), and GL ⊬ϕ→¬Ai”. But that’s an unnecessary complication for this post.
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!
Ah! I’d failed to propagate that somehow.
Given that we’re using PA+n to defeat evil problems, the true modal definition of “action i leads to outcome j” might be something like “there exists a closed formula ϕ such that N⊨ϕ, GL ⊢ϕ→(Ai→Uj), and GL ⊬ϕ→¬Ai”. But that’s an unnecessary complication for this post.
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!