Constructive Embedding from Extensions of Logics of Strict Implication into Modal Logics

Dyckhoff and Negri (Arch Math Logic 51:71-92 (2012), [8]) give a constructive proof of Godel-Mckinsey-Tarski embedding from intermediate logics to modal logics via labelled sequent calculi. Then, they regard amonotonicity of atomic propositions in intuitionistic logic as an initial sequent, i.e., an axiom. However, we regard the monotonicity as an additional inference rule and employ a modified translation sending an atomic variable P to P & P to generalize their result to an embedding from extensions of Corsi's F of logic of strict implication to normal extensions of modal logics K. In this process, we provide a G3-style labelled sequent calculi for extensions of F and show that our calculi admit the cut rule and enjoy soundness and completeness for Kripke semantics.