A Constructive Presentation for the Modal Connective of Necessity (□)

This work provides a constructive presentation of modal logis in natural deduction style. The modal connective □ is presented in a constructive form, which can be considered as an operational semantics for it. Modal connectives have been recognized as intentional connectives for a long time, but modal logicians have insisted in using extensional techniques to deal with them. In this paper, the modal connective is presented as a higher-order connective defined on top of the object level logical connectives. The simplest version of our system of modal logic with classical negation coincides with the classical modal logic K. The most important modal logics have an elegant presentation in this system. T, S4, S5, D, D4, D5 are presented, without any side effect condition on the structure of the deductions. Most presentations of intuitionistic modal logics fail in giving an intuitionistic interpretation to the modal connective. In general, such interpretations are based on some alien element (for instance, the accessibility relation), which are by no means intuitionistic. In the system described here it is not only possible to present an intuitionistic interpretation of the modal connective □, which takes into account only deducibility issues, but also to give a constructive natural deduction presentation for the □.