Editing Natural deduction

{{Short description|Kind of proof calculus}}
{{use dmy dates|date=March 2025}}
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.{{sfn|Indrzejczak}} This contrasts with [[Hilbert system|Hilbert-style systems]], which instead use [[axiom]]s 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 [[David Hilbert|Hilbert]], [[Gottlob Frege|Frege]], and [[Bertrand Russell|Russell]] (see, e.g., [[Hilbert system]]). Such axiomatizations were most famously used by [[Bertrand Russell|Russell]] and [[Alfred North Whitehead|Whitehead]] in their mathematical treatise ''[[Principia Mathematica]]''. Spurred on by a series of seminars in Poland in 1926 by [[Jan Lukasiewicz|Łukasiewicz]] that advocated a more natural treatment of logic, [[Stanisław Jaśkowski|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.{{sfn|Jaśkowski|1934}} His proposals led to different notations such as [[Fitch notation]] or [[Patrick Suppes|Suppes]]' method, for which [[John Lemmon|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]].<ref>{{harvnb|Gentzen|1935a}}, {{harvnb|Gentzen|1935b}}.</ref> The term ''natural deduction'' (or rather, its German equivalent ''natürliches Schließen'') was coined in that paper:

{{verse translation|lang=de|Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein "Kalkül des natürlichen Schließens".{{sfn|Gentzen|1935a|p=176}}|First I wished to construct a formalism that comes as close as possible to actual reasoning. Thus arose a "calculus of natural deduction".}}

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 logic|classical]] and [[intuitionistic logic]]. In a series of seminars in 1961 and 1962 [[Dag Prawitz|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''<ref name=prawitz1965>{{harvnb|Prawitz|1965}}, {{harvnb|Prawitz|2006}}.</ref> was to become a reference work on natural deduction, and included applications for [[modal logic|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 [[Per Martin-Löf|Martin-Löf]]'s description of logical judgments and connectives.{{sfn|Martin-Löf|1996}}

===History of notation styles===
Natural deduction has had a large variety of notation styles,{{sfn|Pelletier|Hazen|2024}} 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 link||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 [https://plato.stanford.edu/archives/spr2024/entries/natural-deduction/ SEP] and [https://iep.utm.edu/natural-deduction/ IEP] for pictures.
* [[Gerhard Gentzen|Gentzen]] invented natural deduction using tree-shaped proofs – see {{section link||Gentzen's tree notation}} for details.
* [[Stanisław Jaśkowski|Jaśkowski]] changed this to a notation that used various nested boxes.{{sfn|Pelletier|Hazen|2024}}
* [[Frederic Fitch|Fitch]] changed Jaśkowski method of drawing the boxes, creating [[Fitch notation]].{{sfn|Pelletier|Hazen|2024}}
* 1940: In a textbook, [[Willard Van Orman Quine|Quine]]<ref>{{harvtxt|Quine|1981}}. See particularly pages 91–93 for Quine's line-number notation for antecedent dependencies.</ref> indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
* 1950: In a textbook, {{harvtxt|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 {{harvtxt|Suppes|1999|pp=25–150}}. This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line.
* 1963: {{harvtxt|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 {{harvtxt|Lemmon|1978}} is an introduction to logic proofs using a method based on that of [[Patrick Suppes|Suppes]], what is now known as [[Suppes–Lemmon notation]].
* 1967: In a textbook, {{harvtxt|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.{{refn|A particular advantage of Kleene's tabular natural deduction systems is that he proves the validity of the inference rules for both propositional calculus and predicate calculus. See {{harvnb|Kleene|2002|pp=44–45, 118–119}}.}}

==Notation==
Here is a table with the most common notational variants for [[logical connective]]s.
{| class="wikitable"
|+ Notational variants of the connectives{{sfn|von Plato|2013|p=9}}{{sfn|Weisstein}}
|-
! Connective
! Symbol
|-
| [[Logical conjunction|AND]]
| <math>A \land B</math>, <math>A \cdot B</math>, <math>AB</math>, <math>A \& B</math>, <math>A \&\& B</math>
|-
| [[Logical biconditional|equivalent]]
| <math>A \equiv B</math>, <math>A \Leftrightarrow B</math>, <math>A \leftrightharpoons B</math>
|-
| [[Material conditional|implies]]
| <math>A \Rightarrow B</math>, <math>A \supset B</math>, <math>A \rightarrow B</math>
|-
| [[Sheffer stroke|NAND]]
| <math>A \overline{\land} B</math>, <math>A \mid B</math>, <math>\overline{A \cdot B}</math>
|-
| nonequivalent
| <math>A \not\equiv B</math>, <math>A \not\Leftrightarrow B</math>, <math>A \nleftrightarrow B</math>
|-
| [[Logical NOR|NOR]]
| <math>A \overline{\lor} B</math>, <math>A \downarrow B</math>, <math>\overline{A+B}</math>
|-
| [[Negation|NOT]]
| <math>\neg A</math>, <math>-A</math>, <math>\overline{A}</math>, <math>\sim A</math>
|-
| [[Logical disjunction|OR]]
| <math>A \lor B</math>, <math>A + B</math>, <math>A \mid B</math>, <math>A \parallel B</math>
|-
| [[XNOR gate|XNOR]]
| <math>A</math> XNOR <math>B</math>
|-
| [[Exclusive or|XOR]]
| <math>A \underline{\lor} B</math>, <math>A \oplus B</math>
|}

===Gentzen's tree notation===

[[Gerhard Gentzen|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 calculus|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:

:<math>1) ~ P \to Q</math>
:<math>2) ~ P</math>
:<math>\therefore ~ Q</math>

In Gentzen's notation,{{sfn|Pelletier|Hazen|2024}} this would be written like this:

:<math>\frac{P \to Q, P}{Q}</math>

The premises are shown above a line, called the '''inference line''',{{sfn|von Plato|2013|pp=9,32,121}}{{sfn|Sutcliffe}} separated by a '''comma''', which indicates ''combination'' of premises.{{sfn|Restall|2018}} The conclusion is written below the inference line.{{sfn|von Plato|2013|pp=9,32,121}} The inference line represents ''syntactic consequence'',{{sfn|von Plato|2013|pp=9,32,121}} sometimes called ''deductive consequence'',{{sfn|Magnus|Button|Trueman|Zach|2023|loc=CHAPTER 20, Proof-theoretic concepts|p=142}}{{sfn|Paseau|Leek}} which is also symbolized with ⊢.{{sfn|Paseau|Leek}} So the above can also be written in one line as <math>P \to Q, P \vdash Q</math>. (The turnstile, for syntactic consequence, is of lower [[Order of operations|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.){{sfn|Restall|2018}}

Syntactic consequence is contrasted with ''semantic consequence'',{{sfn|Paseau|Pregel|2023}} which is symbolized with ⊧.{{sfn|Magnus|Button|Trueman|Zach|2023|loc=12.5 The double turnstile|p=82}}{{sfn|Paseau|Leek}} In this case, the conclusion follows ''syntactically'' because natural deduction is a [[Propositional calculus#Syntactic proof systems|syntactic proof system]], which assumes [[inference rules]] [[Postulate|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 [[sequent]]s ''Γ ⊢A'' instead of a tree of judgments that A (is true).

=== Suppes–Lemmon notation ===
Many textbooks use [[Suppes–Lemmon notation]],{{sfn|Pelletier|Hazen|2024}} so this article will also give that – although as of now, this is only included for [[Propositional calculus|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,{{sfn|Allen|Hand|2022}} where each sentence is either an assumption, or the result of applying a rule of proof to earlier sentences in the sequence.{{sfn|Allen|Hand|2022}} Each '''line of proof''' is made up of a '''sentence of proof''', together with its '''annotation''', its '''assumption set''', and the current '''line number'''.{{sfn|Allen|Hand|2022}} The assumption set lists the assumptions on which the given sentence of proof depends, which are referenced by the line numbers.{{sfn|Allen|Hand|2022}} The annotation specifies which rule of proof was applied, and to which earlier lines, to yield the current sentence.{{sfn|Allen|Hand|2022}} Here's an example proof:
{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|<math>P \to Q, \neg Q \vdash \neg P</math>
|+Suppes–Lemmon style proof (first example)
|-
!Assumption set
!Line number
!Formula (''wff'')
!Annotation
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|<math>P \to Q</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|<math>\neg Q</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|<math>P</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|1, 3
|bgcolor="#bbffbb"|4
|bgcolor="#bbffbb"|<math>Q</math>
|bgcolor="#bbffbb"|1, 3 →E
|-
|bgcolor="#bbffbb"|1, 2
|bgcolor="#bbffbb"|5
|bgcolor="#bbffbb"|<math>\neg P</math>
|bgcolor="#bbffbb"|2, 4 RAA
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D
|-
|}
This proof will become clearer when the inference rules and their appropriate annotations are specified – see {{section link||Propositional inference rules (Suppes–Lemmon style)}}.

==Propositional language syntax==
{{Main|Propositional calculus#Syntax}}This section defines the [[formal syntax]] for a [[Propositional calculus#Language|propositional logic language]], contrasting the common ways of doing so with a Gentzen-style way of doing so.

=== Common definition styles ===
In [[classical logic|classical]] [[propositional calculus]] the [[formal language]] <math>\mathcal{L}</math> is usually defined (here: by [[recursive definition|recursion]]) as follows:{{sfn|Allen|Hand|2022|p=12}}

# Each [[propositional variable]] is a [[Well-formed formula|formula]].
# "<math>\bot</math>" is a formula.
# If <math>\varphi</math> and <math>\psi</math> are formulae, so are <math>(\varphi \land \psi)</math>, <math>(\varphi \lor \psi)</math>, <math>(\varphi \to \psi)</math>, <math>(\varphi \leftrightarrow \psi)</math>.
# Nothing else is a formula.

[[Negation]] (<math>\neg</math>) is defined as implication to [[False (logic)#False, negation and contradiction|falsity]]
:<math>\neg \phi \; \overset{\text{def}}{=} \; \phi \to \bot</math>,
where <math>\bot</math> (falsum) represents a contradiction or absolute falsehood.{{sfn|Kleene|2002}}{{sfn|Prawitz|1965}}{{sfn|von Plato|2013|p=18}}{{sfn|Van Dalen|2013}}{{sfn|Hansson|Hendricks|2018|p=179}}

Older publications, and publications that do not focus on logical systems like [[minimal logic|minimal]], [[intuitionistic logic|intuitionistic]] or [[Hilbert system]]s, take negation as a primitive [[logical connective]], meaning it is assumed as a basic operation and not defined in terms of other connectives.{{sfn|Ayala-Rincón|de Moura|2017|pages=2,20}}{{sfn|Hansson|Hendricks|2018|p=38}} Some authors, such as [[David Bostock (philosopher)|Bostock]], use <math>\bot</math> and <math>\top</math>, and also define <math>\neg</math> as primitives.{{sfn|Bostock|1997|p=21}}<ref>This is required in [[paraconsistent logic]]s that do not treat <math>\neg</math> and <math>(\phi \to \bot)</math> as equivalents.</ref>

=== Gentzen-style definition ===
A syntax definition can also be given using {{section link||Gentzen's tree notation}}, by writing well-formed formulas below the inference line and any schematic variables used by those formulas above it.{{sfn|Ayala-Rincón|de Moura|2017|pages=2,20}} For instance, the equivalent of rules 3 and 4, from Bostock's definition above, is written as follows:

:<math>\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)}</math>.

A different notational convention sees the language's syntax as a [[categorial grammar]] with the single category "formula", denoted by the symbol <math>\mathcal{F}</math>. So any elements of the syntax are introduced by categorizations, for which the notation is <math>\varphi : \mathcal{F}</math>, meaning "<math>\varphi</math> is an expression for an object in the category <math>\mathcal{F}</math>."{{sfn|von Plato|2013|pages=12–13}} The sentence-letters, then, are introduced by categorizations such as <math>P : \mathcal{F}</math>, <math>Q : \mathcal{F}</math>, <math>R : \mathcal{F}</math>, and so on;{{sfn|von Plato|2013|pages=12–13}} the connectives, in turn, are defined by statements similar to the above, but using categorization notation, as seen below:
{| class="wikitable"
|+ '''Connectives defined through a categorial grammar{{sfn|von Plato|2013|pages=12–13}}'''
|-
! style="text-align: center;" | '''Conjunction (&)'''
! style="text-align: center;" | '''Disjunction (∨)'''
! style="text-align: center;" | '''Implication (→)'''
! style="text-align: center;" | '''Negation (¬)'''
|-
| <math>\frac{A : \mathcal{F} \quad B : \mathcal{F}}{\&(A)(B) : \mathcal{F}}</math>
| <math>\frac{A : \mathcal{F} \quad B : \mathcal{F}}{\vee(A)(B) : \mathcal{F}}</math>
| <math>\frac{A : \mathcal{F} \quad B : \mathcal{F}}{\supset(A)(B) : \mathcal{F}}</math>
| <math>\frac{A : \mathcal{F}}{\neg(A) : \mathcal{F}}</math>
|}
In the rest of this article, the <math>\varphi : \mathcal{F}</math> 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 <math>\mathcal{L}</math> be inductively defined as <math>\Phi ::= p_1, p_2, \dots \mid \bot \mid (\Phi \to \Phi) \mid (\Phi \land \Phi) \mid (\Phi \lor \Phi)</math>.

Define negation as <math>\neg \Phi \, \overset{\text{def}}{=} \, (\Phi \to \bot)</math>.

The following is a list of primitive inference rules for natural deduction in propositional logic{{sfn|Prawitz|1965|p=20}}{{sfn|Ayala-Rincón|de Moura|2017|pages=2,20}}

{| class="wikitable"
|+ Rules for propositional logic
! Introduction rules
! Elimination rules
|-
| <math>\begin{array}{c}
\varphi \qquad \psi \\
\hline
\varphi \land \psi 
\end{array} (\land_I)</math>
| <math>\begin{array}{c}
\varphi \land \psi \\
\hline
\varphi 
\end{array} (\land_E)</math>
|-
| <math>\begin{array}{c}
\varphi \\
\hline
\varphi \lor \psi 
\end{array} (\lor_I)</math>
| <math>
\cfrac{
 \varphi \lor \psi
 \quad
 \begin{matrix}
 [\varphi]^u \\
 \vdots \\
 \chi
 \end{matrix}
 \quad
 \begin{matrix}
 [\psi]^v \\
 \vdots \\
 \chi
 \end{matrix}
}{\chi}\ \lor_{E^{u,v}}
</math>
|-
| <math>\begin{array}{c}
[\varphi]^u \\
\vdots \\
\psi \\
\hline
\varphi \to \psi 
\end{array} (\to_I) \ u</math>
| <math>\begin{array}{c}
\varphi \qquad \varphi \to \psi \\
\hline
\psi 
\end{array} (\to_E)</math>
|-
|
|<math>\begin{array}{c}
\bot \\
\hline
\varphi 
\end{array} (\bot_E)</math>
|-
|
|<ref name="RAA"/> <math>\begin{array}{c}
(\varphi \to \bot ) \to \bot \\
\hline
\varphi
\end{array} (\neg\neg_E)</math>
|}
In this table the Greek letters <math>\varphi, \psi, \chi</math> are ''[[Propositional calculus#Constants and schemata|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 <math>\land_I</math>, which is short for "conjunction introduction".

* '''[[Minimal logic]]''': the natural deduction rules are <math>ND_{MPC} = \{ \land_I, \land_E, \lor_I, \lor_E, \to_I, \to_E \}</math>.
:Whithout the rules <math>\bot_E</math> and <math>\neg\neg_E</math> the system defines minimal logic (as discussed by [[Ingebrigt Johansson|Johansson]]).{{sfn|Johansson|1937}}
* '''[[Intuitionistic logic]]''': the natural deduction rules are <math>ND_{IPC} = ND_{MPC} \cup \{ \bot_E \}</math>.
:When the rule <math>\bot_E</math> ([[principle of explosion]]) is added to the rules for minimal logic, the system defines intuitionistic logic.
:The statement <math>P \to \neg \neg P</math> 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 <math>ND_{CPC} = ND_{IPC} \cup \{ \neg\neg_E \}</math>.{{refn|name="RAA"|Instead of <math>\neg\neg</math>E one can add '''[[reductio ad absurdum]]''' as a rule to obtain classical logic:{{sfn|Prawitz|1965|p=21}}{{sfn|Ayala-Rincón|de Moura|2017|pp=17-24}}
:<math>
\frac{\begin{array}{c}
[\varphi \to \bot] \\
\vdots \\
\bot
\end{array}}{\varphi}</math> (RAA)}}
:When all listed natural deduction rules are admitted, the system defines classical logic.{{sfn|Prawitz|1965|p=21}}{{sfn|Ayala-Rincón|de Moura|2017|pp=17-24}}{{sfn|Tennant|1990|p=48}}

=== Gentzen-style example proofs ===
'''Example 1''':{{sfn|Van Dalen|2013}} Proof, whithin minimal logic, of <math> P \to \neg \neg P</math>.

Goal: <math>P \to ((P \to \bot) \to \bot)</math><br/>
Proof:
:<math>
\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}
</math>

'''Example 2''': Proof, whithin minimal logic, of <math>A \to \left ( B \to \left ( A \land B \right ) \right )</math>:
:<math>
 \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}
 </math>

== Fitch-style propositional logic ==
{{main|Fitch notation}}
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]]{{sfn|Suppes|1999}} and [[John Lemmon|E. J. Lemmon]]{{sfn|Lemmon|1978}} 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 ==
{{main|Suppes–Lemmon notation}}

=== 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.{{sfn|Suppes|1999}}
* He defined negation in terms of contradiction: <math>\neg P \equiv (P \to \bot)</math>.
* 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.{{sfn|Lemmon|1978}} He as well defined negation as implication to falsity: <math>\neg P \equiv P \to \bot</math>. This is not stated as a formal definition in ''Beginning Logic'', but it is implicitly assumed throughout the system. Here's how we know:
* Use of RAA (Reductio ad Absurdum): Lemmon regularly used RAA in the form: Assume <math>P</math>, derive <math>\bot</math>, then conclude <math>\neg P</math>.
: This only works if <math>\neg P</math> is understood as <math>P \to \bot</math>.
* Proofs involving contradiction: Lemmon used the fact that from <math>\neg P \land P</math> one can derive <math>\bot</math>.
: This requires treating <math>\neg P</math> as <math>P \to \bot</math>, 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){{sfn|Lemmon|1978|pages=passim, especially 39-40}} and Allen & Hand (2022),{{sfn|Allen|Hand|2022}} Lemmon's <span style="background-color: yellow;">derived rules</span> are highlighted. They can be derived from the (non-highlighted) [[Gerhard Gentzen|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.<ref name="RAA"/>{{sfn|Allen|Hand|2022}} ''Disjunctive Syllogism'' can be used as an easier alternative to the proper ∨-elimination,{{sfn|Allen|Hand|2022}} and MTT is a commonly given rule,{{sfn|Lemmon|1978|pages=passim, especially 39-40}} although it is not primitive.{{sfn|Allen|Hand|2022}}

{| class="wikitable" style="margin:auto;"
|+ List of Inference Rules
|-
! Rule Name
! Alternative names
! Annotation
! Assumption set
! Statement
|-
| Rule of Assumptions 
| Assumption
| '''A'''
| The current line number.
| At any stage of the argument, introduce a proposition as an assumption of the argument.
|-
| Conjunction introduction 
| Ampersand introduction, conjunction (CONJ){{sfn|Arthur|2017}} 
| '''m, n &I''' 
| The union of the assumption sets at lines '''m''' and '''n'''.
| From <math>\varphi</math> and <math>\psi</math> at lines '''m''' and '''n''', infer <math>\varphi \land \psi</math>.
|-
| Conjunction elimination 
| Simplification (S), ampersand elimination
| '''m &E''' 
| The same as at line '''m'''.
| From <math>\varphi \land \psi</math> at line '''m''', infer <math>\varphi</math> and <math>\psi</math>.
|-
| Disjunction introduction
| Addition (ADD)
| '''m ∨I''' 
| The same as at line '''m'''.
| From <math>\varphi</math> at line '''m''', infer <math>\varphi \lor \psi</math>, whatever <math>\psi</math> may be.
|-
| Disjunction elimination 
| Wedge elimination, dilemma (DL){{sfn|Arthur|2017}}
| '''j,k,l,m,n ∨E''' 
| The lines '''j,k,l,m,n'''.
| From <math>\varphi \lor \psi</math> at line '''j''', and an assumption of <math>\varphi</math> at line '''k''', and a derivation of <math>\chi</math> from <math>\varphi</math> at line '''l''', and an assumption of <math>\psi</math> at line '''m''', and a derivation of <math>\chi</math> from <math>\psi</math> at line '''n''', infer <math>\chi</math>. 
|-
| Arrow introduction
| Conditional proof (CP),{{sfn|Arthur|2017}} conditional introduction 
| '''n, →I (m)''' 
| Everything in the assumption set at line '''n''', excepting '''m''', the line where the antecedent was assumed.
| From <math>\psi</math> at line '''n''', following from the assumption of <math>\varphi</math> at line '''m''', infer <math>\varphi \to \psi</math>.
|-
| Arrow elimination
| Modus ponendo ponens (MPP), modus ponens (MP),{{sfn|Arthur|2017}} conditional elimination 
| '''m, n →E''' 
| The union of the assumption sets at lines '''m''' and '''n'''.
| From <math>\varphi \to \psi</math> at line '''m''', and <math>\varphi</math> at line '''n''', infer <math>\psi</math>. 
|-
| Double negation{{sfn|Arthur|2017}} 
| Double negation elimination 
| '''m DN''' 
| The same as at line '''m'''.
| From <math>\neg \neg \varphi</math> at line '''m''', infer <math>\varphi</math>.
|-
| Reductio ad absurdum
| Indirect Proof (IP), negation introduction (¬I), negation elimination (¬E) 
| '''m,'''&nbsp;'''n'''&nbsp;'''RAA'''&nbsp;'''(k)''' 
| The union of the assumption sets at lines '''m''' and '''n''', excluding '''k''' (the denied assumption). 
| From a sentence and its denial{{refn|To simplify the statement of the rule, the word "denial" here is used in this way: the ''denial'' of a formula <math>\varphi</math> that is not a ''negation'' is <math>\neg \varphi</math>, whereas a ''negation'', <math>\neg \varphi</math>, has two ''denials'', viz., <math>\varphi</math> and <math>\neg \neg \varphi</math>. at lines '''m''' and '''n''', infer the denial of any assumption appearing in the proof (at line '''k''').
|-
| bgcolor="yellow"|Disjunctive Syllogism 
| bgcolor="yellow"|Wedge elimination (∨E), modus tollendo ponens (MTP) 
| bgcolor="yellow"|'''m,n DS''' 
| bgcolor="yellow"|The union of the assumption sets at lines '''m''' and '''n'''.
| bgcolor="yellow"|From <math>\varphi \lor \psi</math> at line '''m''' and <math>\neg \varphi</math> at line '''n''', infer <math>\psi</math><br/>From <math>\varphi \lor \psi</math> at line '''m''' and <math>\neg \psi</math> at line '''n''', infer <math>\varphi</math>.
|-
| bgcolor="yellow"|Double arrow introduction
| bgcolor="yellow"|Biconditional definition (''Df'' <math>\leftrightarrow</math>), biconditional introduction 
| bgcolor="yellow"| '''m, n <math>\leftrightarrow</math>I''' 
| bgcolor="yellow"|The union of the assumption sets at lines '''m''' and '''n'''.
| bgcolor="yellow"| From <math>\varphi \to \psi</math> and <math>\psi \to \varphi</math> at lines '''m''' and '''n''', infer <math>\varphi \leftrightarrow \psi</math>.
|-
| bgcolor="yellow"| Double arrow elimination
| bgcolor="yellow"| Biconditional definition (''Df'' <math>\leftrightarrow</math>), biconditional elimination 
| bgcolor="yellow"| '''m <math>\leftrightarrow</math>E''' 
| bgcolor="yellow"|The same as at line '''m'''.
| bgcolor="yellow"| From <math>\varphi \leftrightarrow \psi</math> at line '''m''', infer either <math>\varphi \to \psi</math> or <math>\psi \to \varphi</math>.
|-
| bgcolor="yellow"| Modus tollendo tollens 
| bgcolor="yellow"| Modus tollens (MT)
| bgcolor="yellow"| '''m, n MTT''' 
| bgcolor="yellow"| The union of the assumption sets at lines '''m''' and '''n'''.
| bgcolor="yellow"| From <math>\varphi \to \psi</math> at line '''m''', and <math>\neg \psi</math> at line '''n''', infer <math>\neg \varphi</math>.
|}

=== Suppes–Lemmon-style examples proof ===
Recall that an example proof was already given when introducing {{section link||Suppes–Lemmon notation}}. This is a second example.

==== Example 2 ====
{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|<math>P \lor Q, \neg P, \neg P \to \neg Q \vdash \bot</math> contradiction
|+Suppes–Lemmon style proof (second example)
|-
! Assumption set
! Line number
! Formula
! Annotation
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|<math>P \lor Q</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|<math>\neg P</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|<math>\neg P \to \neg Q</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|2,3
|bgcolor="#bbffbb"|4
|bgcolor="#bbffbb"|<math>\neg Q</math>
|bgcolor="#bbffbb"|2, 3 →E
|-
|bgcolor="#bbffbb"|1,2,3
|bgcolor="#bbffbb"|5
|bgcolor="#bbffbb"|<math>P</math>
|bgcolor="#bbffbb"|A (subproof)
|-
|bgcolor="#bbffbb"|1,2,3,5
|bgcolor="#bbffbb"|6
|bgcolor="#bbffbb"|<math>\bot</math>
|bgcolor="#bbffbb"|2, 5 RAA<ref name="undocumentedRAA">This is not conform the RAA rule. The rule which is implicitly applied is →E on <math>\varphi, \varphi \to \bot</math>. As negation is not defined as an implication, this modus ponens is undocumented.</ref>
|-
|bgcolor="#bbffbb"|1,2,3
|bgcolor="#bbffbb"|7
|bgcolor="#bbffbb"|<math>Q</math>
|bgcolor="#bbffbb"|A (subproof)
|-
|bgcolor="#bbffbb"|1,2,3,7
|bgcolor="#bbffbb"|8
|bgcolor="#bbffbb"|<math>\bot</math>
|bgcolor="#bbffbb"|4, 7 RAA<ref name="undocumentedRAA"/>
|-
|bgcolor="#bbffbb"|1,2,3
|bgcolor="#bbffbb"|9
|bgcolor="#bbffbb"|<math>\bot</math>
|bgcolor="#bbffbb"|1, 5–6, 7–8 vE
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D.
|}

==== Example 3 ====
The next derivation proves two theorems:
* lines 1 - 8 prove '''within minimal logic''':
:<math>\vdash _{MPC} \neg \neg (P \lor \neg P)</math>.
* lines 1 - 9 prove '''within classical logic''':
:<math>\vdash _{CPC} P \lor \neg P</math>.

Goals:
* lines 1 - 8: <math>\vdash _{MPC} ((P \lor ( P \to \bot)) \to \bot ) \to \bot</math>.
* lines 1 - 9: <math>\vdash _{CPC} P \lor ( P \to \bot )</math>.
{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|<math>\vdash P \lor \neg P</math>
|+Suppes–Lemmon style proof (third example)
|-
! Assumption set
! Line number
! Formula
! Annotation
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|<math>(P \lor ( P \to \bot)) \to \bot</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|1, 2
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|<math>P</math>
|bgcolor="#bbffbb"|A
|-
|bgcolor="#bbffbb"|1, 2
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|<math>P \lor ( P \to \bot)</math>
|bgcolor="#bbffbb"|2, ∨I
|-
|bgcolor="#bbffbb"|1, 2
|bgcolor="#bbffbb"|4
|bgcolor="#bbffbb"|<math>\bot</math>
|bgcolor="#bbffbb"|1, 3, →E
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|5
|bgcolor="#bbffbb"|<math>P \to \bot</math>
|bgcolor="#bbffbb"|2, 4, →I (discharging 2)
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|6
|bgcolor="#bbffbb"|<math>P \lor ( P \to \bot)</math>
|bgcolor="#bbffbb"|5, ∨I
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|7
|bgcolor="#bbffbb"|<math>\bot</math>
|bgcolor="#bbffbb"|1, 6, →E
|-
|bgcolor="#bbffbb"|∅
|bgcolor="#bbffbb"|8
|bgcolor="#bbffbb"|<math>((P \lor ( P \to \bot)) \to \bot ) \to \bot</math> 
|bgcolor="#bbffbb"|1, 7, →I (discharging 1)
|-
|bgcolor="#bbffbb"|∅
|bgcolor="#bbffbb"|9
|bgcolor="#bbffbb"|<math>P \lor ( P \to \bot )</math> 
|bgcolor="#bbffbb"|8, DN
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D
|}
'''Remark''': [[Valery Glivenko]] [[Double-negation_translation#Propositional_logic|proved]] the following theorem:
:If <math>\varphi</math> is a [[propositional formula]], then <math>\varphi</math> is a classical [[tautology (logic)|tautology]] [[if and only if]] <math>\neg \neg \varphi</math> is an intuitionistic tautology.

This implies that all classical propositional theorems <math>\varphi</math> can be proved like in this example:
# Prove <math>\neg \neg \varphi</math> within intuitionistic logic (i.e. without <math>\neg\neg_E</math>).
# Apply <math>\neg\neg_E</math> to get <math>\varphi</math> from <math>\neg \neg \varphi</math>.

==Consistency, completeness, and normal forms==
{{Unreferenced section|date=May 2024}}
A [[theory (mathematical logic)|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 theory|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.
:<math>\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</math>

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:
:<math>\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}</math>

These notions correspond exactly to [[Lambda calculus#.CE.B2-reduction|β-reduction (beta reduction)]] and [[Lambda calculus#.CE.B7-conversion|η-conversion (eta conversion)]] in the [[lambda calculus]], using the [[Curry&ndash;Howard isomorphism]]. By local completeness, we see that every derivation can be converted to an equivalent derivation where the principal connective is introduced. In fact, if the entire derivation obeys this ordering of eliminations followed by introductions, then it is said to be ''normal''. In a normal derivation all eliminations happen above introductions. In most logics, every derivation has an equivalent normal derivation, called a ''[[normal form (abstract rewriting)|normal form]]''. The existence of normal forms is generally hard to prove using natural deduction alone, though such accounts do exist in the literature, most notably by [[Dag Prawitz]] in 1961.<ref>See also his book {{harvnb|Prawitz|1965}}, {{harvnb|Prawitz|2006}}.</ref> It is much easier to show this indirectly by means of a [[cut elimination|cut-free]] [[sequent calculus]] presentation.

==First and higher-order extensions==
{{Unreferenced section|date=May 2024}}
[[File:first order natural deduction.png|thumb|right|Summary of first-order system]]

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 ''[[term (logic)|terms]]''. More precisely, we will add a new category, "term", denoted <math>\mathcal{T}</math>. We shall fix a [[countable]] set ''<math>V</math>'' of ''variables'', another countable set <math>F</math> of ''function symbols'', and construct terms with the following formation rules:

:<math>
\frac{v\in V}{v : \mathcal{T}} \hbox{ var}_F
</math>

and
:<math>
\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
</math>

For propositions, we consider a third countable set ''P'' of ''[[Predicate (mathematical logic)|predicates]]'', and define ''atomic predicates over terms'' with the following formation rule:

:<math>
\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
</math>

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 ''[[quantifier (logic)|quantified]]'' propositions; one for universal (∀) and existential (∃) quantification:

:<math>
\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
</math>

The [[universal quantifier]] has the introduction and elimination rules:

:<math>

\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}
</math>

The [[existential quantifier]] has the introduction and elimination rules:
:<math>
\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}}
</math>

In these rules, the notation [''t''/''x''] ''A'' stands for the substitution of ''t'' for every (visible) instance of ''x'' in ''A'', avoiding capture.{{refn|See the article on [[lambda calculus]] for more detail about the concept of substitution.}} 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 [[Decidability (logic)|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:

:<math>
\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}
</math>

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==
{{Unreferenced section|date=May 2024}}
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 (symbol)|turnstile]]'' (⊢). This modification sometimes goes under the name of ''localised hypotheses''. The following diagram summarises the change.
{| style="margin-left: 2em;"
|-
|
 ──── u<sub>1</sub> ──── u<sub>2</sub> ... ──── u<sub>n</sub>
  J<sub>1</sub>      J<sub>2</sub>          J<sub>n</sub>
               ⋮
               J
| width="10%" align="center" | ⇒ || 
 u<sub>1</sub>:J<sub>1</sub>, u<sub>2</sub>:J<sub>2</sub>, ..., u<sub>n</sub>:J<sub>n</sub> ⊢ 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.
{| style="margin-left: 2em;"
|-
|
 u ∈ V
 ─────── proof-F
 u proof
| width="10%" |  ||
 ───────────────────── 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:
{| style="margin-left: 2em;"
|-
|
 π<sub>1</sub> proof    π<sub>2</sub> proof
 ──────────────────── pair-F
 (π<sub>1</sub>, π<sub>2</sub>) proof
| width="10%" |  || 
 Γ ⊢ π<sub>1</sub> : A    Γ ⊢ π<sub>2</sub> : B
 ───────────────────────── ∧I
 Γ ⊢ (π<sub>1</sub>, π<sub>2</sub>) : A ∧ B
|}
The elimination rules ∧E<sub>1</sub> and ∧E<sub>2</sub> select either the left or the right conjunct; thus the proofs are a pair of projections&mdash;first ('''fst''') and second ('''snd''').
{| style="margin-left: 2em;"
|-
|
 π proof
 ─────────── '''fst'''-F
 '''fst''' π proof
| width="10%" |  || 
 Γ ⊢ π : A ∧ B
 ───────────── ∧E<sub>1</sub>
 Γ ⊢ '''fst''' π : A
|-
|
 π proof
 ─────────── '''snd'''-F
 '''snd''' π proof
| width="10%" |  || 
 Γ ⊢ π : A ∧ B
 ───────────── ∧E<sub>2</sub>
 Γ ⊢ '''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''.
{| style="margin-left: 2em;"
|-
|
 π proof
 ──────────── λ-F
 λu. π proof
| width="10%" |  || 
 Γ, u:A ⊢ π : B
 ───────────────── ⊃I
 Γ ⊢ λu. π : A ⊃ B
|-
|
 π<sub>1</sub> proof   π<sub>2</sub> proof
 ─────────────────── app-F
 π<sub>1</sub> π<sub>2</sub> proof
| width="10%" |  || 
 Γ ⊢ π<sub>1</sub> : A ⊃ B    Γ ⊢ π<sub>2</sub> : A
 ──────────────────────────── ⊃E
 Γ ⊢ π<sub>1</sub> π<sub>2</sub> : 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 [[mathematical induction|induction]] on the depth (or structure) of the second judgment.

=== Substitution theorem ===
{{Unreferenced section|date=May 2024}}
: ''If'' Γ ⊢ π<sub>1</sub> : ''A'' ''and'' Γ, ''u'':''A'' ⊢ π<sub>2</sub> : ''B'', ''then'' Γ ⊢ [π<sub>1</sub>/''u''] π<sub>2</sub> : 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 type|product]] (×), implication as the function [[function type|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 ''[[normalization property (abstract rewriting)|normalising]]'' (or ''weakly normalising''). If the canonical form is unique, then the theory is said to be ''strongly normalising''. Normalisability is a rare feature of most non-trivial type theories, which is a big departure from the logical world. (Recall that almost every logical derivation has an equivalent normal derivation.) To sketch the reason: in type theories that admit recursive definitions, it is possible to write programs that never reduce to a value; such looping programs can generally be given any type. In particular, the looping program has type ⊥, although there is no logical proof of "⊥". For this reason, the ''propositions as types; proofs as programs'' paradigm only works in one direction, if at all: interpreting a type theory as a logic generally gives an inconsistent logic.

===Example: Dependent Type Theory===
{{Unreferenced section|date=May 2024}}
Like logic, type theory has many extensions and variants, including first-order and higher-order versions. One branch, known as [[dependent type theory]], is used in a number of [[computer-assisted proof]] systems.  Dependent type theory allows quantifiers to range over programs themselves. These quantified types are written as Π and Σ instead of ∀ and ∃, and have the following formation rules:
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ A type    Γ, x:A ⊢ B type
 ───────────────────────────── Π-F
 Γ ⊢ Πx:A. B type
| width="10%" |  || 
 Γ ⊢ A type  Γ, x:A ⊢ B type
 ──────────────────────────── Σ-F
 Γ ⊢ Σx:A. B type
|}
These types are generalisations of the arrow and product types, respectively, as witnessed by their introduction and elimination rules.
{| style="margin-left: 2em;"
|-
|
 Γ, x:A ⊢ π : B
 ──────────────────── ΠI
 Γ ⊢ λx. π : Πx:A. B
| width="10%" |  || 
 Γ ⊢ π<sub>1</sub> : Πx:A. B   Γ ⊢ π<sub>2</sub> : A
 ───────────────────────────── ΠE
 Γ ⊢ π<sub>1</sub> π<sub>2</sub> : [π<sub>2</sub>/x] B
|}
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ π<sub>1</sub> : A    Γ, x:A ⊢ π<sub>2</sub> : B
 ───────────────────────────── ΣI
 Γ ⊢ (π<sub>1</sub>, π<sub>2</sub>) : Σx:A. B
| width="10%" |  || 
 Γ ⊢ π : Σx:A. B
 ──────────────── ΣE<sub>1</sub>
 Γ ⊢ '''fst''' π : A
|}
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ π : Σx:A. B
 ──────────────────────── ΣE<sub>2</sub>
 Γ ⊢ '''snd''' π : ['''fst''' π/x] B
|}
Dependent type theory in full generality is very powerful: it is able to express almost any conceivable property of programs directly in the types of the program. This generality comes at a steep price &mdash; either typechecking is undecidable ([[extensional type theory]]), or extensional reasoning is more difficult ([[intensional type theory]]). For this reason, some dependent type theories do not allow quantification over arbitrary programs, but rather restrict to programs of a given decidable ''index domain'', for example integers, strings, or linear programs.

Since dependent type theories allow types to depend on programs, a natural question to ask is whether it is possible for programs to depend on types, or any other combination. There are many kinds of answers to such questions. A popular approach in type theory is to allow programs to be quantified over types, also known as ''[[parametric polymorphism]]''; of this there are two main kinds: if types and programs are kept separate, then one obtains a somewhat more well-behaved system called ''[[predicative polymorphism]]''; if the distinction between program and type is blurred, one obtains the type-theoretic analogue of higher-order logic, also known as ''[[impredicative polymorphism]]''. Various combinations of dependency and polymorphism have been considered in the literature, the most famous being the [[lambda cube]] of [[Henk Barendregt]].

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 [[logical framework]]. Popular modern logical frameworks such as the [[calculus of constructions]] and [[LF (logical framework)|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==
{{Unreferenced section|date=May 2024}}
For simplicity, the logics presented so far have been [[intuitionistic logic|intuitionistic]]. [[Classical logic]] extends intuitionistic logic with an additional [[axiom]] or principle of [[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 [[David Hilbert|Hilbert]] and [[Arend Heyting|Heyting]]:
{| style="margin-left: 2em;"
|-
|
 ────────────── XM<sub>1</sub>
 A ∨ ¬A
| width="5%" |  ||
 ¬¬A
 ────────── XM<sub>2</sub>
 A
| width="5%" |  ||
 ──────── ''u''
 ¬A
 ⋮
 ''p''
 ────── XM<sub>3</sub><sup>''u, p''</sup>
 A
|}

(XM<sub>3</sub> is merely XM<sub>2</sub> 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 [[Michel Parigot|Parigot]] in 1992 in the form of a classical [[lambda calculus]] called [[Lambda-mu calculus|λμ]]. The key insight of his approach was to replace a truth-centric judgment ''A'' with a more classical notion, reminiscent of the [[sequent calculus]]: in localised form, instead of Γ ⊢ ''A'', he used Γ ⊢ Δ, with Δ a collection of propositions similar to Γ. Γ was treated as a conjunction, and Δ as a disjunction. This structure is essentially lifted directly from classical [[sequent calculus|sequent calculi]], but the innovation in λμ was to give a computational meaning to classical natural deduction proofs in terms of a [[callcc]] or a throw/catch mechanism seen in [[LISP]] and its descendants. (See also: [[first class control]].)

Another important extension was for [[modal logic|modal]] and other logics that need more than just the basic judgment of truth. These were first described, for the alethic modal logics [[S4 (modal logic)|S4]] and [[S5 (modal logic)|S5]], in a natural deduction style by [[Dag Prawitz|Prawitz]] in 1965,<ref name=prawitz1965 /> and have since accumulated a large body of related work. To give a simple example, the modal logic S4 requires one new judgment, "''A valid''", that is categorical with respect to truth:

:If "A" (is true) under no assumption that "B" (is true), then "A valid".

This categorical judgment is internalised as a unary connective ◻''A'' (read "''necessarily A''") with the following introduction and elimination rules:
{| style="margin-left: 2em;"
|-
|
 A valid
 ──────── ◻I
 ◻ A
| width="5%" |  ||
 ◻ A
 ──────── ◻E
 A
|}

Note that the premise "''A valid''" has no defining rules; instead, the categorical definition of validity is used in its place. This mode becomes clearer in the localised form when the hypotheses are explicit. We write "Ω;Γ ⊢ ''A''" where Γ contains the true hypotheses as before, and Ω contains valid hypotheses. On the right there is just a single judgment "''A''"; validity is not needed here since "Ω ⊢ ''A valid''" is by definition the same as "Ω;⋅ ⊢ ''A''". The introduction and elimination forms are then:
{| style="margin-left: 2em;"
|-
|
 Ω;⋅ ⊢ π : A
 ──────────────────── ◻I
 Ω;⋅ ⊢ '''box''' π : ◻ A
| width="5%" |  ||
 Ω;Γ ⊢ π : ◻ A
 ────────────────────── ◻E
 Ω;Γ ⊢ '''unbox''' π : A
|}

The modal hypotheses have their own version of the hypothesis rule and substitution theorem.
{| style="margin-left: 2em;"
|-
|
 ─────────────────────────────── valid-hyp
 Ω, u: (A valid) ; Γ ⊢ u : A
|}

=== Modal substitution theorem ===
; {{Unreferenced section|date=May 2024}}: ''If'' Ω;⋅ ⊢ π<sub>1</sub> : ''A'' ''and'' Ω, ''u'': (''A valid'') ; Γ ⊢ π<sub>2</sub> : ''C'', ''then'' Ω;Γ ⊢ [π<sub>1</sub>/''u''] π<sub>2</sub> : ''C''.

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 logic|linear]] and other [[substructural logic]]s, 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 [[analytic tableau]]x to be applied, as has been done in the case of [[labelled deduction]]. Labels also allow the naming of worlds in Kripke semantics; {{harvtxt|Simpson|1994}} presents an influential technique for converting frame conditions of modal logics in Kripke semantics into inference rules in a natural deduction formalisation of [[hybrid logic]]. {{harvtxt|Stouppa|2004}} surveys the application of many proof theories, such as Avron and Pottinger's [[hypersequent]]s and Belnap's [[display logic]] to such modal logics as S5 and B.

==Comparison with sequent calculus==
{{Unreferenced section|date=May 2024}}
{{Main|Sequent calculus}}

The sequent calculus is the chief alternative to natural deduction as a foundation of [[mathematical logic]]. In natural deduction the flow of information is bi-directional: elimination rules flow information downwards by deconstruction, and introduction rules flow information upwards by assembly. Thus, a natural deduction proof does not have a purely bottom-up or top-down reading, making it unsuitable for automation in proof search. To address this fact, [[Gerhard Gentzen|Gentzen]] in 1935 proposed his [[sequent calculus]], though he initially intended it as a technical device for clarifying the consistency of [[predicate logic]]. [[Stephen Cole Kleene|Kleene]], in his seminal 1952 book ''Introduction to Metamathematics'', gave the first formulation of the sequent calculus in the modern style.<ref>{{harvnb|Kleene|2009|pp=440–516}}. See also {{harvnb|Kleene|1980}}.</ref>

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 (symbol)|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:
{| style="margin-left: 2em;"
|-
|
 Γ ⇒ A
 ───────── ∨R<sub>1</sub>
 Γ ⇒ A ∨ B
| with="10%" |  || 
 Γ ⇒ B
 ───────── ∨R<sub>2</sub>
 Γ ⇒ A ∨ B
|}
On the left:
{| style="margin-left: 2em;"
|-
|
 Γ, u:A ⇒ C       Γ, v:B ⇒ C
 ─────────────────────────── ∨L
 Γ, w: (A ∨ B) ⇒ C
|}
Recall the ∨E rule of natural deduction in localised form:
{| style="margin-left: 2em;"
|-
|
 Γ ⊢ 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:
{| align="center"
|-
! natural deduction
|
! sequent calculus
|-
|<pre>
 ────── hyp
 |
 | elim. rules
 |
 ↓
 ────────────────────── ↑↓ meet
 ↑
 |
 | intro. rules
 |
 conclusion</pre>
| width="20%" align="center" | ⇒ ||<pre>
 ─────────────────────────── init
 ↑            ↑
 |            |
 | left rules | right rules
 |            |
 conclusion</pre>
|}
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:
{| style="margin-left: 2em;"
|-
|
 ────────── 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
{| style="margin-left: 2em;"
|-
! sequent calculus
|
! natural deduction
|-
|
 Γ ⇒ π<sub>1</sub> : A     Γ ⇒ π<sub>2</sub> : B
 ─────────────────────────── ∧R
 Γ ⇒ (π<sub>1</sub>, π<sub>2</sub>) : A ∧ B
| width="20%" |  || 
 Γ ⊢ π<sub>1</sub> : A      Γ ⊢ π<sub>2</sub> : B
 ───────────────────────── ∧I
 Γ ⊢ (π<sub>1</sub>, π<sub>2</sub>) : A ∧ B
|}
The left rule, however, performs some additional substitutions that are not performed in the corresponding elimination rules.
{| style="margin-left: 2em;"
|-
! sequent calculus
|
! natural deduction
|-
|
 Γ, u:A ⇒ π : C
 ──────────────────────────────── ∧L<sub>1</sub>
 Γ, v: (A ∧ B) ⇒ ['''fst''' v/u] π : C
| width="20%" |  || 
 Γ ⊢ π : A ∧ B
 ───────────── ∧E<sub>1</sub>
 Γ ⊢ '''fst''' π : A
|-
|
 Γ, u:B ⇒ π : C
 ──────────────────────────────── ∧L<sub>2</sub>
 Γ, v: (A ∧ B) ⇒ ['''snd''' v/u] π : C
| width="20%" |  || 
 Γ ⊢ π : A ∧ B
 ───────────── ∧E<sub>2</sub>
 Γ ⊢ '''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) ===
{{Unreferenced section|date=May 2024}}
: ''If'' Γ ⇒ π<sub>1</sub> : ''A'' ''and'' Γ, ''u'':''A'' ⇒ π<sub>2</sub> : ''C'', ''then'' Γ ⇒ [π<sub>1</sub>/u] π<sub>2</sub> : ''C''.

In most well behaved logics, cut is unnecessary as an inference rule, though it remains provable as a [[meta-theorem]]; the superfluousness of the cut rule is usually presented as a computational process, known as ''cut elimination''. This has an interesting application for natural deduction; usually it is extremely tedious to prove certain properties directly in natural deduction because of an unbounded number of cases. For example, consider showing that a given proposition is ''not'' provable in natural deduction. A simple inductive argument fails because of rules like ∨E or E which can introduce arbitrary propositions. However, we know that the sequent calculus is complete with respect to natural deduction, so it is enough to show this unprovability in the sequent calculus. Now, if cut is not available as an inference rule, then all sequent rules either introduce a connective on the right or the left, so the depth of a sequent derivation is fully bounded by the connectives in the final conclusion. Thus, showing unprovability is much easier, because there are only a finite number of cases to consider, and each case is composed entirely of sub-propositions of the conclusion. A simple instance of this is the ''global consistency'' theorem: "⋅ ⊢ ⊥" is not provable. In the sequent calculus version, this is manifestly true because there is no rule that can have "⋅ ⇒ ⊥" as a conclusion! Proof theorists often prefer to work on cut-free sequent calculus formulations because of such properties.

== See also ==
{{Portal|Philosophy}}
{{columns-list|colwidth=25em|
* [[Mathematical logic]]
* [[Sequent calculus]]
* [[Gerhard Gentzen]]
* [[System L]] (tabular natural deduction)
* [[Argument map]], the general term for tree-like logic notation
}}

==Notes==
{{Reflist}}

==References==
===General references===
* {{Cite book
 |last1=Allen
 |first1=Colin
 |last2=Hand
 |first2=Michael
 |title=Logic Primer
 |date=2022
 |publisher=The MIT Press
 |isbn=978-0-262-54364-4
 |edition=3rd
 |location=Cambridge, Massachusetts
}}
* {{Cite book
 |last=Arthur
 |first=Richard T. W.
 |title=An Introduction to Logic: Using Natural Deduction, Real Arguments, a Little History, and Some Humour
 |date=2017
 |publisher=Broadview Press
 |isbn=978-1-55481-332-2
 |edition=2nd
 |location=Peterborough, Ontario
 |oclc=962129086
 |url=https://www.worldcat.org/title/962129086
}}
* {{Cite book
 |last1=Ayala-Rincón
 |first1=Mauricio
 |last2=de Moura
 |first2=Flávio L. C.
 |title=Applied Logic for Computer Scientists
 |date=2017
 |publisher=Springer
 |series=Undergraduate Topics in Computer Science
 |isbn=978-3-319-51651-6
 |doi=10.1007/978-3-319-51653-0
 |url=https://link.springer.com/book/10.1007/978-3-319-51653-0
}}
* {{cite book|last1=Barker-Plummer|first1=Dave|last2=Barwise|first2=Jon|author2-link=Jon Barwise|last3=Etchemendy|first3=John|author3-link=John Etchemendy|year=2011|title=Language Proof and Logic|publisher=CSLI Publications|edition=2nd|isbn=978-1575866321}}
* {{Cite book
 |last=Bostock
 |first=David
 |title=Intermediate Logic
 |date=1997
 |publisher=Clarendon Press ; Oxford University Press
 |isbn=978-0-19-875141-0
 |location=Oxford ; New York
}}
* {{cite web|last1=Gallier|first1=Jean|author-link= Jean Gallier |title=Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi|url=ftp://ftp.cis.upenn.edu/pub/papers/gallier/conslog1.ps|access-date=12 June 2014|archive-url=https://web.archive.org/web/20170705061009/ftp://ftp.cis.upenn.edu/pub/papers/gallier/conslog1.ps|archive-date=2017-07-05|url-status=dead|year=2005}}
* {{Cite journal|last=Gentzen|first=Gerhard Karl Erich|author-link=Gerhard Gentzen|year=1935a|title=Untersuchungen über das logische Schließen. I|journal=[[Mathematische Zeitschrift]]|volume=39 | issue = 2 |pages=176–210|doi=10.1007/bf01201353 |s2cid=121546341|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508|archive-url=https://web.archive.org/web/20151224194624/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178|archive-date=2015-12-24|url-status=live}}
:{{cite journal|author-mask=1|last=Gentzen|first=Gerhard Karl Erich|author-link=Gerhard Gentzen|year=1964|orig-year=1935| title=Investigations into logical deduction | journal=[[American Philosophical Quarterly]] | volume=1 | number=4 | pages=249–287}}
* {{Cite journal|last=Gentzen|first=Gerhard Karl Erich|author-link=Gerhard Gentzen|year=1935b|title=Untersuchungen über das logische Schließen. II|journal=[[Mathematische Zeitschrift]]|volume=39 | issue = 3 |pages=405–431|doi=10.1007/bf01201363 |s2cid=186239837|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375605|archive-url=https://archive.today/20120709063902/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17188|archive-date=2012-07-09|url-status=live}}
:{{cite journal|author-mask=1|last=Gentzen|first=Gerhard Karl Erich|author-link=Gerhard Gentzen| year=1965|orig-year=1935| title=Investigations into logical deduction | journal=[[American Philosophical Quarterly]] | volume=2 | number=3 | pages=204–218}}
* {{cite book
 | last1 = Girard
 | first1 = Jean-Yves
 | author1-link = Jean-Yves Girard
 | url = http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html
 | publisher = Cambridge University Press, Cambridge, England
 | series = Cambridge Tracts in Theoretical Computer Science
 | title = Proofs and Types
 | year = 1990
 | access-date = 2006-04-20
 | archive-url = https://web.archive.org/web/20160704202340/http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html
 | archive-date = 2016-07-04
 | url-status = dead
 }} Translated and with appendices by Paul Taylor and Yves Lafont.
* {{Cite book
 |last1=Hansson
 |first1=Sven Ove
 |last2=Hendricks
 |first2=Vincent F.
 |title=Introduction to Formal Philosophy
 |date=2018
 |publisher=Springer
 |isbn=978-3-030-08454-7
 |series=Springer Undergraduate Texts in Philosophy
 |location=Cham
}}
* {{cite book|last1=Jaśkowski|first1=Stanisław|author1-link=Stanisław Jaśkowski|title=On the rules of suppositions in formal logic|year=1934}} Reprinted in ''Polish logic 1920–39'', ed. Storrs McCall.
*{{cite journal|last= Johansson|first=Ingebrigt|author-link=Ingebrigt Johansson|year=1937|title=Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus|url=http://www.numdam.org/item/CM_1937__4__119_0|journal=[[Compositio Mathematica]]|volume=4|pages=119–136|language=de}}
* {{cite book|last1=Kleene|first1=Stephen Cole|author1-link=Stephen Cole Kleene|title=Introduction to metamathematics|orig-year=1952|year=1980|publisher=North-Holland|edition=Eleventh|isbn=978-0-7204-2103-3}} 
* {{cite book|last1=Kleene|first1=Stephen Cole|author1-link=Stephen Cole Kleene|title=Introduction to metamathematics|orig-year=1952|year=2009|publisher=Ishi Press International|isbn=978-0-923891-57-2}} 
* {{cite book|last1=Kleene|first1=Stephen Cole|author1-link=Stephen Cole Kleene|title=Mathematical logic|orig-year=1967|year=2002|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-42533-7}}
* {{Cite book
 |last=Lemmon
 |first=Edward John
 |author-link=John Lemmon
 |title=Beginning Logic
 |url= https://archive.org/details/beginninglogic00lemm
 |year=1978
 |orig-year=1965
 |edition= Fifth printing, 1985
 |publisher=[[Hackett Publishing Company]]
 |isbn=0915144-50-6
 |location=Boca Raton, FL
}}
* {{cite book
 | last1 = Magnus
 | first1 = P.D.
 | last2 = Button
 | first2 = Tim
 | last3 = Trueman
 | first3 = Robert
 | last4 = Zach
 | first4 = Richard
 | title = forall x: An Introduction to Formal Logic
 | edition = Fall 2023
 | publisher = Open Logic Project
 | year = 2023
 | url = https://forallx.openlogicproject.org/
 | access-date = 2025-05-04
}}
* {{cite journal
 | last=Martin-Löf
 | first=Per
 | author-link=Per Martin-Löf
 | url = http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf
 | title = On the meanings of the logical constants and the justifications of the logical laws
 | journal=[[Nordic Journal of Philosophical Logic]]
 | volume=1
 | issue=1
 | year=1996
 | pages=11–60
}} Lecture notes to a short course at Università degli Studi di Siena, April 1983.
* {{Cite web
 |last1=Paseau
 |first1=A. C.
 |last2=Leek
 |first2=Robert
 |title=The Compactness Theorem
 |publisher= Internet Encyclopedia of Philosophy
 |url=https://iep.utm.edu/compactness/
 |access-date=2024-03-22
 |language=en-US
}}
* {{Citation
 |last1=Paseau
 |first1=Alexander
 |last2=Pregel
 |first2=Fabian
 |title=Deductivism in the Philosophy of Mathematics
 |date=2023
 |encyclopedia=The Stanford Encyclopedia of Philosophy
 |editor-last=Zalta
 |editor-first=Edward N.
 |editor2-last=Nodelman
 |editor2-first=Uri
 |url=https://plato.stanford.edu/archives/fall2023/entries/deductivism-mathematics/
 |access-date=2024-03-22
 |edition=Fall 2023
 |publisher=Metaphysics Research Lab, Stanford University
}}
* {{Citation
 |last1=Pelletier
 |first1=Francis Jeffry
 |last2=Hazen
 |first2=Allen
 |title=Natural Deduction Systems in Logic
 |date=2024
 |encyclopedia=The Stanford Encyclopedia of Philosophy
 |editor-last=Zalta
 |editor-first=Edward N.
 |editor2-last=Nodelman
 |editor2-first=Uri
 |url=https://plato.stanford.edu/archives/spr2024/entries/natural-deduction/
 |access-date=2024-03-22
 |edition=Spring 2024
 |publisher=Metaphysics Research Lab, Stanford University
}}
* {{cite journal
 | last1 = Pfenning
 | first1 = Frank
 | last2 = Davies
 | first2 = Rowan
 | url = https://www-2.cs.cmu.edu/~fp/papers/mscs00.pdf
 | title = A judgmental reconstruction of modal logic
 | journal = Mathematical Structures in Computer Science
 | volume = 11
 | issue = 4
 | year = 2001
 | pages = 511–540
 | doi = 10.1017/S0960129501003322
 | doi-broken-date=2025-02-25 <!-- This line generates a template warning -->
 | citeseerx = 10.1.1.43.1611
 | s2cid = 16467268
}}
* {{Prawitz Natural Deduction|year=1965}}
* {{Prawitz Natural Deduction|year=2006|include-link=no}}
* {{cite book|last1=Quine|first1=Willard Van Orman|author1-link=Willard Van Orman Quine|title=Mathematical logic|edition=Revised|publisher=Harvard University Press|location=Cambridge, Massachusetts|year=1981|orig-year=1940|isbn=978-0-674-55451-1}}
* {{cite book|last1=Quine|first1=Willard Van Orman|author1-link=Willard Van Orman Quine|title=Methods of logic|edition=Fourth|publisher=Harvard University Press|location=Cambridge, Massachusetts|year=1982|orig-year=1950|isbn=978-0-674-57176-1}}
* {{Citation
 | last = Restall
 | first = Greg
 | title = Substructural Logics
 | date = 2018
 | encyclopedia = The Stanford Encyclopedia of Philosophy
 | editor-last = Zalta
 | editor-first = Edward N.
 | url = https://plato.stanford.edu/archives/spr2018/entries/logic-substructural/
 | access-date = 2024-03-22
 | edition = Spring 2018
 | publisher = Metaphysics Research Lab, Stanford University
}}
*{{cite thesis|last=Simpson|first=Alex K.|year=1994|title=The Proof Theory and Semantics of Intuitionistic Modal Logic|url=https://era.ed.ac.uk/bitstream/handle/1842/407/ECS-LFCS-94-308.PDF?sequence=2&isAllowed=y|hdl=1842/407|publisher=[[University of Edinburgh|Edinburgh Research Archive (ERA)]]}}
* {{cite book|last1=Stoll|first1=Robert Roth|title=Set Theory and Logic|location=Mineola, New York|publisher=Dover Publications|year=1979|orig-year=1963|isbn=978-0-486-63829-4}}
* {{cite book|last1=Stouppa|first1=Phiniki|title=The Design of Modal Proof Theories: The Case of S5|year=2004|publisher=University of Dresden|citeseerx=10.1.1.140.1858}} MSc thesis.
* {{cite book|last1=Suppes|first1=Patrick Colonel|author1-link=Patrick Suppes|year=1999|orig-year=1957|title=Introduction to logic|publisher=Dover Publications|location=Mineola, New York|isbn=978-0-486-40687-9}}
* {{Cite web |last=Sutcliffe|first=Geoff|title=Propositional Logic |url=https://www.cs.miami.edu/home/geoff/Courses/CSC648-12S/Content/Propositional.shtml |access-date=2025-05-04|publisher=University of Miami|website=www.cs.miami.edu}}
*{{cite book | last = Tennant | first = Neil | title = Natural Logic | publisher = [[Edinburgh University Press]] | year = 1990 | orig-year = 1978 | edition = 1st, repr. with corrections | isbn = 0852245793 }}
* {{cite book|last=Van Dalen|first=Dirk|author-link=Dirk van Dalen|year=2013|orig-year=1980|title=Logic and Structure|series=Universitext |edition=5|publisher=[[Springer Science+Business Media|Springer]]|location=London, Heidelberg, New York, Dordrecht|isbn=978-1-4471-4558-5|doi=10.1007/978-1-4471-4558-5}}
* {{Cite book
 |last=von Plato
 |first=Jan
 |title=Elements of Logical Reasoning
 |date=2013
 |publisher=[[Cambridge University Press]]
 |isbn=978-1-107-03659-8
 |edition=1. publ
 |location=Cambridge
}}
* {{Cite web
 |last=Weisstein
 |first=Eric W.
 |title=Connective
 |url=https://mathworld.wolfram.com/
 |access-date=2024-03-22
 |website=mathworld.wolfram.com
 |language=en
}}

==External links==
*{{Cite web |last=Indrzejczak|first=Andrzej |title=Natural Deduction |publisher=[[Internet Encyclopedia of Philosophy]] |url=https://iep.utm.edu/natural-deduction/ |access-date=2025-05-04}}
* {{Cite web|
last=Laboreo|first=Daniel Clemente|date=August 2004|url=https://www.danielclemente.com/logica/dn.en.pdf|title=Introduction to natural deduction}}
* {{Cite web|url=http://www.winterdrache.de/freeware/domino/|title=Domino On Acid|quote=Natural deduction visualized as a game of dominoes|access-date=10 December 2023}}
* {{Cite web|last=Pelletier|first=Francis Jeffry|url=https://www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf|title=A History of Natural Deduction and Elementary Logic Textbooks}}
* {{SEP|natural-deduction|Natural Deduction Systems in Logic|Pelletier, Francis Jeffry; Hazen, Allen|29 October 2021}}
* {{Cite web|last=Levy|first=Michel|url=http://teachinglogic.univ-grenoble-alpes.fr/DN1/|title= A Propositional Prover}}

{{Mathematical logic}}
{{Foundations-footer}}

{{DEFAULTSORT:Natural Deduction}}
[[Category:Logical calculi]]
[[Category:Deductive reasoning]]
[[Category:Proof theory]]
[[Category:Methods of proof]]