| Summary: | We adapt our light Dialectica interpretation to usual and light modal
formulas (with universal quantification on boolean and natural variables) and
prove it sound for a non-standard modal arithmetic based on Goedel's T and
classical S4. The range of this light modal Dialectica is the usual (non-modal)
classical Arithmetic in all finite types (with booleans); the propositional
kernel of its domain is Boolean and not S4. The `heavy' modal Dialectica
interpretation is a new technique, as it cannot be simulated within our
previous light Dialectica. The synthesized functionals are at least as good as
before, while the translation process is improved. Through our modal
Dialectica, the existence of a realizer for the defining axiom of classical S5
reduces to the Drinking Principle (cf. Smullyan).
|
|---|