A sequent represents a formal step in a proof. Typically it consists of two lists of formulas, one representing the premises and one the conclusions. A typical sequent might be:
where and are the premises and and are the conclusions.
This claims that, from premises and either or must be true. Note that is not a symbol in the language, rather it is a symbol in the metalanguage used to discuss proofs. Also, notice the asymmetry: everything on the left must be true to conclude only one thing on the right. This does create a different kind of symmetry, since adding formulas to either side results in a weaker sequent, while removing them from either side gives a stronger one.
Some systems allow only one formula on the right.
Most proof systems provide ways to deduce one sequent from another. These rules are written with a list of sequents above and below a line. This rule indicates that if everything above the line is true, so is everything under the line. A typical rule is:
This indicates that if we can deduce from , we can also deduce it from together with .
Note that the capital Greek letters are usually used to denote a (possibly empty) list of formulas. is used to denote the contraction of and , that is, the list of those formulas appearing in either or but with no repeats.
|Date of creation||2013-03-22 13:05:11|
|Last modified on||2013-03-22 13:05:11|
|Last modified by||Henry (455)|