# Definition:Sequent

Jump to navigation
Jump to search

## Definition

A **sequent** is an expression in the form:

- $\phi_1, \phi_2, \ldots, \phi_n \vdash \psi$

where $\phi_1, \phi_2, \ldots, \phi_n$ are premises (any number of them), and $\psi$ the conclusion (only one), of an argument.

## Also presented as

Instead of presenting the **sequent** all on one line, separated by commas, it is often arranged in a vertical form:

\(\ds \phi_1\) | \(\) | \(\ds \) | ||||||||||||

\(\ds \phi_2\) | \(\) | \(\ds \) | ||||||||||||

\(\ds \ldots\) | \(\) | \(\ds \) | ||||||||||||

\(\ds \phi_n\) | \(\) | \(\ds \) | ||||||||||||

\(\ds \vdash \ \ \) | \(\ds \psi\) | \(\) | \(\ds \) |

Which form is preferred depends on personal taste or convenience.

A long **sequent** with complex premises is often better presented in the vertical form, whereas a simpler **sequent** which is easily comprehended at a glance may merit the single-line treatment.

## Sources

- 1965: E.J. Lemmon:
*Beginning Logic*... (previous) ... (next): $\S 1.2$: Conditionals and Negation - 2000: Michael R.A. Huth and Mark D. Ryan:
*Logic in Computer Science: Modelling and reasoning about systems*... (previous) ... (next): $\S 1.2$: Natural Deduction