We introduce a dual-context style sequent calculus which is complete with respect to Kripke semantics where implication is interpreted as strict implication in the modal lic K. The cut-elimination theorem for this calculus is proved by a variant of Gentzen's method.
|Number of pages||6|
|Journal||Mathematical Logic Quarterly|
|Publication status||Published - 2002 Aug 21|
- Dual-context sequent calculus
- Kripke semantics
- Strict implication
ASJC Scopus subject areas