A cut-free sequent calculus for the bi-intuitionistic logic 2Int

arXiv2009.14787MaRDI QIDQ6350253FDOQ6350253

Publication date: 23 September 2020

Abstract: The purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int. Calculi for this logic represent a kind of bilateralist reasoning, since they do not only internalize processes of verification or provability but also the dual processes in terms of falsification or what is called dual provability. A normal form theorem for a natural deduction calculus of 2Int has already been stated, in this paper I want to prove a cut-elimination theorem for SC2Int, i.e. if successful, this would extend the results existing so far.

This page was built for publication: A cut-free sequent calculus for the bi-intuitionistic logic 2Int

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6350253)