Natural Deduction: Why Implication Is Defined by Two Rules

A truth table assigns a meaning to implication by enumeration: A → B is false exactly when A is true and B is false. That definition is available only for connectives whose components already have truth values, and it says nothing about how a proof of an implication is built from proofs of its parts. Natural deduction takes the other route. A connective is defined by the rules that introduce it and the rules that eliminate it, and the meaning of a proof is whatever those rules permit.

Judgments with assumptions

The central object is a hypothetical judgment, written Γ ⊢ A: from the assumptions in Γ, the formula A follows. Γ is a list, or more often a set, of formulas. Every rule operates on the right of the turnstile, and assumptions enter and leave only through specific rules.

Two conventions are worth fixing because they are usually left implicit. Assumptions are labelled, so a derivation can refer to a particular one, and the same formula may be assumed twice under different labels, which matters for the rules that discharge assumptions. Weakening (adding an unused assumption) and contraction (using one assumption twice) are absorbed into the notation rather than stated as rules, which is one thing that distinguishes natural deduction from the sequent calculus described in Cut Elimination and the Subformula Property.

An assumption on its own is a one-line derivation: A ⊢ A. Every other rule takes derivations as premises and produces a derivation of a new conclusion. There is no axiom schema and no separate notion of theoremhood; a theorem is a derivation whose context is empty.

The introduction rule fixes what a proof of A → B is

The introduction rule for implication is

     [A]
      ⋮
      B
   -------  (→I)
    A → B

The brackets mark an assumption that the rule discharges. Read operationally: to prove A → B, assume A, derive B, and the derivation of B from that assumption becomes a proof of A → B in the surrounding context. The conclusion depends on Γ only, not on Γ extended with A.

This is the constructive reading of implication. A proof of A → B is a procedure that turns any proof of A into a proof of B, not a claim about truth values. Under the propositions-as-types reading developed in Proof Terms, the same rule is typed abstraction, and the discharged assumption is the bound variable.

The rule is also the only way to obtain a proof of an implication. Nothing asserts A → A as an axiom; the derivation is two steps, the assumption and its discharge. Systems that do assert implication axioms exist, and they are discussed below, but they do not have this property.

Elimination must undo introduction

The elimination rule is modus ponens:

   ⋮       ⋮
 A → B     A
 -----------  (→E)
     B

Introduction says how to build a proof of the connective; elimination says how to use one. In a well-designed system the two are inverse in a precise sense: eliminating a connective from a proof whose last step introduced it produces a detour that can be removed.

A detour has this shape: assume A, derive B, discharge to get A → B, then immediately apply that implication to an actual proof of A. The round trip proves B by first pretending A and then supplying A. Removing the detour means substituting the actual proof of A for every use of the assumption in the subderivation of B. In the typed reading the same operation is beta reduction: (λx. t) u becomes t[u/x].

The removal is local. It touches the introduction, the elimination, and the assumption occurrences they connect, and nothing else in the derivation. A derivation containing no such pattern is called normal. Prawitz’s normalisation theorem states that every derivation in intuitionistic natural deduction reduces to a normal one by repeated local reductions. From the normal form, a stronger fact follows: two derivations of the same conclusion with the same open assumptions can be reduced to a common normal form, which is what makes proof identity a meaningful notion rather than an artefact of a rewriting strategy.

Harmony, and what happens when it fails

The pair of rules must be in harmony: the elimination rule may draw no more from a proof of the connective than the introduction rule put into it. Harmony is what stops a connective from being defined by rules that prove too much or too little.

Two tests formalise it. Local soundness requires that every introduction followed by an elimination reduces, so that the elimination cannot extract information the introduction did not supply. Local completeness requires that every derivation of a formula whose principal connective is C converts to one ending in the introduction rule for C, so the elimination rules lose nothing. When both hold, the connective is conservative over the rest of the system and normalisation goes through.

Failures are easy to construct and instructive. Add an elimination rule for implication that concludes A from A → B regardless of B. Local soundness fails: the new rule recovers the antecedent, which the introduction rule never put into the proof, and the system now derives A from A → B. Add an extra premise to the introduction rule instead, and completeness fails, because a proof built with the weaker rule cannot be brought into the required form.

The same test explains why the two rules are not arbitrary conventions. Any pair satisfying harmony defines the connective up to provable equivalence, and the resulting system inherits the properties that follow from normalisation, chiefly consistency and the disjunction property.

What the two-rule definition buys

The gain is that the meaning of a connective is independent of any model. Normalisation is proved syntactically, by induction on derivations, and the corollaries are stronger than what truth-table semantics gives directly.

Consistency. The system cannot derive the empty sequent, so no formula and its negation are both provable. The proof inspects normal derivations: a normal derivation of ⊥ would have to end with an introduction rule for ⊥, and there is none. No semantics is required, and the argument survives when the object logic is much stronger than propositional calculus.

The disjunction property. If A ∨ B is provable then A is provable or B is provable, and the normal proof indicates which. This fails classically, where P ∨ ¬P holds for every P, and it is the property that makes proofs usable as programs: a proof of a disjunction is a decision plus a witness, and the witness can be read off the derivation.

The cost is bookkeeping. Assumption labels, discharge, and the side conditions on variables in the quantifier rules make derivations tedious by hand and fiddly to implement. A checker must track which assumptions are open at each step, and the substitution performed during detour removal must avoid capturing free variables. These are exactly the difficulties of a type checker for a lambda calculus with binders, which is why implementations choose a representation that makes them mechanical, such as de Bruijn indices, where the bookkeeping is a shift on numbers rather than a search for name clashes.

A second cost is that derivations are not canonical. The same entailment has many proofs, and normalisation collapses some but not all of them. Deciding whether two derivations establish the same fact requires more than reduction, which is the problem taken up in Definitional and Propositional Equality.

The definition stops short of classical logic

Intuitionistic natural deduction does not prove A ∨ ¬A or ¬¬A → A. Adding either restores classical logic and destroys the properties above. The usual addition is a rule allowing a derivation of A from a derivation of ⊥ under the assumption ¬A, which corresponds to the classical reductio argument. The resulting system is consistent and normalises, but normal proofs no longer have the disjunction property, because a normal proof of A ∨ ¬A need not end in either introduction rule.

Axiom-based presentations, in the Hilbert style, are the alternative. Propositional logic there needs a finite set of axiom schemata plus modus ponens; for implication alone, two schemata suffice, and adding the other connectives adds one or two more each. A proof of A → A still takes several lines, because each step is an axiom instance or an application of modus ponens and there is no rule that discharges an assumption. The system is compact and easy to state, and it is the natural target for machine-oriented proof search, but it has no notion of assumption discharge, so it does not expose the structure that normalisation acts on. Natural deduction is larger and more awkward to mechanise, and it is the presentation that connects to typed computation.

Where the rules come from, and where they are chosen

Natural deduction is often presented as the logic of ordinary mathematical argument, and that is a historical claim rather than a formal one. What the system actually guarantees is that a connective’s behaviour is fully determined by four or five rules, and that those rules can be checked for harmony independently of any intended reading.

That is why the same schema reappears for connectives with no classical counterpart. The rules for a necessity modality, for a resource-sensitive conjunction, or for a type of computations all follow the introduction/elimination pattern, and the interesting design work is deciding which eliminations are in harmony with which introductions. The pattern is a specification method, and normalisation is its acceptance test.