moving in the opposite directions, from axioms to theorems. Thus they are exact mirror-images of the rules above, except that here symmetry is not implicitly assumed, and rules regarding quantification are added. Restrictions: In the rules and , the variable must not occur free anywhere in the respective lower sequents. 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 . In contrast, the structural rules operate on the structure of the sequents, ignoring the exact shape of the formulae. 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 . It says that, whenever one can prove that can be concluded from some sequence of formulae that contain , then one can also conclude from the (stronger) assumption that holds. Likewise, the rule states that, if and suffice to conclude , then from alone one can either still conclude or must be false, i.e. holds. All the rules can be interpreted in this way. For an intuition about the quantifier rules, consider the rule . Of course concluding that holds just from the fact that 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 formulae), then one may assume, that 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, says that, to prove that follows from the assumptions and , it suffices to prove that can be concluded from and can be concluded from , respectively. Note that, given some antecedent, it is not clear how this is to be split into and . 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