In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.
History Natural deduction grew out of a context of dissatisfaction with the axiomatizations of deductive reasoning common to the systems of Hilbert, Frege, and Russell (see, e.g., Hilbert system). Such axiomatizations were most famously used by Russell and Whitehead in their mathematical treatise Principia Mathematica. Spurred on by a series of seminars in Poland in 1926 by Łukasiewicz that advocated a more natural treatment of logic, Jaśkowski made the earliest attempts at defining a more natural deduction, first in 1929 using a diagrammatic notation, and later updating his proposal in a sequence of papers in 1934 and 1935. His proposals led to different notations such as Fitch notation or Suppes' method, for which Lemmon gave a variant now known as Suppes–Lemmon notation. Natural deduction in its modern form was independently proposed by the German mathematician Gerhard Gentzen in 1933, in a dissertation delivered to the faculty of mathematical sciences of the University of Göttingen. The term natural deduction (or rather, its German equivalent natürliches Schließen) was coined in that paper:
Gentzen was motivated by a desire to establish the consistency of number theory. He was unable to prove the main result required for the consistency result, the cut elimination theorem—the Hauptsatz—directly for natural deduction. For this reason he introduced his alternative system, the sequent calculus, for which he proved the Hauptsatz both for classical and intuitionistic logic. In a series of seminars in 1961 and 1962 Prawitz gave a comprehensive summary of natural deduction calculi, and transported much of Gentzen's work with sequent calculi into the natural deduction framework. His 1965 monograph Natural deduction: a proof-theoretical study was to become a reference work on natural deduction, and included applications for modal and second-order logic. In natural deduction, a proposition is deduced from a collection of premises by applying inference rules repeatedly. The system presented in this article is a minor variation of Gentzen's or Prawitz's formulation, but with a closer adherence to Martin-Löf's description of logical judgments and connectives.
History of notation styles Natural deduction has had a large variety of notation styles, which can make it difficult to recognize a proof for a reader not familiar with one of them. To help with this situation, this article has a § Notation section explaining how to read all the notation that it will actually use. This section just explains the historical evolution of notation styles, most of which cannot be shown because there are no illustrations available under a public copyright license – the reader is pointed to the SEP and IEP for pictures.
Gentzen invented natural deduction using tree-shaped proofs – see § Gentzen's tree notation for details. Jaśkowski changed this to a notation that used various nested boxes. Fitch changed Jaśkowski method of drawing the boxes, creating Fitch notation. 1940: In a textbook, Quine indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation. 1950: In a textbook, Quine (1982, pp. 241–255) demonstrated a method of using one or more asterisks to the left of each line of proof to indicate dependencies. This is equivalent to Kleene's vertical bars. (It is not totally clear if Quine's asterisk notation appeared in the original 1950 edition or was added in a later edition.) 1957: An introduction to practical logic theorem proving in a textbook by Suppes (1999, pp. 25–150). This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line. 1963: Stoll (1979, pp. 183–190, 215–219) uses sets of line numbers to indicate antecedent dependencies of the lines of sequential logical arguments based on natural deduction inference rules. 1965: The entire textbook by Lemmon (1978) is an introduction to logic proofs using a method based on that of Suppes, what is now known as Suppes–Lemmon notation. 1967: In a textbook, Kleene (2002, pp. 50–58, 128–130) briefly demonstrated two kinds of practical logic proofs, one system using explicit quotations of antecedent propositions on the left of each line, the other system using vertical bar-lines on the left to indicate dependencies.
Notation Here is a table with the most common notational variants for logical connectives.
Gentzen's tree notation Gentzen, who invented natural deduction, had his own notation style for arguments. This will be exemplified by a simple argument below. Let's say we have a simple example argument in propositional logic, such as, "if it's raining then it's cloudly; it is raining; therefore it's cloudy". (This is in modus ponens.) Representing this as a list of propositions, as is common, we would have:
1 ) P → Q {\displaystyle 1)~P\to Q}
2 ) P {\displaystyle 2)~P}
∴ Q {\displaystyle \therefore ~Q}
In Gentzen's notation, this would be written like this:
P → Q , P Q {\displaystyle {\frac {P\to Q,P}{Q}}}
The premises are shown above a line, called the inference line, separated by a comma, which indicates combination of premises. The conclusion is written below the inference line. The inference line represents syntactic consequence, sometimes called deductive consequence, which is also symbolized with ⊢. So the above can also be written in one line as P → Q , P ⊢ Q {\displaystyle P\to Q,P\vdash Q} . (The turnstile, for syntactic consequence, is of lower precedence than the comma, which represents premise combination, which in turn is of lower precedence than the arrow, used for material implication; so no parentheses are needed to interpret this formula.) Syntactic consequence is contrasted with semantic consequence, which is symbolized with ⊧. In this case, the conclusion follows syntactically because natural deduction is a syntactic proof system, which assumes inference rules as primitives. Gentzen's style will be used in much of this article. Gentzen's discharging annotations used to internalise hypothetical judgments can be avoided by representing proofs as a tree of sequents Γ ⊢ A instead of a tree of judgments that A (is true).
Suppes–Lemmon notation Many textbooks use Suppes–Lemmon notation, so this article will also give that – although as of now, this is only included for propositional logic, and the rest of the coverage is given only in Gentzen style. A proof, laid out in accordance with the Suppes–Lemmon notation style, is a sequence of lines containing sentences, where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence. Each line of proof is made up of a sentence of proof, together with its annotation, its assumption set, and the current line number. The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers. The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence. Here's an example proof:
This proof will become clearer when the inference rules and their appropriate annotations are specified – see § Propositional inference rules (Suppes–Lemmon style).
Propositional language syntax This section defines the formal syntax for a propositional logic language, contrasting the common ways of doing so with a Gentzen-style way of doing so.
Common definition styles In classical propositional calculus the formal language L {\displaystyle {\mathcal {L}}} is usually defined (here: by recursion) as follows:
Each propositional variable is a formula. " ⊥ {\displaystyle \bot } " is a formula. If φ {\displaystyle \varphi } and ψ {\displaystyle \psi } are formulae, so are ( φ ∧ ψ ) {\displaystyle (\varphi \land \psi )} , ( φ ∨ ψ ) {\displaystyle (\varphi \lor \psi )} , ( φ → ψ ) {\displaystyle (\varphi \to \psi )} , ( φ ↔ ψ ) {\displaystyle (\varphi \leftrightarrow \psi )} . Nothing else is a formula. Negation ( ¬ {\displaystyle \neg } ) is defined as implication to falsity
¬ ϕ = def ϕ → ⊥ {\displaystyle \neg \phi \;{\overset {\text{def}}{=}}\;\phi \to \bot } , where ⊥ {\displaystyle \bot } (falsum) represents a contradiction or absolute falsehood. Older publications, and publications that do not focus on logical systems like minimal, intuitionistic or Hilbert systems, take negation as a primitive logical connective, meaning it is assumed as a basic operation and not defined in terms of other connectives. Some authors, such as Bostock, use ⊥ {\displaystyle \bot } and ⊤ {\displaystyle \top } , and also define ¬ {\displaystyle \neg } as primitives.
Gentzen-style definition A syntax definition can also be given using § Gentzen's tree notation, by writing well-formed formulas below the inference line and any schematic variables used by those formulas above it. For instance, the equivalent of rules 3 and 4, from Bostock's definition above, is written as follows:
φ ( ¬ φ ) φ ψ ( φ ∨ ψ ) φ ψ ( φ ∧ ψ ) φ ψ ( φ → ψ ) φ ψ ( φ ↔ ψ ) {\displaystyle {\frac {\varphi }{(\neg \varphi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \lor \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \land \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \rightarrow \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \leftrightarrow \psi )}}} . A different notational convention sees the language's syntax as a categorial grammar with the single category "formula", denoted by the symbol F {\displaystyle {\mathcal {F}}} . So any elements of the syntax are introduced by categorizations, for which the notation is φ : F {\displaystyle \varphi :{\mathcal {F}}} , meaning " φ {\displaystyle \varphi } is an expression for an object in the category F {\displaystyle {\mathcal {F}}} ." The sentence-letters, then, are introduced by categorizations such as P : F {\displaystyle P:{\mathcal {F}}} , Q : F {\displaystyle Q:{\mathcal {F}}} , R : F {\displaystyle R:{\mathcal {F}}} , and so on; the connectives, in turn, are defined by statements similar to the above, but using categorization notation, as seen below:
In the rest of this article, the φ : F {\displaystyle \varphi :{\mathcal {F}}} categorization notation will be used for any Gentzen-notation statements defining the language's grammar; any other statements in Gentzen notation will be inferences, asserting that a sequent follows rather than that an expression is a well-formed formula.
Gentzen-style propositional logic
Gentzen-style inference rules Let the propositional language L {\displaystyle {\mathcal {L}}} be inductively defined as Φ ::= p 1 , p 2 , ⋯ ∣ ⊥ ∣ ( Φ → Φ ) ∣ ( Φ ∧ Φ ) ∣ ( Φ ∨ Φ ) {\displaystyle \Phi ::=p_{1},p_{2},\dots \mid \bot \mid (\Phi \to \Phi )\mid (\Phi \land \Phi )\mid (\Phi \lor \Phi )} . Define negation as ¬ Φ = def ( Φ → ⊥ ) {\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,(\Phi \to \bot )} . The following is a list of primitive inference rules for natural deduction in propositional logic:
In this table the Greek letters φ , ψ , χ {\displaystyle \varphi ,\psi ,\chi } are schemata, which range over formulas rather than only over atomic propositions. The name of a rule is given to the right of its formula tree. For instance, the first introduction rule is named ∧ I {\displaystyle \land _{I}} , which is short for "conjunction introduction".
Minimal logic: the natural deduction rules are N D M P C = { ∧ I , ∧ E , ∨ I , ∨ E , → I , → E } {\displaystyle ND_{MPC}=\{\land _{I},\land _{E},\lor _{I},\lor _{E},\to _{I},\to _{E}\}} . Without the rules ⊥ E {\displaystyle \bot _{E}} and ¬ ¬ E {\displaystyle \neg \neg _{E}} the system defines minimal logic (as discussed by Johansson). Intuitionistic logic: the natural deduction rules are N D I P C = N D M P C ∪ { ⊥ E } {\displaystyle ND_{IPC}=ND_{MPC}\cup \{\bot _{E}\}} . When the rule ⊥ E {\displaystyle \bot _{E}} (principle of explosion) is added to the rules for minimal logic, the system defines intuitionistic logic. The statement P → ¬ ¬ P {\displaystyle P\to \neg \neg P} is valid (already in minimal logic, see example 1 below), unlike the reverse implication which would entail the law of excluded middle. Classical logic: the natural deduction rules are N D C P C = N D I P C ∪ { ¬ ¬ E } {\displaystyle ND_{CPC}=ND_{IPC}\cup \{\neg \neg _{E}\}} . When all listed natural deduction rules are admitted, the system defines classical logic.
Gentzen-style example proofs Example 1: Proof, within minimal logic, of P → ¬ ¬ P {\displaystyle P\to \neg \neg P} . Goal: P → ( ( P → ⊥ ) → ⊥ ) {\displaystyle P\to ((P\to \bot )\to \bot )}
Proof:
[ P ] v [ P → ⊥ ] u ⊥ → E ( ( P → ⊥ ) → ⊥ ) P → ( ( P → ⊥ ) → ⊥ ) → I v → I u {\displaystyle {\cfrac {{\cfrac {[P]^{v}\qquad [P\to \bot ]^{u}}{\bot }}\to _{E}}{{\cfrac {((P\to \bot )\to \bot )}{P\to ((P\to \bot )\to \bot )}}\to _{I^{v}}}}\to _{I^{u}}}
Example 2: Proof, within minimal logic, of A → ( B → ( A ∧ B ) ) {\displaystyle A\to \left(B\to \left(A\land B\right)\right)} :
[ A ] u [ B ] w A ∧ B ∧ I B → ( A ∧ B ) A → ( B → ( A ∧ B ) ) → I u → I w {\displaystyle {\cfrac {{\cfrac {[A]^{u}\quad [B]^{w}}{A\land B}}\ \land _{I}}{{\cfrac {B\to \left(A\land B\right)}{A\to \left(B\to \left(A\land B\right)\right)}}\ \to _{I^{u}}}}\ \to _{I^{w}}}
Fitch-style propositional logic
Fitch developed a system of natural deduction which is characterized by
linear presentation of the proof, instead of presentation as a tree; subordinate proofs, where assumptions could be opened within a subderivation and discharged later. Later logicians and educators such as Patrick Suppes and E. J. Lemmon rebranded Fitch's system. While they introduced graphical changes—such as replacing indentation with vertical bars—the underlying structure of Fitch-style natural deduction remained intact. These variations are often referred to as the Suppes–Lemmon format, though they are fundamentally based on Fitch's original notation.
Suppes–Lemmon-style propositional logic
Suppes–Lemmon-style inference rules The linear presentation used in Fitch- and Suppes–Lemmon-style proofs — with line numbers and vertical alignment/assumption sets — makes subproofs clearly visible. Fitch (sparingly and cautiously) used derived rules. Suppes–Lemmon went further and added derived rules to the toolbox of natural deduction rules. Suppes introduced natural deduction using Gentzen-style rules.
He defined negation in terms of contradiction: ¬ P ≡ ( P → ⊥ ) {\displaystyle \neg P\equiv (P\to \bot )} . He discussed derived rules explicitly, though not always distinguishing them clearly from primitive ones in layout. His system is close to minimal, but allows derived steps for brevity. Lemmon formalized more derived rules. He as well defined negation as implication to falsity: ¬ P ≡ P → ⊥ {\displaystyle \neg P\equiv P\to \bot } . This is not stated as a formal definition in Beginning Logic, but it is implicitly assumed throughout the system, as evidenced by the following:
Use of RAA (Reductio ad Absurdum): Lemmon regularly used RAA in the form: Assume P {\displaystyle P} , derive ⊥ {\displaystyle \bot } , then conclude ¬ P {\displaystyle \neg P} . This only works if ¬ P {\displaystyle \neg P} is understood as P → ⊥ {\displaystyle P\to \bot } . Proofs involving contradiction: Lemmon used the fact that from ¬ P ∧ P {\displaystyle \neg P\land P} one can derive ⊥ {\displaystyle \bot } . This requires treating ¬ P {\displaystyle \neg P} as P → ⊥ {\displaystyle P\to \bot } , so that modus ponens yields contradiction. Absence of a primitive “¬” rule: Lemmon did not include a standalone rule for introducing or eliminating ¬. Instead, he derived negation using implication and contradiction. In the table below, based on Lemmon (1978) and Allen & Hand (2022), Lemmon's derived rules are highlighted. They can be derived from the (non-highlighted) Gentzen rules. There are nine primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rules of double negation and reductio ad absurdum, of which only one is needed. Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination, and MTT is a commonly given rule, although it is not primitive.
Suppes–Lemmon-style examples proof Recall that an example proof was already given when introducing § Suppes–Lemmon notation. This is a second example.
Example 2
Example 3 The next derivation proves two theorems:
lines 1 - 8 prove within minimal logic:
⊢ M P C ¬ ¬ ( P ∨ ¬ P ) {\displaystyle \vdash _{MPC}\neg \neg (P\lor \neg P)} . lines 1 - 9 prove within classical logic:
⊢ C P C P ∨ ¬ P {\displaystyle \vdash _{CPC}P\lor \neg P} . Goals:
lines 1 - 8: ⊢ M P C ( ( P ∨ ( P → ⊥ ) ) → ⊥ ) → ⊥ {\displaystyle \vdash _{MPC}((P\lor (P\to \bot ))\to \bot )\to \bot } . lines 1 - 9: ⊢ C P C P ∨ ( P → ⊥ ) {\displaystyle \vdash _{CPC}P\lor (P\to \bot )} .
Remark: Valery Glivenko proved the following theorem:
If φ {\displaystyle \varphi } is a propositional formula, then φ {\displaystyle \varphi } is a classical tautology if and only if ¬ ¬ φ {\displaystyle \neg \neg \varphi } is an intuitionistic tautology. This implies that all classical propositional theorems φ {\displaystyle \varphi } can be proved like in this example:
Prove ¬ ¬ φ {\displaystyle \neg \neg \varphi } within intuitionistic logic (i.e. without ¬ ¬ E {\displaystyle \neg \neg _{E}} ). Apply ¬ ¬ E {\displaystyle \neg \neg _{E}} to get φ {\displaystyle \varphi } from ¬ ¬ φ {\displaystyle \neg \neg \varphi } .
Consistency, completeness, and normal forms
A theory is said to be consistent if falsehood is not provable (from no assumptions) and is complete if every theorem or its negation is provable using the inference rules of the logic. These are statements about the entire logic, and are usually tied to some notion of a model. However, there are local notions of consistency and completeness that are purely syntactic checks on the inference rules, and require no appeals to models. The first of these is local consistency, also known as local reducibility, which says that any derivation containing an introduction of a connective followed immediately by its elimination can be turned into an equivalent derivation without this detour. It is a check on the strength of elimination rules: they must not be so strong that they include knowledge not already contained in their premises. As an example, consider conjunctions.
A u
B w A ∧ B ∧ I A ∧ E 1 ⇒
A u {\displaystyle {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ }}u\qquad {\cfrac {}{B\ }}w}{A\wedge B\ }}\wedge _{I}}{A\ }}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ }}u}
Dually, local completeness says that the elimination rules are strong enough to decompose a connective into the forms suitable for its introduction rule. Again for conjunctions:
A ∧ B u ⇒
A ∧ B