#### 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.