Original scientific paper

On multiple conclusion deductions in classical logic

Marcel Maretić ; Faculty of Organization and Informatics, University of Zagreb, Varaždin, Croatia

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 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 tableaux 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 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 truth-functional classical propositional logic.

Keywords

multiple conclusion natural deductions; Kneale’s developments; analytic deductions; classical propositional logic

Hrčak ID:

192128

URI

https://hrcak.srce.hr/192128

Publication date:

30.5.2018.

Visits: 1.371 *