I thought it was a bit “cheating” to give the programs access to an oracle that the formal system couldn’t decide (but that thing with the finite number of options is quite elegant and satisfying).
That paper about who long you need to search is super interesting! I wasn’t sure who long you would need to search if you disallowed infinite search.
Ah, makes sense this was discovered before. Thanks! I have added a link to your comment at the top of the post.
The chicken rule mitigated spurious counterfactuals for the original proof-based UDT back in 2011. But in a provability modal logic formulation the chicken rule is not needed (there is now an even nicer decision rule formulation in provability logic). And the result goes through without an oracle using a variant of Löb’s theorem for provability with proofs of bounded length.
Oh, very nice!
I thought it was a bit “cheating” to give the programs access to an oracle that the formal system couldn’t decide (but that thing with the finite number of options is quite elegant and satisfying).
That paper about who long you need to search is super interesting! I wasn’t sure who long you would need to search if you disallowed infinite search.