Natural deduction

The formal language ${\displaystyle {\mathcal {L}}}$ of a propositional calculus is usually defined by a recursive definition, such as this one, from Bostock:^[18]

1. Each sentence-letter is a formula.
2. "${\displaystyle \top }$" and "${\displaystyle \bot }$" are formulae.
3. If ${\displaystyle \varphi }$ is a formula, so is ${\displaystyle \neg \varphi }$.
4. 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 )}$.
5. Nothing else is a formula.

There are other ways of doing it, such as the

${\displaystyle \phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\&~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi }$

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.^[20] 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 ${\displaystyle {\mathcal {F}}}$. So any elements of the syntax are introduced by categorizations, for which the notation is ${\displaystyle \varphi :{\mathcal {F}}}$, meaning "${\displaystyle \varphi }$ is an expression for an object in the category ${\displaystyle {\mathcal {F}}}$."^[21] The sentence-letters, then, are introduced by categorizations such as ${\displaystyle P:{\mathcal {F}}}$, ${\displaystyle Q:{\mathcal {F}}}$, ${\displaystyle R:{\mathcal {F}}}$, and so on;^[21] the connectives, in turn, are defined by statements similar to the above, but using categorization notation, as seen below:

Connectives defined through a categorial grammar^[21]

Conjunction (&)	Disjunction (∨)	Implication (→)	Negation (¬)
${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\&(A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\vee (A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\supset (A)(B):{\mathcal {F}}}}}$	${\displaystyle {\frac {A:{\mathcal {F}}}{\neg (A):{\mathcal {F}}}}}$

