Abstract In this paper, we investigate the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an ‘actuality’ operator among the connectives. This logic was initially considered by L. Humberstone, and, more recently, also by S. Niki and H. Omori to present a possible application of intuitionism to empirical discourse. Niki and Omori’s idea to consider the notion of actuality based on intuitionistic logic was presented, among other things, using Gentzen sequents. Unfortunately, their proof system is not cut-free. In this paper, we define another proof system for Niki and Omori’s logic, namely a hypersequent calculus, and present a proof of cut-elimination for it.
Fabio De Martin Polo (Thu,) studied this question.