Dual-Context Sequent Calculus and Strict Implication
Kentaro Kikuchi · Mathematical logic quarterly · 2002
We introduce a dual-context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut-elimination theorem for this calculus is proved by a variant of Gentzen's method.