Basically we use Gentzen's version of LK (see ),
but extend it by equality and definition rules. The axioms may be
arbitrary atomic sequents. There are two groups of
rules, the logical and the structural ones. All rules with
the exception of cut have left and right versions; left versions
are denoted by , right versions by . Every logical
rule introduces a logical operator on the left or on the right
side of a sequent. Structural rules serve the purpose of making
logical inferences possible (e.g. permutation) or to put proofs
and denote formulas,
sequences of formulas. In the rules there are introducing or auxiliary
formulas (in the premises) and introduced or principal formulas in the
conclusion. We indicate these formulas for all rules. In particular we
mark the auxiliary formulas by and the principal ones by .
The logical rules:
where is an arbitrary term containing only free variables.
where is a free variable which may not occur in . is called an eigenvariable.
- The logical rules for -introduction (the variable conditions
for are these for
, and similarly for and
The structural rules:
where is a permutation. In all formulas on the left side of the conclusion sequent are principal formulas and all formulas on the left side of the premise sequent are auxiliary formulas; similarly for .
- The cut rule:
As unary structural rules are not important in classical logic we frequently
indicate their use by double lines, e.g.
indicates the application of the rule plus a sequence of unary structural rules before and/or after the application of .