Unified Natural Deduction for Logics of Strong Negation

This study introduces Gentzen-style natural deduction systems for Gurevich logic, Nelson logic, intuitionistic logic, classical logic, and modal logic. Gurevich logic is an extended constructive three-valued logic obtained from intuitionistic logic by adding strong negation, and Nelson logic is the intuitionistic-negation-less fragment of Gurevich logic. The proposed natural deduction systems are constructed in a modular manner based on primitive rules for negation, that is, rules of explosion, of negation introduction, and of excluded middle. Theorems for equivalence between these natural deduction systems and the corresponding previously proposed cut-free Gentzen-style sequent calculi are proved. Moreover, normalization theorems for the proposed natural deduction systems are proved.