Editing Sequent calculus (section)

===An intuitive explanation===

The above rules can be divided into two major groups: ''logical'' and ''structural'' ones. Each of the logical rules introduces a new logical formula either on the left or on the right of the [[Turnstile (symbol)|turnstile]] <math>\vdash</math>. In contrast, the structural rules operate on the structure of the sequents, ignoring the exact shape of the formulas. The two exceptions to this general scheme are the axiom of identity (I) and the rule of (Cut).

Although stated in a formal way, the above rules allow for a very intuitive reading in terms of classical logic. Consider, for example, the rule <math>({\land}L_1)</math>. It says that, whenever one can prove that <math>\Delta</math> can be concluded from some sequence of formulas that contain <math>A</math>, then one can also conclude <math>\Delta</math> from the (stronger) assumption that <math>A \land B</math> holds. Likewise, the rule <math>({\neg}R)</math> states that, if <math>\Gamma</math> and <math>A</math> suffice to conclude <math>\Delta</math>, then from <math>\Gamma</math> alone one can either still conclude <math>\Delta</math> or <math>A</math> must be false, i.e. <math>{\neg}A</math> holds. All the rules can be interpreted in this way.

For an intuition about the quantifier rules, consider the rule <math>({\forall}R)</math>. Of course concluding that <math>\forall{x} A</math> holds just from the fact that <math>A[y/x]</math> is true is not in general possible. If, however, the variable y is not mentioned elsewhere (i.e. it can still be chosen freely, without influencing the other formulas), then one may assume, that <math>A[y/x]</math> holds for any value of y. The other rules should then be pretty straightforward.

Instead of viewing the rules as descriptions for legal derivations in predicate logic, one may also consider them as instructions for the construction of a proof for a given statement. In this case the rules can be read bottom-up; for example, <math>({\land}R)</math> says that, to prove that <math>A \land B</math> follows from the assumptions <math>\Gamma</math> and <math>\Sigma</math>, it suffices to prove that <math>A</math> can be concluded from <math>\Gamma</math> and <math>B</math> can be concluded from <math>\Sigma</math>, respectively. Note that, given some antecedent, it is not clear how this is to be split into <math>\Gamma</math> and <math>\Sigma</math>. However, there are only finitely many possibilities to be checked since the antecedent by assumption is finite. This also illustrates how proof theory can be viewed as operating on proofs in a combinatorial fashion: given proofs for both <math>A</math> and <math>B</math>, one can construct a proof for <math>A \land B</math>.

When looking for some proof, most of the rules offer more or less direct recipes of how to do this. The rule of cut is different: it states that, when a formula <math>A</math> can be concluded and this formula may also serve as a premise for concluding other statements, then the formula <math>A</math> can be "cut out" and the respective derivations are joined. When constructing a proof bottom-up, this creates the problem of guessing <math>A</math> (since it does not appear at all below). The [[cut-elimination theorem]] is thus crucial to the applications of sequent calculus in [[automated deduction]]: it states that all uses of the cut rule can be eliminated from a proof, implying that any provable sequent can be given a ''cut-free'' proof.

The second rule that is somewhat special is the axiom of identity (I). The intuitive reading of this is obvious: every formula proves itself.  Like the cut rule, the axiom of identity is somewhat redundant: the [[completeness of atomic initial sequents]] states that the rule can be restricted to [[atomic formula]]s without any loss of provability.

Observe that all rules have mirror companions, except the ones for implication. This reflects the fact that the usual language of first-order logic does not include the "is not implied by" connective <math>\not\leftarrow</math> that would be the De Morgan dual of implication. Adding such a connective with its natural rules would make the calculus completely left–right symmetric.