Dan Hernest ; Trifon Trifonov - Modal Functional (Dialectica) Interpretation

lmcs:7132 - Logical Methods in Computer Science, October 25, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:3)2021
Modal Functional (Dialectica) InterpretationArticle

Authors: Dan Hernest ; Trifon Trifonov

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


    Volume: Volume 17, Issue 4
    Published on: October 25, 2021
    Accepted on: September 22, 2021
    Submitted on: January 26, 2021
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03F99, 03H99, 03B45, 68T99, 68V15

    Consultation statistics

    This page has been seen 1037 times.
    This article's PDF has been downloaded 280 times.