A Calculus of Natural Deductions for the Full First-Order Predicate Logic with Identity
Hubert H. Schneider · Lincoln (University of Nebraska) · 1979
Natural deductions form an important tool in applications of logic to scientific theories. Our calculus for natural deductions is formulated in such a manner that it can be applied to the language of the full first-order predicate logic. Among its features are a certain symmetry of its deduction rules and simplified restrictions governing finished deductions. The adequacy of our natural deduction system is established by means of showing its equivalence with a more standard type of deduction system, known to be sound and complete. The proof for the equivalence of the two systems is constructive so that any deduction in one of the systems provides a deduction in the other system.