In the rest of this article, the ${\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

The following is a complete list of primitive inference rules for natural deduction in classical propositional logic:^[20]

Rules for classical propositional logic

Introduction rules	Elimination rules
${\displaystyle {\begin{array}{c}\varphi \qquad \psi \\\hline \varphi \wedge \psi \end{array}}(\wedge _{i})}$	${\displaystyle {\begin{array}{c}\varphi \wedge \psi \\\hline \varphi \end{array}}(\wedge _{e})}$
${\displaystyle {\begin{array}{c}\varphi \\\hline \varphi \vee \psi \end{array}}(\vee _{i})}$	${\displaystyle {\cfrac {\varphi \vee \psi \quad {\begin{matrix}[\varphi ]^{u}\\\vdots \\\chi \end{matrix}}\quad {\begin{matrix}[\psi ]^{v}\\\vdots \\\chi \end{matrix}}}{\chi }}\ \vee _{E^{u,v}}}$
${\displaystyle {\begin{array}{c}[\varphi ]^{u}\\\vdots \\\psi \\\hline \varphi \to \psi \end{array}}(\to _{i})\ u}$	${\displaystyle {\begin{array}{c}\varphi \qquad \varphi \to \psi \\\hline \psi \end{array}}(\to _{e})}$
${\displaystyle {\begin{array}{c}[\varphi ]^{u}\\\vdots \\\bot \\\hline \neg \varphi \end{array}}(\neg _{i})\ u}$	${\displaystyle {\begin{array}{c}\varphi \qquad \neg \varphi \\\hline \bot \end{array}}(\neg _{e})}$
	${\displaystyle {\begin{array}{c}[\neg \varphi ]^{u}\\\vdots \\\bot \\\hline \varphi \end{array}}({\text{PBC}})\ u}$

This table follows the custom of using Greek letters as schemata, which may range over any 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 ${\displaystyle \wedge _{i}}$, which is short for "conjunction introduction".

Gentzen-style example proofs

As an example of the use of inference rules, consider commutativity of conjunction. If A ∧ B, then B ∧ A; this derivation can be drawn by composing inference rules in such a fashion that premises of a lower inference match the conclusion of the next higher inference.

As a second example, consider the derivation of "A ⊃ (B ⊃ (A ∧ B))":

This full derivation has no unsatisfied premises; however, sub-derivations are hypothetical. For instance, the derivation of "B ⊃ (A ∧ B)" is hypothetical with antecedent "A" (named u).

Suppes–Lemmon-style propositional logic

Suppes–Lemmon-style inference rules

Natural deduction inference rules, due ultimately to Gentzen, are given below.^[22] There are ten primitive rules of proof, which are the rule assumption, plus four pairs of introduction and elimination rules for the binary connectives, and the rule reductio ad adbsurdum.^[17] Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,^[17] and MTT and DN are commonly given rules,^[22] although they are not primitive.^[17]

List of Inference Rules

Rule Name	Alternative names	Annotation	Assumption set	Statement
Rule of Assumptions[22]	Assumption[17]	A[22][17]	The current line number.[17]	At any stage of the argument, introduce a proposition as an assumption of the argument.[22][17]
Conjunction introduction	Ampersand introduction,[22][17] conjunction (CONJ)[17][23]	m, n &I[17][22]	The union of the assumption sets at lines m and n.[17]	From ${\displaystyle \varphi }$ and ${\displaystyle \psi }$ at lines m and n, infer ${\displaystyle \varphi ~\&~\psi }$.[22][17]
Conjunction elimination	Simplification (S),[17] ampersand elimination[22][17]	m &E[17][22]	The same as at line m.[17]	From ${\displaystyle \varphi ~\&~\psi }$ at line m, infer ${\displaystyle \varphi }$ and ${\displaystyle \psi }$.[17][22]
Disjunction introduction[22]	Addition (ADD)[17]	m ∨I[17][22]	The same as at line m.[17]	From ${\displaystyle \varphi }$ at line m, infer ${\displaystyle \varphi \lor \psi }$, whatever ${\displaystyle \psi }$ may be.[17][22]
Disjunction elimination	Wedge elimination,[22] dilemma (DL)[23]	j,k,l,m,n ∨E[22]	The lines j,k,l,m,n.[22]	From ${\displaystyle \varphi \lor \psi }$ at line j, and an assumption of ${\displaystyle \varphi }$ at line k, and a derivation of ${\displaystyle \chi }$ from ${\displaystyle \varphi }$ at line l, and an assumption of ${\displaystyle \psi }$ at line m, and a derivation of ${\displaystyle \chi }$ from ${\displaystyle \psi }$ at line n, infer ${\displaystyle \chi }$.[22]
Disjunctive Syllogism	Wedge elimination (∨E),[17] modus tollendo ponens (MTP)[17]	m,n DS[17]	The union of the assumption sets at lines m and n.[17]	From ${\displaystyle \varphi \lor \psi }$ at line m and ${\displaystyle -\varphi }$ at line n, infer ${\displaystyle \psi }$; from ${\displaystyle \varphi \lor \psi }$ at line m and ${\displaystyle -\psi }$ at line n, infer ${\displaystyle \varphi }$.[17]
Arrow elimination[17]	Modus ponendo ponens (MPP),[22][17] modus ponens (MP),[23][17] conditional elimination	m, n →E[17][22]	The union of the assumption sets at lines m and n.[17]	From ${\displaystyle \varphi \to \psi }$ at line m, and ${\displaystyle \varphi }$ at line n, infer ${\displaystyle \psi }$.[17]
Arrow introduction[17]	Conditional proof (CP),[23][22][17] conditional introduction	n, →I (m)[17][22]	Everything in the assumption set at line n, excepting m, the line where the antecedent was assumed.[17]	From ${\displaystyle \psi }$ at line n, following from the assumption of ${\displaystyle \varphi }$ at line m, infer ${\displaystyle \varphi \to \psi }$.[17]
Reductio ad absurdum[22]	Indirect Proof (IP),[17] negation introduction (−I),[17] negation elimination (−E)[17]	m, n RAA (k)[17]	The union of the assumption sets at lines m and n, excluding k (the denied assumption).[17]	From a sentence and its denial[b] at lines m and n, infer the denial of any assumption appearing in the proof (at line k).[17]
Double arrow introduction[17]	Biconditional definition (Df ↔),[22] biconditional introduction	m, n ↔ I[17]	The union of the assumption sets at lines m and n.[17]	From ${\displaystyle \varphi \to \psi }$ and ${\displaystyle \psi \to \varphi }$ at lines m and n, infer ${\displaystyle \varphi \leftrightarrow \psi }$.[17]
Double arrow elimination[17]	Biconditional definition (Df ↔),[22] biconditional elimination	m ↔ E[17]	The same as at line m.[17]	From ${\displaystyle \varphi \leftrightarrow \psi }$ at line m, infer either ${\displaystyle \varphi \to \psi }$ or ${\displaystyle \psi \to \varphi }$.[17]
Double negation[22][23]	Double negation elimination	m DN[22]	The same as at line m.[22]	From ${\displaystyle --\varphi }$ at line m, infer ${\displaystyle \varphi }$.[22]
Modus tollendo tollens[22]	Modus tollens (MT)[23]	m, n MTT[22]	The union of the assumption sets at lines m and n.[22]	From ${\displaystyle \varphi \to \psi }$ at line m, and ${\displaystyle -\psi }$ at line n, infer ${\displaystyle -\varphi }$.[22]

Suppes–Lemmon-style example proof

Recall that an example proof was already given when introducing § Suppes–Lemmon notation. This is a second example.

Suppes–Lemmon style proof (second example)

Assumption set	Line number	Sentence of proof	Annotation
1	1	${\displaystyle P\lor Q}$	A
2	2	${\displaystyle \neg P}$	A
3	3	${\displaystyle \neg P\to \neg Q}$	A
2, 3	4	${\displaystyle \neg Q}$	2, 3 →E
1, 2, 3	5	${\displaystyle P}$	1, 4 &E
1, 3	6	${\displaystyle P}$	2, 5 RAA(2)
2, 3	7	${\displaystyle \neg P}$	2, 3 RAA(1)

Consistency, completeness, and normal forms

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

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.

${\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:

${\displaystyle {\cfrac {}{A\wedge B\ }}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ }}u}{A\ }}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ }}u}{B\ }}\wedge _{E2}}{A\wedge B\ }}\wedge _{I}\end{aligned}}}$

