Classical Natural Deduction for S4 Modal Logic

This paper proposes a natural deduction system CNDS4 for classical S4 modal logic with necessity and possibility modalities. This new system is an extension of Parigot's Classical Natural Deduction with dual-context to formulate S4 modal logic. The modal lambda mu-calculus is also introduced as a computational extraction of CNDS4. It is an extension of both the lambda mu-calculus and the modal lambda-calculus. Subject reduction, confluency, and strong normalization of the modal lambda mu-calculus are shown. Finally, the computational interpretation of the modal lambda mu-calculus, especially the computational meaning of the modal possibility operator, is discussed.