Definition:Sequent

From ProofWiki
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