An Agda Implementation of the Modal Logic S4.2: First Investigations

This paper is the first step towards a new mechanization of modal logics strongly oriented to constructive mathematics. We introduce ES4.2, a sequent calculus for the logic S4.2, that extends S4 with the axiom ♦□𝜙 → □♦𝜙 and emerges as the underlying logic in different fields. We build on previous investigations where formulas are equipped with a position, i.e. set of uninterpreted tokens used to manage modal information. The calculus is designed to enjoy strong proof-theoretical properties, such as a direct syntactical proof of cut-elimination, which in turn yields the consistency of the system and the subformula property. We implement in Agda the system and we present the implementation of the proof of the Cut-Elimination Theorem as a work in progress.