HLK ProofTool
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 $\xi:l$, right versions by $\xi:r$. 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). $A$ and $B$ denote formulas, $\Gamma, \Delta, \Pi, \Lambda$ 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 $\star$.

The logical rules:

The structural rules:

As unary structural rules are not important in classical logic we frequently indicate their use by double lines, e.g.

\begin{displaymath}
\infer=[\xi]{\Gamma',\Pi'\vdash \Delta',\Lambda'}{
\Gamma\vdash \Delta
&
\Pi\vdash \Lambda
}
\end{displaymath}

indicates the application of the rule $\xi$ plus a sequence of unary structural rules before and/or after the application of $\xi$.