3.4.1 Sequents

A sequent is a formal statement describing something we want to prove.

Sequents are of the following form

$H \vdash G$

where $H$ is the set of hypotheses (predicates) and $G$ is the goal that can be proved from the predicates.

The above statement can be read as follows: Under the hypotheses $H$, prove the goal $G$.

Work sponsored by the Deploy Project | Handbook as PDF | Rodin Wiki | Creative Commons License Creative Commons License | Feedback