Editing Sequent calculus (section)

===Inference rules===

The following notation will be used:
* <math>\vdash</math> known as the [[Turnstile (symbol)|turnstile]], separates the ''assumptions'' on the left from the ''propositions'' on the right
* <math>A</math> and <math>B</math> denote formulas of first-order predicate logic (one may also restrict this to propositional logic),
* <math>\Gamma, \Delta, \Sigma</math>, and <math>\Pi</math> are finite (possibly empty) sequences of formulas (in fact, the order of formulas does not matter; see {{slink||Structural rules}}),  called contexts,
** when on the ''left'' of the <math>\vdash</math>, the sequence of formulas is considered ''conjunctively'' (all assumed to hold at the same time),
** while on the ''right'' of the <math>\vdash</math>, the sequence of formulas is considered ''disjunctively'' (at least one of the formulas must hold for any assignment of variables),
* <math>t</math> denotes an arbitrary term,
* <math>x</math> and <math>y</math> denote variables.
* a variable is said to occur [[Free variables and bound variables|free]] within a formula if it is not bound by quantifiers <math>\forall</math> or <math>\exists</math>.
* <math>A[t/x]</math> denotes the formula that is obtained by substituting the term <math>t</math> for every free occurrence of the variable <math>x</math> in formula <math>A</math> with the restriction that the term <math>t</math> must be free for the variable <math>x</math> in <math>A</math> (i.e., no occurrence of any variable in <math>t</math> becomes bound in <math>A[t/x]</math>).
* <math>WL</math>, <math>WR</math>, <math>CL</math>, <math>CR</math>, <math>PL</math>, <math>PR</math>: These six stand for the two versions of each of three structural rules; one for use on the left ('L') of a <math>\vdash</math>, and the other on its right ('R'). The rules are abbreviated 'W' for ''Weakening (Left/Right)'', 'C' for ''Contraction'', and 'P' for ''Permutation''.

Note that, contrary to the rules for proceeding along the reduction tree presented above, the following rules are for moving in the opposite directions, from axioms to theorems. Thus they are exact mirror-images of the rules above, except that here symmetry is not implicitly assumed, and rules regarding [[quantifier (logic)|quantification]] are added.

{| class="wikitable"
|-
! Axiom
! Cut
|-
| <math> \cfrac{\qquad }{ A \vdash A} \quad (I) </math>
| <math> 
   \cfrac{\Gamma \vdash \Delta, A \qquad A, \Sigma \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})
 </math>
|}
{| class="wikitable"
|-
! Left logical rules
! Right logical rules
|-
| <math> \cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \quad ({\land}L_1)
 </math>
| <math> \cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad  ({\lor}R_1)
 </math>
|-
| <math> \cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \land B \vdash \Delta}  \quad ({\land}L_2)
 </math>
| <math> \cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_2)
 </math>
|-
| <math> \cfrac{\Gamma, A \vdash \Delta \qquad \Gamma, B \vdash \Delta}{\Gamma, A \lor B \vdash \Delta} \quad ({\lor}L)
 </math>
| <math> \cfrac{\Gamma \vdash A, \Delta \qquad \Gamma \vdash B, \Delta}{\Gamma \vdash A \land B, \Delta} \quad ({\land}R)
 </math>
|-
| <math>
  \cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad  ({\rightarrow }L)
 </math>
| <math>
   \cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)
 </math>
|-
| <math>
  \cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad  ({\lnot}L)
 </math>
| <math>
  \cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)
 </math>
|-
| <math>
  \cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta} \quad  ({\forall}L)
 </math>
| <math>
  \cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta} \quad  ({\forall}R) 
 </math> (†)
|-
| <math>
  \cfrac{\Gamma, A[y/x] \vdash \Delta}{\Gamma, \exists x A \vdash \Delta} \quad  ({\exists}L)
 </math> (†)
| <math>
  \cfrac{\Gamma \vdash A[t/x], \Delta}{\Gamma \vdash \exists x A, \Delta} \quad  ({\exists}R)
 </math>
|}
{| class="wikitable"
|-
! Left structural rules
! Right structural rules
|-
| <math>
  \cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})
 </math>
| <math>
  \cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})
 </math>
|-
| <math>
  \cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})
 </math>
| <math>
  \cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})
 </math>
|-
| <math>
  \cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})
 </math>
| <math>
  \cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})
 </math>
|}

'''''Restrictions''': In the rules marked with (†), <math>({\forall}R)</math> and <math>({\exists}L)</math>, the variable <math>y</math> must not occur free anywhere in the respective lower sequents.''