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

TL;DR

This paper introduces a new cut-free sequent calculus for bi-intuitionistic logic 2Int, providing proofs of admissibility for structural rules and aiming to establish a cut-elimination theorem.

Contribution

It presents SC2Int, a novel sequent calculus for 2Int, and proves its cut-elimination, advancing the proof-theoretic understanding of bi-intuitionistic logic.

Findings

Proved admissibility of structural rules in SC2Int

Established a cut-elimination theorem for the calculus

Extended previous results on natural deduction calculus for 2Int

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.