TU Vienna logic.at Theory and Logic Group (E185-2)

LK

Basically we use Gentzen's version of LK (see [1]), 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 together (cut). 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:

• -introduction:

• -introduction:

• -introduction:

• -introduction:

• -introduction:

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:

• permutation

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 .
• weakening:

• contraction:

• 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 .