# 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:

$$\frac{\mathrm{\Gamma}\Rightarrow \mathrm{\Sigma}}{\begin{array}{cc}\hfill \mathrm{\Gamma},\alpha \Rightarrow \mathrm{\Sigma}\hfill & \hfill \alpha ,\mathrm{\Gamma}\Rightarrow \mathrm{\Sigma}\hfill \end{array}}$$ |

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 |