Constructive modal logics. I (Q750417)

The main system considered is intuitionistic predicate logic plus Gentzen-type rules for K-modalities: \(X,A\to B/\square X,\diamondsuit A\to \diamondsuit B;\) \(X,A\to /\square X,\diamondsuit A\to\) and \(X\to A/\square X\to \square A.\) Cut elimination and completeness theorems for Kripke semantics are proved. The difference from other systems in literature is for example the lack of distributivity \(\diamondsuit (A\vee B)\to \diamondsuit A\vee \diamondsuit B.\) Additional axioms are considered. They are said to be useful for proving properties of concurrent programs.