The Cut-Elimination System CERES

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). and 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:

$\wedge$ -introduction:

$\begin{displaymath} \infer[\wedge \colon l^1]{(A \wedge B)^\star, \Gamma \vdash ... ...dge B)^\star, \Gamma \vdash \Delta}{B^+, \Gamma \vdash \Delta} \end{displaymath}$

$\begin{displaymath} \infer[\wedge :r]{\Gamma, \Pi \vdash \Delta, \Lambda, (A \we... ...star} { \Gamma \vdash \Delta, A^+ & \Pi \vdash \Lambda, B^+ } \end{displaymath}$
$\vee$ -introduction:

$\begin{displaymath} \infer[\vee \colon l]{ (A \vee B)^\star,\Gamma, \Pi \vdash \... ...ma \vdash \Delta, (A \vee B)^\star}{\Gamma \vdash \Delta, B^+} \end{displaymath}$
$\rightarrow$ -introduction:

$\begin{displaymath} \infer[\rightarrow \colon l]{(A \rightarrow B)^\star, \Gamma... ...ta, (A \rightarrow B)^\star} {A^+, \Gamma \vdash \Delta, B^+} \end{displaymath}$
$\neg$ -introduction:

$\begin{displaymath} \infer[\neg\colon l]{\neg A^\star, \Gamma \vdash \Delta}{\Ga... ...\Gamma \vdash \Delta, \neg A^\star}{A^+, \Gamma \vdash \Delta} \end{displaymath}$
$\forall$ -introduction:

$\begin{displaymath} \infer[\forall \colon l]{(\forall x)A^\star, \Gamma \vdash \Delta}{A\{x \leftarrow t\}^+, \Gamma \vdash \Delta} \end{displaymath}$

where is an arbitrary term containing only free variables.

$\begin{displaymath} \infer[\forall \colon r]{\Gamma \vdash \Delta, (\forall x)A^\star}{\Gamma \vdash \Delta, A\{x \leftarrow \alpha\}^+} \end{displaymath}$

where $\alpha$ is a free variable which may not occur in $\Gamma,\Delta,A$ . $\alpha$ is called an eigenvariable.
The logical rules for $\exists$ -introduction (the variable conditions for $\exists :l$ are these for $\forall \colon r$ , and similarly for $\exists :r$ and $\forall \colon l$ ):

$\begin{displaymath} \infer[\exists \colon l]{(\exists x)A^\star, \Gamma \vdash \... ...exists x)A^\star}{\Gamma \vdash \Delta, A\{x \leftarrow t\}^+} \end{displaymath}$

The structural rules:

permutation

$\begin{displaymath} \infer[\pi:l(\sigma)]{A_{\sigma(1)},\ldots,A_{\sigma(n)}\vda... ...{\sigma(1)},\ldots,A_{\sigma(n)}}{\Gamma\vdash A_1,\ldots,A_n} \end{displaymath}$

where $\sigma$ is a permutation. In $\pi:l$ 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 $\pi:r$ .
weakening:

$\begin{displaymath} \infer[w\colon r]{\Gamma \vdash \Delta, A^\star}{\Gamma \vd... ...colon l]{A^\star ,\Gamma \vdash \Delta}{\Gamma \vdash \Delta} \end{displaymath}$
contraction:

$\begin{displaymath} \infer[c\colon l]{A^\star, \Gamma \vdash \Delta}{A^+,A^+,\Ga... ...amma \vdash \Delta, A^\star }{\Gamma \vdash \Delta, A^+, A^+} \end{displaymath}$
The cut rule:

$\begin{displaymath} \infer[{\it cut}]{\Gamma,\Pi \vdash \Delta, \Lambda} {\Gamma \vdash \Delta, A^+ & A^+, \Pi \vdash \Lambda} \end{displaymath}$

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