Natural deduction

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. 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 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 if you're 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 and for pictures.

Gentzen invented natural deduction using tree-shaped proofs – see 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, 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.
1957: An introduction to practical logic theorem proving in a textbook by. This indicated dependencies by line numbers at the left of each line.
1963: 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 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, 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.

Connective	Symbol
AND	,,,,
equivalent	,,,
implies	,,
NAND	,,
nonequivalent	,,
NOR	,,
NOT	,,,
OR	,,,
XNOR
XOR	,

Gentzen's tree notation

, 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". 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.
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.

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 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 is usually defined as follows:

Each propositional variable is a formula.
"" is a formula.
If and are formulae, so are,,,.
Nothing else is a formula.

Negation is defined as implication to falsity
where 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.

Gentzen-style definition

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:

Conjunction	Disjunction	Implication	Negation

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.

Gentzen-style propositional logic

Gentzen-style inference rules

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:

Introduction rules	Elimination rules

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

Minimal logic: the natural deduction rules are.
Intuitionistic logic: the natural deduction rules are.
Classical logic: the natural deduction rules are.