On multiple conclusion deductions in classical logic.

Saved in:

Bibliographic Details
Title:	On multiple conclusion deductions in classical logic.
Authors:	MARETIĆ, MARCEL¹ marcel.maretic@foi.hr
Source:	Mathematical Communications. 2018, Vol. 23 Issue 1, p79-95. 17p.
Subjects:	Calculus, Natural deduction (Logic), Intuitionistic mathematics, Linear differential equations, Nonlinear equations
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. AMS subject classifications: 03B05, 03F03 [ABSTRACT FROM AUTHOR]
	Copyright of Mathematical Communications is the property of University of Osijek, Department of Mathematics and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
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. AMS subject classifications: 03B05, 03F03 [ABSTRACT FROM AUTHOR]
ISSN:	13310623