Possible world semantics underlies many of the applications of modal logic in computer science and philosophy. The standard theory arises from interpreting the semantic definitions in the ordinary meta-theory of informal classical mathematics. Classical modal logics are classical in the sense that all are built on top of ordinary classical logic. Similarly, intuitionistic modal logics are modal logics whose underlying logic is intuitionistic. The cut-elimination theorem (or Gentzen’s Hauptsatz) is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper ”Investigations in Logical Deduction” for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. But they are admissible in it standard sequent calculi for the classical propositional logic, corresponding calculus to the intuitionistic propositional by limiting the right side of the sequents to the maximum of a formula.
