Natural Deduction for the Sheffer Stroke and Peirce's Arrow (And Any Other Truth-Functional Connective)

TL;DR

This paper demonstrates how to develop sound and complete natural deduction systems for all classical truth-functional connectives, including Sheffer stroke and Peirce's arrow, using axiomatization methods for finite-valued logics.

Contribution

It introduces a systematic approach to axiomatize and derive natural deduction rules for all classical connectives, including NAND and NOR, with simple additional rules for completeness.

Findings

Sound and complete natural deduction systems for Sheffer stroke and Peirce's arrow.

Additional rules are needed for single-conclusion systems to achieve completeness.

Intuitionistic versions of these connectives are obtainable by omitting certain rules.

Abstract

Methods available for the axiomatization of arbitrary finite-valued logics can be applied to obtain sound and complete intelim rules for all truth-functional connectives of classical logic including the Sheffer stroke (NAND) and Peirce's arrow (NOR). The restriction to a single conclusion in standard systems of natural deduction requires the introduction of additional rules to make the resulting systems complete; these rules are nevertheless still simple and correspond straightforwardly to the classical absurdity rule. Omitting these rules results in systems for intuitionistic versions of the connectives in question.