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 λμ-calculus is also introduced as a computational extraction of CNDS4. It is an extension of both the λμ-calculus and the modal λ-calculus. Subject reduction, confluency, and strong normalization of the modal λμ-calculus are shown. Finally, the computational interpretation of the modal λμ-calculus, especially the computational meaning of the modal possibility operator, is discussed.