Editing Natural deduction (section)

=== 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}}