Editing Sequent (section)

=== Rules ===
Most proof systems provide ways to deduce one sequent from another. These inference rules are written with a list of sequents above and below a [[Coplanarity|line]]. This rule indicates that if everything above the line is true, so is everything under the line.

A typical rule is:

:<math> \frac{\Gamma,\alpha\vdash\Sigma\qquad \Gamma\vdash\alpha}{\Gamma\vdash\Sigma}</math>

This indicates that if we can deduce that <math>\Gamma,\alpha</math> yields <math>\Sigma</math>, and that <math>\Gamma</math> yields <math>\alpha</math>, then we can also deduce that <math>\Gamma</math> yields  <math>\Sigma</math>. (See also the full set of [[sequent calculus#Inference rules|sequent calculus inference rules]].)