Natural deduction for dual-intuitionistic logic (Q694491)

The paper is dedicated to studying the dual-intuitionistic logic. The natural deduction system NDJ, which is a dual counterpart of the Gentzen system NJ, is constructed. The duality is proven in Theorem 3.2. It is also observed in Theorem 2.3 that NDJ is equivalent to the system LDJ, introduced by \textit{I. Urbas} [Notre Dame J. Formal Logic 37, No. 3, 440--451 (1996; Zbl 0869.03008)]. It is also observed that NDJ enjoys the dual deduction theorem. In Section 4, the duality between NDJ and NJ is extended to the systems NDK and NK.