Further simplification (which Benja and Marcello worked out): since every modal formula is decidable conditional on ¬□n⊥ for large enough n, you don’t need special axioms for each modal decision problem and decision theory, you just need a strong enough consistency axiom. That’s a pretty nifty optimality result.
(It requires the decidability result above, which currently is an unpublished folk theorem proved in an alternate draft of the modal combat paper, but we’ll see if we can get that included in a nice peer-reviewed citable source.)
Further simplification (which Benja and Marcello worked out): since every modal formula is decidable conditional on ¬□n⊥ for large enough n, you don’t need special axioms for each modal decision problem and decision theory, you just need a strong enough consistency axiom. That’s a pretty nifty optimality result.
(It requires the decidability result above, which currently is an unpublished folk theorem proved in an alternate draft of the modal combat paper, but we’ll see if we can get that included in a nice peer-reviewed citable source.)
Two further notes:
Said folk theorem is in fact shown in Boolos.
Benja verified that the optimality result should work for chicken-playing modal UDT as well as descending-search-order modal UDT.