Natural deduction

Natural deduction presents logic through introduction and elimination rules for each logical connective.

Reading an inference rule backwards to replace a desired conclusion by sufficient subgoals. A conjunction goal can be replaced by its two conjuncts using the conjunction introduction rule; an available disjunction can instead lead to two case subgoals using the disjunction elimination rule. Different choices change the organization and sharing of subproofs. Scope and assumption discharge conditions remain obligations even when a rule is applied backwards during proof search.

Adding unused assumptions to the context of a logical derivation. The original derivation still proves the same conclusion because it need not use every available assumption. When eigenvariables are used, rename them first if necessary to preserve the eigenvariable condition for any newly added assumptions. This explains how disjunction elimination with different branch contexts can be written using a common context containing all their assumptions.

Thinning enlarges the assumptions without changing a conclusion. In a predicate-calculus presentation with context-sensitive generalization, a generalization valid before adding an unused assumption may not be replayable with that assumption open. An explicit weakening step nevertheless imports the already proved conclusion. In propositional calculus with only axiom schemes and modus ponens, weakening is admissible by replaying the proof. The need for a separately stated rule depends on how proof dependencies are represented.

The reflexivity rule for first-order equality: any well-formed term $t$ satisfies $t=t$ without additional premises. Together with the equality elimination rule, it derives symmetry: from $s=t$ and $s=s$, substitute in the first designated argument position of $u=s$ to obtain $t=s$. Transitivity follows from $s=t$ and $t=u$ by substitution in the second designated argument position of $s=v$.

Derive each side of a logical biconditional under a temporary assumption of the other, then discharge both assumptions. The surrounding assumptions $\Gamma$ remain. This is equivalent to deriving the two implications and combining them as the two directions of equivalence.

Introduce exclusive or from either $P,\neg Q$ or $\neg P,Q$. To eliminate $P\oplus Q$, derive the same conclusion $K$ in two subproofs, one under $P,\neg Q$ and the other under $\neg P,Q$, then discharge both pairs of case assumptions. These rules express exactly the two disjuncts of the displayed disjunctive normal form. Conjunction introduction and disjunction introduction derive that formula in each elimination branch; conversely disjunction elimination and conjunction elimination supply the two introduction cases. This proves equivalence without adding an unproved truth-table inference to a formal derivation.

From $P$, temporarily assume $\neg P$. Negation elimination rule gives logical falsity; discharge that temporary assumption by negation introduction to obtain $\neg \neg P$. This is valid in Intuitionistic propositional logic, unlike unrestricted double-negation elimination.

A local derivation made under additional temporary assumptions. Its conclusions can be used within their scopes, but exporting a result requires a rule that accounts for those assumptions. Indentation, boxes or explicit assumption labels record that dependency information.

A temporary assumption is introduced for a hypothetical subproof and retained only within that scope. A suitable inference rule can discharge it while forming a conclusion valid under the surrounding assumptions. Its scope must be recorded even when the assumption is unused inside the subproof.

From $\varphi \to (\psi \to \rho )$ infer $(\varphi \to \psi )\to (\varphi \to \rho )$. Assume $\varphi \to \psi$, then assume $\varphi$. Implication elimination rule gives $\psi$ and $\psi \to \rho$, hence $\rho$. Discharge $\varphi$ and then $\varphi \to \psi$ by the implication introduction rule. The original premise and any surrounding assumptions remain available.

From a logical derivation of $\psi$, infer $\varphi \to \psi$ under the same surrounding assumptions. To derive the rule, temporarily assume $\varphi$, retain the available $\psi$, and discharge $\varphi$ by the implication introduction rule. Its being unused is allowed.

From $\exists xA(x)$, reason under a temporary assumption $A(u)$ for a fresh witness $u$. If this yields a conclusion $B$ not containing $u$ free, close the witness subproof and infer $B$. The eigenvariable condition also requires that $u$ not be free in other undischarged assumptions. The rule does not authorize selecting one fixed named object as a witness or allowing the witness to escape its scope.

An eigenvariable condition ensures that a variable chosen as arbitrary or as an existential witness cannot smuggle extra information into a quantifier inference. For the universal quantifier introduction rule, the generalized variable must not occur free in any undischarged assumption. For the existential quantifier elimination rule, the fresh witness must not occur free in the resulting conclusion or in the other undischarged assumptions. Temporary assumptions may contain it if they are discharged before the final inference.

A variable used as an arbitrary parameter in a natural deduction subproof, subject to an eigenvariable condition. For universal introduction, it must be free in no undischarged assumption. For existential elimination, a temporary witness must also be free in no conclusion exported from its subproof. These restrictions distinguish an arbitrary object from one constrained by a special hypothesis.

An invalid quantifier inference that exports a formula still referring freely to a temporary existential witness. From $\exists xS(x)$ one cannot infer $S(v)$ for an independently named object $v$. A two-element interpretation with exactly one $S$-object refutes that inference. Introducing another quantifier after the invalid step does not repair it; the introduction must take place before the witness scope is closed.

Assumption discharge closes a designated temporary assumption together with its dependent subproof. Implication introduction rule turns a logical derivation of $B$ under $A$ into $A\to B$ outside that temporary scope. Negation introduction rule turns a logical derivation of logical falsity under $A$ into $\neg A$. Disjunction elimination rule discharges its separate case assumptions while retaining any surrounding premises.

From logical falsity infer any proposition. This rule permits a contradictory case inside a disjunction elimination rule proof to reach the common required conclusion.

From $s=t$ and $A(s)$, infer $A(t)$ by capture-free substitution. Rewriting in the opposite direction first uses symmetry of equality.

From $A(t)$, infer $\exists xA(x)$ when the substitution is capture-free. The term $t$ supplies a witness.

From $\forall xA(x)$, infer $A(t)$ provided the substitution is free for $x$, meaning no free variable of $t$ becomes captured.

If $A(u)$ is proved and $u$ is not free in any undischarged assumption, infer $\forall xA(x)$, with capture-free replacement. The freshness condition prevents generalizing from a special object.

From $A\leftrightarrow B$, infer $A\to B$ or $B\to A$. Applying the resulting implication requires a further modus ponens rule.

From $A\vee B$ and two subproofs deriving the same conclusion $C$, one under an additional assumption $A$ and the other under an additional assumption $B$, infer $C$ and discharge those two case assumptions. Any other assumptions remain in force.

If each of $A$, $B$ and $C$ separately yields the same conclusion $K$, then $A\vee B\vee C$ yields $K$, with the three case assumptions discharged. For $(A\vee B)\vee C$, first eliminate the outer logical disjunction, using a nested applications of the disjunction elimination rule on the $A\vee B$ branch. For $A\vee (B\vee C)$, nest the second elimination in the other branch. Common surrounding assumptions remain open.

The disjunction introduction rule in natural deduction permits either inferenceHere $A$ and $B$ are propositions, and $\vee$ denotes logical disjunction. Establishing either disjunct is sufficient to establish the compound proposition.

The truth table explains soundness in classical propositional logic: every assignment making the premise true makes the conclusion true. For example, a proof of $x=0$ also proves $x=0\vee x=1$, without requiring a proof of $x=1$.

The conjunction elimination rule in natural deduction permits both inferencesThe symbol $\wedge$ denotes logical conjunction. A proof of the conjunction supplies each of its component propositions, so either component can be used in a later argument.

For example, from $0<x\wedge x<1$ one can infer $0<x$ when establishing positivity, and separately infer $x<1$ when establishing an upper bound. The truth table makes the rule sound: every assignment satisfying the conjunction satisfies both components.

From derivations of $A$ and $B$ under the current assumptions, infer $A\wedge B$.

From a propositional formula and its negation, infer logical falsity. This identifies a contradiction inside a natural deduction derivation; a later negation introduction rule may discharge the assumption that led to it.

If a natural deduction subproof derives logical falsity from a temporary assumption $P$, discharge that assumption to conclude $\neg P$. Other undischarged assumptions remain available. This gives a constructive proof of a negation and does not require double-negation elimination.

The rule with premises $C,D$ and conclusion $C$ retains the first derivation while allowing an unused second assumption. Under the Curry-Howard correspondence, the output term is the first premise term, with the enlarged context. This allows a lambda abstraction whose bound variable does not occur in its body.

From $A\to B$ and $A$, implication elimination derives $B$. Under the Curry-Howard correspondence, this is application: from lambda terms $f:A\to B$ and $a:A$ form $fa:B$.

The implication introduction rule discharges a temporary assumption $A$ from a derivation of $B$, producing $A\to B$. Under the Curry-Howard correspondence, a body $t:B$ under $a:A$ gives the lambda abstraction $\lambda a^A.t:A\to B$. Unused assumptions may also be discharged.