Jump to navigation Jump to search
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.
- 1965: E.J. Lemmon: Beginning Logic ... (previous) ... (next): Chapter $1$: The Propositional Calculus $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