4.2 Natural deduction calculi

Gentzen introduced in his pioneering papers in the 1930s the idea of a natural deduction proof. (Similar ideas were in the air in the work of Herz.) There are various notions: one version is that a proof consists of a tree of formulae, where the leaves are assumptions, and the discharge of an assumption (for a rule such as ÁI, for example) is indicated by striking it out. Those assumptions on which the conclusion (the formula at the tree's root) depends are just those not struck out.

This is convenient, in the sense of requiring little copying of formulae: but it is often not clear at a glance what assumptions any formula in the midst of the tree depends on. Gentzen therefore introduced a so-called "logistic" version of natural deduction, in which the judgments (the objects on which inference rules operate) are sequents of the form used in MacLogic: a formula list, then a special symbol such as Ê, then a formula. Proofs are then defined as trees, where each node is such a sequent, and is either a leaf node, justified by the rule of Assumption, or is an internal node, justified from its children (the nodes just above it) by a rule of inference.

The notation we use in presenting proofs in the style of Lemmon is essentially a condensed version of this. First, the tree is squashed to a graph, to allow maximal sharing of sub-proofs: second, the graph is stretched out into a linear form, for ease of layout on the page, and third, the references back to assumptions are by line number rather than by using the formulae themselves.

The rules of natural deduction are generally of two kinds: rules for introducing a logical constant, and rules for eliminating one. The constants are introduced and eliminated only in the formula on the right of the turnstile Ê. (In classical logic, there is an extra rule, DN, not fitting into this pattern, for removing two negation symbols at once. We avoid calling this rule an "elimination rule".)

See the monograph by Prawitz, or the survey by Sundholm, for further details of natural deduction.