Editing Natural deduction (section)

==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:{{sfn|Ayala-Rincón|de Moura|2017|pages=2,20}}

{| class="wikitable"
|+ Rules for classical propositional logic
! Introduction rules
! Elimination rules
|-
| <math>\begin{array}{c}
\varphi \qquad \psi \\
\hline
\varphi \wedge \psi 
\end{array} (\wedge_i)</math>
| <math>\begin{array}{c}
\varphi \wedge \psi \\
\hline
\varphi 
\end{array} (\wedge_e)</math>
|-
| <math>\begin{array}{c}
\varphi \\
\hline
\varphi \vee \psi 
\end{array} (\vee_i)</math>
| <math>
\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}}
</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}
[\varphi]^u \\
\vdots \\
\bot \\
\hline
\neg \varphi 
\end{array} (\neg_i) \ u</math>
| <math>\begin{array}{c}
\varphi \qquad \neg \varphi \\
\hline
\bot 
\end{array} (\neg_e)</math>
|-
|
| <math>\begin{array}{c}
[\neg \varphi]^u \\
\vdots \\
\bot \\
\hline
\varphi 
\end{array} (\text{PBC}) \ u</math>
|}
This table follows [[Propositional calculus#Constants and schemata|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 <math>\wedge_i</math>, 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.

<div style="margin-left: 2em">
<math>
 \cfrac{\cfrac{A \wedge B}{B}\ \wedge_{E2} 
 \qquad \cfrac{A \wedge B}{A}\ \wedge_{E1}}
 {B \wedge A}\ \wedge_I
</math>
</div>

As a second example, consider the derivation of "''A → (B → (A ∧ B))''":
<div style="margin-left: 2em">
<math>
 \cfrac{\cfrac{\cfrac{}{A}\ u \quad \cfrac{}{B}\ w}{A \wedge B}\ \wedge_I}{
 \cfrac{B \to \left ( A \wedge B \right )}{
 A \to \left ( B \to \left ( A \wedge B \right ) \right )
 }\ \to_{I^u}
 }\ \to_{I^w}
 </math>
</div>
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'').