These notions correspond exactly to

presentation.

First and higher-order extensions

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

The logic of the earlier section is an example of a single-sorted logic, i.e., a logic with a single kind of object: propositions. Many extensions of this simple framework have been proposed; in this section we will extend it with a second sort of individuals or terms. More precisely, we will add a new category, "term", denoted ${\displaystyle {\mathcal {T}}}$. We shall fix a

${\displaystyle V}$

${\displaystyle F}$

${\displaystyle {\frac {v\in V}{v:{\mathcal {T}}}}{\hbox{ var}}_{F}}$

and

${\displaystyle {\frac {f\in F\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{f(t_{1},t_{2},\cdots ,t_{n}):{\mathcal {T}}}}{\hbox{ app}}_{F}}$

For propositions, we consider a third countable set P of predicates, and define atomic predicates over terms with the following formation rule:

${\displaystyle {\frac {\phi \in P\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{\phi (t_{1},t_{2},\cdots ,t_{n}):{\mathcal {F}}}}{\hbox{ pred}}_{F}}$

The first two rules of formation provide a definition of a term that is effectively the same as that defined in term algebra and model theory, although the focus of those fields of study is quite different from natural deduction. The third rule of formation effectively defines an atomic formula, as in first-order logic, and again in model theory.

To these are added a pair of formation rules, defining the notation for quantified propositions; one for universal (∀) and existential (∃) quantification:

${\displaystyle {\frac {x\in V\qquad A:{\mathcal {F}}}{\forall x.A:{\mathcal {F}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A:{\mathcal {F}}}{\exists x.A:{\mathcal {F}}}}\;\exists _{F}}$

The

${\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a:{\mathcal {T}}}}{\text{ u}}\\\vdots \\{}[a/x]A\end{array}}{\forall x.A}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A\qquad t:{\mathcal {T}}}{[t/x]A}}\;\forall _{E}}$

The

${\displaystyle {\frac {[t/x]A}{\exists x.A}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a:{\mathcal {T}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A\quad &C\\\end{array}}{C}}\exists _{E^{a,u,v}}}$

In these rules, the notation [t/x] A stands for the substitution of t for every (visible) instance of x in A, avoiding capture.^[c] As before the superscripts on the name stand for the components that are discharged: the term a cannot occur in the conclusion of ∀I (such terms are known as eigenvariables or parameters), and the hypotheses named u and v in ∃E are localised to the second premise in a hypothetical derivation. Although the propositional logic of earlier sections was decidable, adding the quantifiers makes the logic undecidable.

So far, the quantified extensions are first-order: they distinguish propositions from the kinds of objects quantified over. Higher-order logic takes a different approach and has only a single sort of propositions. The quantifiers have as the domain of quantification the very same sort of propositions, as reflected in the formation rules:

${\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\forall p.A:{\mathcal {F}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\exists p.A:{\mathcal {F}}}}\;\exists _{F^{u}}}$

A discussion of the introduction and elimination forms for higher-order logic is beyond the scope of this article. It is possible to be in-between first-order and higher-order logics. For example, second-order logic has two kinds of propositions, one kind quantifying over terms, and the second kind quantifying over propositions of the first kind.

Proofs and type theory

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

The presentation of natural deduction so far has concentrated on the nature of propositions without giving a formal definition of a proof. To formalise the notion of proof, we alter the presentation of hypothetical derivations slightly. We label the antecedents with proof variables (from some countable set V of variables), and decorate the succedent with the actual proof. The antecedents or hypotheses are separated from the succedent by means of a turnstile (⊢). This modification sometimes goes under the name of localised hypotheses. The following diagram summarises the change.

──── u1 ──── u2 ... ──── un
 J1      J2          Jn
              ⋮
              J

u1:J1, u2:J2, ..., un:Jn ⊢ J

The collection of hypotheses will be written as Γ when their exact composition is not relevant. To make proofs explicit, we move from the proof-less judgment "A" to a judgment: "π is a proof of (A)", which is written symbolically as "π : A". Following the standard approach, proofs are specified with their own formation rules for the judgment "π proof". The simplest possible proof is the use of a labelled hypothesis; in this case the evidence is the label itself.

u ∈ V
─────── proof-F
u proof

───────────────────── hyp
u:A ⊢ u : A

Let us re-examine some of the connectives with explicit proofs. For conjunction, we look at the introduction rule ∧I to discover the form of proofs of conjunction: they must be a pair of proofs of the two conjuncts. Thus:

π1 proof    π2 proof
──────────────────── pair-F
(π1, π2) proof

Γ ⊢ π1 : A    Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

The elimination rules ∧E₁ and ∧E₂ select either the left or the right conjunct; thus the proofs are a pair of projections—first (fst) and second (snd).

π proof
─────────── fst-F
fst π proof

Γ ⊢ π : A ∧ B
───────────── ∧E1
Γ ⊢ fst π : A

π proof
─────────── snd-F
snd π proof

Γ ⊢ π : A ∧ B
───────────── ∧E2
Γ ⊢ snd π : B

For implication, the introduction form localises or binds the hypothesis, written using a λ; this corresponds to the discharged label. In the rule, "Γ, u:A" stands for the collection of hypotheses Γ, together with the additional hypothesis u.

π proof
──────────── λ-F
λu. π proof

Γ, u:A ⊢ π : B
───────────────── ⊃I
Γ ⊢ λu. π : A ⊃ B

π1 proof   π2 proof
─────────────────── app-F
π1 π2 proof

Γ ⊢ π1 : A ⊃ B    Γ ⊢ π2 : A
──────────────────────────── ⊃E
Γ ⊢ π1 π2 : B

With proofs available explicitly, one can manipulate and reason about proofs. The key operation on proofs is the substitution of one proof for an assumption used in another proof. This is commonly known as a substitution theorem, and can be proved by induction on the depth (or structure) of the second judgment.

Substitution theorem

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

If Γ ⊢ π₁ : A and Γ, u:A ⊢ π₂ : B, then Γ ⊢ [π₁/u] π₂ : B.

So far the judgment "Γ ⊢ π : A" has had a purely logical interpretation. In type theory, the logical view is exchanged for a more computational view of objects. Propositions in the logical interpretation are now viewed as types, and proofs as programs in the lambda calculus. Thus the interpretation of "π : A" is "the program π has type A". The logical connectives are also given a different reading: conjunction is viewed as product (×), implication as the function arrow (→), etc. The differences are only cosmetic, however. Type theory has a natural deduction presentation in terms of formation, introduction and elimination rules; in fact, the reader can easily reconstruct what is known as simple type theory from the previous sections.

The difference between logic and type theory is primarily a shift of focus from the types (propositions) to the programs (proofs). Type theory is chiefly interested in the convertibility or reducibility of programs. For every type, there are canonical programs of that type which are irreducible; these are known as canonical forms or values. If every program can be reduced to a canonical form, then the type theory is said to be

Example: Dependent Type Theory

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

Like logic, type theory has many extensions and variants, including first-order and higher-order versions. One branch, known as

Γ ⊢ A type    Γ, x:A ⊢ B type
───────────────────────────── Π-F
Γ ⊢ Πx:A. B type

Γ ⊢ A type  Γ, x:A ⊢ B type
──────────────────────────── Σ-F
Γ ⊢ Σx:A. B type

Γ, x:A ⊢ π : B
──────────────────── ΠI
Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π1 : Πx:A. B   Γ ⊢ π2 : A
───────────────────────────── ΠE
Γ ⊢ π1 π2 : [π2/x] B

Γ ⊢ π1 : A    Γ, x:A ⊢ π2 : B
───────────────────────────── ΣI
Γ ⊢ (π1, π2) : Σx:A. B

