摘要
It was A. N. Prior who introduced the system MIPC in his monograph Time and Modality in 1957, which is of type S5 in the sense of R. A. Bull, i. e. adding the law of excluded middle to it yields S5. Many different modal intuitionistic calculi of type S5 (also in the same sense of Bull )were given by several logicians in recent years. One of the basic prob-
