On multiple conclusion deductions in classical logic

Abstract

Kneale observed that Gentzen's calculus of natural deductions NK for classical logic is not symmetric and has unnecessarily complicated hypothetical inference rules. Kneale proposed inference rules with multiple conclusions as a basis for a symmetric natural deduction calculus for classical logic. However, Kneale's informally presented calculus is not complete. In this paper we define a calculus of  multiple conclusion natural deductions (MCD) for classical propositional logic based on Kneale's multiple conclusion inference rules. For MCD we present an elementary proof search that produces proofs in normal form. MCD proof search is motivated and explained as being a notational variant of Smullyan's analytic tableau method in its initial part and a notational variant of refutation proofs based on Robinson's resolution in its final part. We consider MCD to have a semantic motivation of both its inference rules and its proof search. This is unusual for the natural deduction calculi as they are syntactically motivated. Syntactic motivation is adequate for intuitionistic logic but not a natural fit for the truth-functional classical propositional logic.