Natural deduction Glossary
Definition
A natural deduction calculus for a system of logic is one in which there are many rules intended to capture the meanings of all the logical devices (connectives, quantifiers, etc) involved. Generally, each connective, quantifier or other logical expression is given an introduction rule, saying what formulae of that form follow from, and an elimination rule, saying what follows from them.
Comments
Natural deduction contrasts with other presentations of logic such as axiomatic systems, semantic tableaux and sequent calculi. As the name suggests, it is an attempt to formulate reasoning in a human way, appealing at each step to the basic logical properties of the main operator involved.
Natural deduction proofs can be written in several ways. They can be drawn as trees, with the formulae as nodes of a graph joined by lines representing applications of the rules. Alternatively, they can be written as sequential lists of formulae, either with indentation to show sub-proofs or with the assumptions on which each line depends explicitly written out.