Naslov
On multiple conclusion deductions in classical logic

Autori
Maretić, Marcel

Izvornik
Mathematical communications (1331-0623) 23 (2018), 1; 79-95

Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni

Ključne riječi
multiple conclusion natural deductions ; Kneale's developments ; analytic deductions ; classical propositional logic

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika

POVEZANOST RADA