Modal Functional (Dialectica) Interpretation

TL;DR

This paper develops a modal Dialectica interpretation adapting light and heavy variants to modal logic, proving soundness for a modal arithmetic based on S4 and S5, and improving translation processes.

Contribution

It introduces a new heavy modal Dialectica interpretation technique that cannot be derived from previous light versions, enhancing the translation process and connecting modal axioms to realizability.

Findings

Soundness of the modal Dialectica interpretation for modal arithmetic based on S4.

The heavy modal Dialectica cannot be simulated within the light version.

Existence of realizers for S5 axioms reduces to the Drinking Principle.

Abstract

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).