Abstract

Gentzen’s singular sequential system of first-order logic was an alternative notation for his system of natural deductions. His multiple sequential system was his symmetric generalization that was more appropriate to classical logic. Beth’s tableaus system was a system that was derived directly from the semantic analysis of connectives and quantifiers. It was soon realized that the Beth’s system and the Gentzen’s multiple system were only notational variants of each other. Kneale’s system of multiple natural deductions was a generalization of Gentzen’s system of natural deductions. We prove that Kneale’s natural deductions are also a notational variant of Beth’s tableaus.