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:

$$\varphi ,\psi \Rightarrow \alpha ,\beta$$

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

This claims that, from premises $\varphi$ 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:

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

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

Title	sequent
Canonical name	Sequent
Date of creation	2013-03-22 13:05:11
Last modified on	2013-03-22 13:05:11
Owner	Henry (455)
Last modified by	Henry (455)
Numerical id	10
Author	Henry (455)
Entry type	Definition
Classification	msc 03F03
Related topic	GentzenSystem
Defines	contraction
Defines	premise
Defines	conclusion