Γ ⊢ π : Σx:A. B
──────────────── ΣE1
Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B
──────────────────────── ΣE2
Γ ⊢ snd π : [fst π/x] B

.

The intersection of logic and type theory is a vast and active research area. New logics are usually formalised in a general type theoretic setting, known as a

LF

are based on higher-order dependent type theory, with various trade-offs in terms of decidability and expressive power. These logical frameworks are themselves always specified as natural deduction systems, which is a testament to the versatility of the natural deduction approach.

Classical and modal logics

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

For simplicity, the logics presented so far have been

excluded middle

:

For any proposition p, the proposition p ∨ ¬p is true.

This statement is not obviously either an introduction or an elimination; indeed, it involves two distinct connectives. Gentzen's original treatment of excluded middle prescribed one of the following three (equivalent) formulations, which were already present in analogous forms in the systems of Hilbert and Heyting:

────────────── XM1
A ∨ ¬A

¬¬A
────────── XM2
A

──────── u
¬A
⋮
p
────── XM3u, p
A

(XM₃ is merely XM₂ expressed in terms of E.) This treatment of excluded middle, in addition to being objectionable from a purist's standpoint, introduces additional complications in the definition of normal forms.

A comparatively more satisfactory treatment of classical natural deduction in terms of introduction and elimination rules alone was first proposed by

A valid
──────── ◻I
◻ A

◻ A
──────── ◻E
A

Ω;⋅ ⊢ π : A
──────────────────── ◻I
Ω;⋅ ⊢ box π : ◻ A

Ω;Γ ⊢ π : ◻ A
────────────────────── ◻E
Ω;Γ ⊢ unbox π : A

─────────────────────────────── valid-hyp
Ω, u: (A valid) ; Γ ⊢ u : A

This framework of separating judgments into distinct collections of hypotheses, also known as multi-zoned or polyadic contexts, is very powerful and extensible; it has been applied for many different modal logics, and also for linear and other substructural logics, to give a few examples. However, relatively few systems of modal logic can be formalised directly in natural deduction. To give proof-theoretic characterisations of these systems, extensions such as labelling or systems of deep inference.

The addition of labels to formulae permits much finer control of the conditions under which rules apply, allowing the more flexible techniques of

Comparison with sequent calculus

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

The sequent calculus is the chief alternative to natural deduction as a foundation of

In the sequent calculus all inference rules have a purely bottom-up reading. Inference rules can apply to elements on both sides of the turnstile. (To differentiate from natural deduction, this article uses a double arrow ⇒ instead of the right tack ⊢ for sequents.) The introduction rules of natural deduction are viewed as right rules in the sequent calculus, and are structurally very similar. The elimination rules on the other hand turn into left rules in the sequent calculus. To give an example, consider disjunction; the right rules are familiar:

Γ ⇒ A
───────── ∨R1
Γ ⇒ A ∨ B

Γ ⇒ B
───────── ∨R2
Γ ⇒ A ∨ B

On the left:

Γ, u:A ⇒ C       Γ, v:B ⇒ C
─────────────────────────── ∨L
Γ, w: (A ∨ B) ⇒ C

Recall the ∨E rule of natural deduction in localised form:

Γ ⊢ A ∨ B    Γ, u:A ⊢ C    Γ, v:B ⊢ C
─────────────────────────────────────── ∨E
Γ ⊢ C

The proposition A ∨ B, which is the succedent of a premise in ∨E, turns into a hypothesis of the conclusion in the left rule ∨L. Thus, left rules can be seen as a sort of inverted elimination rule. This observation can be illustrated as follows:

 ────── hyp
 |
 | elim. rules
 |
 ↓
 ────────────────────── ↑↓ meet
 ↑
 |
 | intro. rules
 |
 conclusion

 ─────────────────────────── init
 ↑            ↑
 |            |
 | left rules | right rules
 |            |
 conclusion

In the sequent calculus, the left and right rules are performed in lock-step until one reaches the initial sequent, which corresponds to the meeting point of elimination and introduction rules in natural deduction. These initial rules are superficially similar to the hypothesis rule of natural deduction, but in the sequent calculus they describe a transposition or a handshake of a left and a right proposition:

────────── init
Γ, u:A ⇒ A

The correspondence between the sequent calculus and natural deduction is a pair of soundness and completeness theorems, which are both provable by means of an inductive argument.

Soundness of ⇒ wrt. ⊢

If Γ ⇒ A, then Γ ⊢ A.

