## You are here

Homesequent

## Primary tabs

# sequent

A *sequent* represents a formal step in a proof. Typically it consists of two lists of formulas, one representing the premises and one the conclusions. A typical sequent might be:

$\phi,\psi\Rightarrow\alpha,\beta$ |

where $\phi$ and $\psi$ are the premises and $\alpha$ and $\beta$ are the conclusions.

This claims that, from premises $\phi$ and $\psi$ either $\alpha$ or $\beta$ must be true. Note that $\Rightarrow$ is not a symbol in the language, rather it is a symbol in the metalanguage used to discuss proofs. Also, notice the asymmetry: everything on the left must be true to conclude only one thing on the right. This does create a different kind of symmetry, since adding formulas to either side results in a weaker sequent, while removing them from either side gives a stronger one.

Some systems allow only one formula on the right.

Most proof systems provide ways to deduce one sequent from another. These rules are written with a list of sequents above and below a line. This rule indicates that if everything above the line is true, so is everything under the line. A typical rule is:

$\frac{\Gamma\Rightarrow\Sigma}{\begin{array}[]{cc}\Gamma,\alpha\Rightarrow% \Sigma&\alpha,\Gamma\Rightarrow\Sigma\end{array}}$ |

This indicates that if we can deduce $\Sigma$ from $\Gamma$, we can also deduce it from $\Gamma$ together with $\alpha$.

Note that the capital Greek letters are usually used to denote a (possibly empty) list of formulas. $[\Gamma,\Sigma]$ is used to denote the *contraction* of $\Gamma$ and $\Sigma$, that is, the list of those formulas appearing in either $\Gamma$ or $\Sigma$ but with no repeats.

## Mathematics Subject Classification

03F03*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections