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 …