Alternative First-order Constructive Logics

Gentzen-style sequent calculi are introduced for certain alternative first-order constructive logics that feature both intuitionistic and paraconsistent negations. These first-order constructive logics were developed by Niki and Omori to enhance Nelson’s constructive paraconsistent four-valued logic N4 and Wansing’s constructive connexive four-valued logic C. For the proposed Gentzen-style sequent calculi, theorems on embedding, cut-elimination, Craig interpolation, and Kripke completeness are established. Additionally, some constructive properties, such as the disjunction property and the constructible falsity property, are derived from these calculi.