Completeness of ⇒ wrt. ⊢

If Γ ⊢ A, then Γ ⇒ A.

It is clear by these theorems that the sequent calculus does not change the notion of truth, because the same collection of propositions remain true. Thus, one can use the same proof objects as before in sequent calculus derivations. As an example, consider the conjunctions. The right rule is virtually identical to the introduction rule

Γ ⇒ π1 : A     Γ ⇒ π2 : B
─────────────────────────── ∧R
Γ ⇒ (π1, π2) : A ∧ B

Γ ⊢ π1 : A      Γ ⊢ π2 : B
───────────────────────── ∧I
Γ ⊢ (π1, π2) : A ∧ B

The left rule, however, performs some additional substitutions that are not performed in the corresponding elimination rules.

Γ, u:A ⇒ π : C
──────────────────────────────── ∧L1
Γ, v: (A ∧ B) ⇒ [fst v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E1
Γ ⊢ fst π : A

Γ, u:B ⇒ π : C
──────────────────────────────── ∧L2
Γ, v: (A ∧ B) ⇒ [snd v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E2
Γ ⊢ snd π : B

The kinds of proofs generated in the sequent calculus are therefore rather different from those of natural deduction. The sequent calculus produces proofs in what is known as the β-normal η-long form, which corresponds to a canonical representation of the normal form of the natural deduction proof. If one attempts to describe these proofs using natural deduction itself, one obtains what is called the intercalation calculus (first described by John Byrnes), which can be used to formally define the notion of a normal form for natural deduction.

The substitution theorem of natural deduction takes the form of a structural rule or structural theorem known as cut in the sequent calculus.

Cut (substitution)

This section does not cite any sources. Please help improve this section by adding citations to reliable sources. Unsourced material may be challenged and removed. (May 2024) (Learn how and when to remove this message)

If Γ ⇒ π₁ : A and Γ, u:A ⇒ π₂ : C, then Γ ⇒ [π₁/u] π₂ : C.

In most well behaved logics, cut is unnecessary as an inference rule, though it remains provable as a

See also

Notes

References

General references

• Barker-Plummer, Dave;
  ISBN 978-1575866321
  .
• Gallier, Jean (2005). "Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi". Retrieved 12 June 2014.
• S2CID 121546341
  . (English translation Investigations into Logical Deduction in M. E. Szabo. The Collected Works of Gerhard Gentzen. North-Holland Publishing Company, 1969.)
• S2CID 186239837
  .
• Girard, Jean-Yves (1990). Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, England. Archived from the original on 2016-07-04. Retrieved 2006-04-20. Translated and with appendices by Paul Taylor and Yves Lafont.
• Jaśkowski, Stanisław (1934). On the rules of suppositions in formal logic. Reprinted in Polish logic 1920–39, ed. Storrs McCall.
• ISBN 978-0-7204-2103-3
  .
• ISBN 978-0-923891-57-2
  .
• ISBN 978-0-486-42533-7
  .
• ISBN 978-0-17-712040-4
  .
• Martin-Löf, Per (1996). "On the meanings of the logical constants and the justifications of the logical laws" (PDF). Nordic Journal of Philosophical Logic. 1 (1): 11–60. Lecture notes to a short course at Università degli Studi di Siena, April 1983.
• Pfenning, Frank; Davies, Rowan (2001). "A judgmental reconstruction of modal logic" (PDF). Mathematical Structures in Computer Science. 11 (4): 511–540.
  S2CID 16467268
  .
• Prawitz, Dag (1965). Natural deduction: A proof-theoretical study. Acta Universitatis Stockholmiensis, Stockholm studies in philosophy 3. Stockholm, Göteborg, Uppsala: Almqvist & Wicksell.
• ISBN 978-0-486-44655-4
  .
• ISBN 978-0-674-55451-1
  .
• ISBN 978-0-674-57176-1
  .
• Simpson, Alex (1993). The proof theory and semantics of intuitionistic modal logic (PDF). University of Edinburgh. PhD thesis.
• Stoll, Robert Roth (1979) [1963]. Set Theory and Logic. Mineola, New York: Dover Publications.
  ISBN 978-0-486-63829-4
  .
• Stouppa, Phiniki (2004). The Design of Modal Proof Theories: The Case of S5. University of Dresden.
  CiteSeerX 10.1.1.140.1858
  . MSc thesis.
• ISBN 978-0-486-40687-9
  .
• ISBN 978-1-4471-4558-5
  .