Proof Theory for Extended Belnap–Dunn and Intuitionistic Logics

First, G0-style sequent calculi for extended Belnap-Dunn and intuitionistic logics, including Nelson and Gurevich logics, are introduced. A theorem establishing the equivalence between G0- and G3-style sequent calculi for these logics is then presented, and the cut-elimination theorem for these G0-style calculi is obtained as a result. Next, natural deduction systems with general elimination rules are introduced for these logics, and a full normalization theorem for these natural deduction systems is proved. This proof is achieved using bi-directional translations between the proposed G0-style sequent calculi and the natural deduction systems with general elimination rules.