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.
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.
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 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.
Here is a table with the most common notational variants for logical connectives.
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:
In Gentzen's notation, this would be written like this:
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 . (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).
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 .
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.
In classical propositional calculus the formal language is usually defined (here: by recursion) as follows:
Negation () is defined as implication to falsity
where (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 and , and also define as primitives.
A syntax definition can also be given using , 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:
A different notational convention sees the language's syntax as a categorial grammar with the single category "formula", denoted by the symbol . So any elements of the syntax are introduced by categorizations, for which the notation is , meaning " is an expression for an object in the category ." The sentence-letters, then, are introduced by categorizations such as ,âÂÂ,âÂÂ, 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 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.
Let the propositional language be inductively defined as .
Define negation as .
The following is a list of primitive inference rules for natural deduction in propositional logic:
In this table the Greek letters 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 , which is short for "conjunction introduction".
Example 1: Proof, within minimal logic, of .
Goal: <br/> Proof:
Example 2: Proof, within minimal logic, of :
Fitch developed a system of natural deduction which is characterized by
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.
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.
Lemmon formalized more derived rules. He as well defined negation as implication to falsity: . This is not stated as a formal definition in Beginning Logic, but it is implicitly assumed throughout the system. Here's how we know:
In the table below, based on Lemmon (1978) and Allen & Hand (2022), Lemmon's derived rules are <span style="background-color: yellow;">highlighted</span>. 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.