A sequent is a proposition combined
with the hypotheses necessary to prove it. A Typol sequent has the syntax:
The turnstyle must appear in every sequent. A sequent is a proposition combined
with the hypotheses necessary to prove it. A Typol sequent has the syntax:
<hypotheses> "|-" <consequent>
where <hypotheses> is a list of expressions separated by commas, and <consequent> is a proposition.
Since we don't require any hypotheses when evaluating pure arithmetic expressions -the evaluation of expressions is context independent- our sequents initially have the form:
expression : value
The very first abstract syntax expression in the consequent of a sequent is called the subject of the sequent. The subject has a particular role during the proof of a propostion, as we will see shortly.