in a combinatorial fashion: given proofs for both and , one can construct a proof for . 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 can be concluded and this formula may also serve as a premise for concluding other statements, then the formula can be "cut out" and the respective derivations are joined. When constructing a proof bottom-up, this creates the problem of guessing (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 formulas 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 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. Example derivations Here is the derivation of "", known as the Law of excluded middle (tertium non datur in Latin). Next is the proof of a simple fact involving quantifiers. Note that the converse is not true, and its falsity can be seen when attempting to derive it bottom-up, because an existing free variable cannot be used in substitution in the rules and . For something more interesting we shall prove . It is straightforward to find the derivation, which exemplifies the usefulness of LK in automated proving. These derivations also emphasize the strictly formal structure of the sequent calculus. For example, the logical rules as defined above always act on a formula immediately adjacent to the turnstile, such that the permutation rules are necessary. Note, however, that this is in part an artifact of the presentation, in the original style of Gentzen. A common simplification involves the use of