The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality

TL;DR

This paper explores the extension of the sequent calculus to first order logic with equality, focusing on cut elimination and nonlengthening properties, building on Leibnitz's principle and Gentzen's work.

Contribution

It introduces new insights into cut elimination and enhances the nonlengthening property for sequent calculus with equality.

Findings

Established cut elimination for the extended calculus.

Improved the nonlengthening property for equality logic.

Connected Leibnitz's principle with sequent calculus extensions.

Abstract

We show how Leibnitz.s indiscernibility principle and Gentzen's original work lead to extensions of the sequent calculus to first order logic with equality and investigate the cut elimination property. Furthermore we discuss and improve the nonlengthening property of Lifshitz and Orevkov.

Equations

$$\begin{array}[]{clccc}\Lambda\Rightarrow F\{v/r\}~{}~{}~{}~{}~{}\Gamma,F\{v/s\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=^{(2)}\Rightarrow$}}&{}{}{}{}\hfil&\Gamma,Z(r)\Rightarrow Z(s)&\vbox to0.0pt{\hbox{$\Rightarrow=^{(2)}$}}\\ \cline{1-1}\cr\cline{4-4}\cr\Lambda,\Gamma,r=s\Rightarrow\Delta&&&\Gamma\Rightarrow r=s\end{array}$$

$$\begin{array}[]{cl}F\{v/r\}~{}~{}~{}~{}~{}r=s&\vbox to0.0pt{\hbox{$=_{1}^{N}$}}\\ \cline{1-1}\cr F\{v/s\}&\end{array}$$

$$\begin{array}[]{cl}\Gamma\Rightarrow F\{v/r\}&\vbox to0.0pt{\hbox{$=_{1}$}}\\ \cline{1-1}\cr\Gamma,r=s\Rightarrow F\{v/s\}&\end{array}$$

$$\begin{array}[]{cl}\Gamma\Rightarrow F\{v/r\}~{}~{}~{}~{}~{}\Lambda\Rightarrow r=s&\vbox to0.0pt{\hbox{$~{}CNG$}}\\ \cline{1-1}\cr\Gamma,\Lambda\Rightarrow F\{v/s\}\end{array}$$

$$\begin{array}[]{cl}\Gamma\Rightarrow F\{v/r\}&\vbox to0.0pt{\hbox{$=_{2}$}}\\ \cline{1-1}\cr\Gamma,s=r\Rightarrow F\{v/s\}\end{array}$$

$$\begin{array}[]{cl}F\{v/r\}~{}~{}~{}~{}~{}s=r&\vbox to0.0pt{\hbox{$=_{2}^{N}$}}\\ \cline{1-1}\cr F\{v/s\}&\end{array}$$

$$\begin{array}[]{clccl}\Gamma,F\{v/r\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=_{1}^{l}$ }}&~{}~{}~{}\mbox{and}{}{}{}&\Gamma,F\{v/r\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=_{2}^{l}$ }}\\ \cline{1-1}\cr\cline{4-4}\cr\Gamma,F\{v/s\},r=s\Rightarrow\Delta&&&\Gamma,F\{v/s\},s=r\Rightarrow\Delta\end{array}$$

$$\begin{array}[]{c}\Lambda\Rightarrow F\{v/r\}~{}~{}~{}~{}~{}~{}~{}~{}\Gamma,F\{v/s\}\Rightarrow\Delta\\ \cline{1-1}\cr\Lambda,\Gamma,r=s\Rightarrow\Delta\end{array}$$

$$\begin{array}[]{c}\Gamma,Z(r)\Rightarrow Z(s)\\ \cline{1-1}\cr\Gamma\Rightarrow r=s\end{array}$$

$$\begin{array}[]{cccl}Z(r)\Rightarrow Z(r)~{}~{}~{}~{}~{}Z(s)\Rightarrow Z(s)&\vbox to0.0pt{\hbox{$=^{(2)}\Rightarrow$}}{}{}{}{}{}{}&Z(r)\Rightarrow Z(r)~{}~{}~{}~{}~{}Z(s)\Rightarrow Z(s)&\\ \cline{1-1}\cr\cline{3-3}\cr Z(r),r=s\Rightarrow Z(s)&&Z(r)\rightarrow Z(s),Z(r)\Rightarrow Z(s)&\\ \cline{1-1}\cr\cline{3-3}\cr r=s\Rightarrow Z(r)\rightarrow Z(s)&&\forall X(X(r)\rightarrow X(s)),Z(r)\Rightarrow Z(s)&\vbox to0.0pt{\hbox{$\Rightarrow=^{(2)}$}}\\ \cline{1-1}\cr\cline{3-3}\cr r=s\Rightarrow\forall X(X(r)\rightarrow X(s))&&\forall X(X(r)\rightarrow X(s))\Rightarrow r=s&\end{array}$$

$$\begin{array}[]{ccc}\Gamma,Z(r)\Rightarrow Z(s)&{}{}{}{}\hfil&\Rightarrow r=r~{}~{}~{}~{}~{}r=s\Rightarrow r=s\\ \cline{1-1}\cr\cline{3-3}\cr\Gamma\Rightarrow Z(r)\rightarrow Z(s)&&r=r\rightarrow r=s\Rightarrow r=s\\ \cline{1-1}\cr\cline{3-3}\cr\Gamma\Rightarrow\forall X(X(r)\rightarrow X(s))&&\forall X(X(r)\rightarrow X(s))\Rightarrow r=s\\ \cline{1-3}\cr\lx@intercol\hfil\Gamma\Rightarrow r=s\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{cccl}\Gamma\Rightarrow F\{v/r\}&&F\{v/s\}\Rightarrow F\{v/s\}&\vbox to0.0pt{\hbox{$=\Rightarrow$}}\\ \cline{1-3}\cr\lx@intercol\hfil\Gamma,r=s\Rightarrow F\{v/s\}\hfil\lx@intercol&\end{array}$$

$$\begin{array}[]{cccccl}&&\Gamma\Rightarrow F\{v/r\}&&F\{v/s\}\Rightarrow F\{v/s\}&\vbox to0.0pt{\hbox{$=\Rightarrow$}}\\ \cline{3-5}\cr\Rightarrow s=s&&\lx@intercol\hfil\Gamma,r=s\Rightarrow F\{v/s\}\hfil\lx@intercol&\vbox to0.0pt{\hbox{$=\Rightarrow$}}\\ \cline{1-5}\cr\lx@intercol\hfil\Gamma,s=r\Rightarrow F\{v/s\}\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{clcc}\Lambda\Rightarrow F\{v/r\}&\vbox to0.0pt{\hbox{$=_{1}$}}&{}{}{}{}{}{}{}\hfil&\\ \cline{1-1}\cr\Lambda,r=s\Rightarrow F\{v/s\}&&~{}~{}~{}~{}~{}\Gamma,F\{v/s\}\Rightarrow\Delta\\ \cline{1-4}\cr\lx@intercol\hfil\Lambda,\Gamma,r=s\Rightarrow\Delta\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{clclc}\Rightarrow s=s&\vbox to0.0pt{\hbox{$=_{2}$}}{}{}{}&\Lambda\Rightarrow F\{v/r\}&\vbox to0.0pt{\hbox{$=_{2}$}}{}{}{}&\\ \cline{1-1}\cr\cline{3-3}\cr r=s\Rightarrow s=r&&\Lambda,s=r\Rightarrow F\{v/s\}&&\\ \cline{1-3}\cr\lx@intercol\hfil~{}~{}~{}~{}\Lambda,r=s\Rightarrow F\{v/s\}\hfil\lx@intercol&\Gamma,F\{v/s\}\Rightarrow\Delta\\ \cline{2-4}\cr&\lx@intercol\hfil\Lambda,\Gamma,r=s\Rightarrow\Delta\hfil\lx@intercol\par\end{array}$$

$$\begin{array}[]{clccl}\Gamma,F\{v/r\}\Rightarrow\Delta&&~{}~{}~{}\mbox{and}{}{}{}&\Gamma,F\{v/r\}\Rightarrow\Delta&\\ \cline{1-1}\cr\cline{4-4}\cr\Gamma,F\{v/s\},r=s\Rightarrow\Delta&&&\Gamma,F\{v/s\},s=r\Rightarrow\Delta\end{array}$$

$$\begin{array}[]{cccl}&&F\{v/s\}\Rightarrow F\{v/s\}~{}~{}~{}~{}\Gamma,F\{v/r\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=\Rightarrow$}}\\ \cline{3-3}\cr\Rightarrow r=r&{}{}{}\hfil&\Gamma,F\{v/s\},s=r\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=\Rightarrow$}}\\ \cline{1-3}\cr\lx@intercol\hfil\Gamma,F\{v/s\},r=s\Rightarrow\Delta\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{cl}F\{v/s\}\Rightarrow F\{v/s\}~{}~{}~{}~{}\Gamma,F\{v/r\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=\Rightarrow$ }}\\ \cline{1-1}\cr\Gamma,F\{v/s\},s=r\Rightarrow\Delta\end{array}$$

$$\begin{array}[]{cccl}&&\Lambda,F\{v/s\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=_{2}^{l}$}}\\ \cline{3-3}\cr\Gamma\Rightarrow F\{v/r\}&{}{}{}\hfil&\Lambda,F\{v/r\},r=s\Rightarrow\Delta&\\ \cline{1-3}\cr\lx@intercol\hfil\Gamma,\Lambda,r=s\Rightarrow\Delta\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{cccl}&&\Gamma,F\{v/s\}\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=_{1}^{l}$}}\\ \cline{3-3}\cr&&\Lambda,F\{v/r\},s=r\Rightarrow\Delta&\vbox to0.0pt{\hbox{$=_{1}^{l}$}}\\ \cline{3-3}\cr&\Rightarrow s=s&\Lambda,F\{v/r\},s=s,r=s\Rightarrow\Delta&\\ \cline{2-3}\cr\Gamma\Rightarrow F\{v/r\}&&\Lambda,F\{v/r\},r=s\Rightarrow\Delta&\\ \cline{1-3}\cr\lx@intercol\hfil\Gamma,\Lambda,r=s\Rightarrow\Delta\hfil\lx@intercol\par\end{array}$$

$$\begin{array}[]{clccl}\Gamma\Rightarrow\Delta,F\{v/r\}&\vbox to0.0pt{\hbox{ $=_{1}$}}~{}~{}~{}\mbox{and}{}{}{}{}&\Gamma\Rightarrow\Delta,F\{v/r\}&\vbox to0.0pt{\hbox{ $=_{2}$}}\\ \cline{1-1}\cr\cline{3-3}\cr\Gamma,r=s\Rightarrow\Delta,F\{v/s\}&&\Gamma,s=r\Rightarrow\Delta,F\{v/s\}\end{array}$$

$$\begin{array}[]{ccccc}\Gamma\Rightarrow H&{}{}{}\hfil&\Gamma_{1},F,G,\Gamma_{2}\Rightarrow H&{}{}{}\hfil&\Gamma,F,F\Rightarrow H\\ \cline{1-1}\cr\cline{3-3}\cr\cline{5-5}\cr\Gamma,F\Rightarrow H&&\Gamma_{1},G,F,\Gamma_{2}\Rightarrow H&{}{}{}\hfil&\Gamma,F\Rightarrow H\end{array}$$

$$\begin{array}[]{c}\Gamma\Rightarrow F~{}~{}~{}~{}\Lambda,F\Rightarrow H\\ \cline{1-1}\cr\Gamma,\Lambda\Rightarrow H\end{array}$$

$$\begin{array}[]{ccc}\Gamma\Rightarrow F\{v/r\}&{}{}{}{}{}{}{}\hfil&\Gamma\Rightarrow F\{v/r\}\\ \cline{1-1}\cr\cline{3-3}\cr\Gamma,r=s\Rightarrow F\{v/s\}&{}{}{}{}{}{}{}\hfil&\Gamma,s=r\Rightarrow F\{v/s\}\end{array}$$

$$\begin{array}[]{ccc}\Gamma\Rightarrow\Delta,A\{v/r\}&{}{}{}{}{}\hfil&\Gamma\Rightarrow\Delta,A\{v/r\}\\ \cline{1-1}\cr\cline{3-3}\cr\Gamma,r=s\Rightarrow\Delta,A\{v/s\}&{}{}{}{}{}\hfil&\Gamma,s=r\Rightarrow\Delta,A\{v/s\}\end{array}$$

$$\begin{array}[]{cl}F\{v/r\}\Rightarrow F\{v/r\}&\vbox to0.0pt{\hbox{$=_{1}$}}\\ \cline{1-1}\cr F\{v/r\},r=s\Rightarrow F\{v/s\}\end{array}$$

$$\begin{array}[]{c}{\cal D}\\ G\{v/s\},r=s\Rightarrow G\{v/r\}\\ \cline{1-1}\cr G\{v/s\},r=s,\neg G\{v/r\}\Rightarrow\\ \cline{1-1}\cr\neg G\{v/r\},r=s\Rightarrow\neg G\{v/s\}\end{array}$$

$$\begin{array}[]{ccc}{\cal D}&{}{}{}{}{}{}{}\hfil&{\cal E}\\ G\{v/s\},r=s\Rightarrow G\{v/r\}&&H\{v/r\},r=s\Rightarrow H\{v/s\}\\ \cline{1-3}\cr\lx@intercol\hfil G\{v/s\},r=s,r=s,G\{v/r\}\rightarrow H\{v/r\}\Rightarrow H\{v/s\}\hfil\lx@intercol\\ \cline{1-3}\cr\lx@intercol\hfil G\{v/s\},r=s,G\{v/r\}\rightarrow H\{v/r\}\Rightarrow H\{v/s\}\hfil\lx@intercol\\ \cline{1-3}\cr\lx@intercol\hfil G\{v/r\}\rightarrow H\{v/r\},r=s\Rightarrow G\{v/s\}\rightarrow H\{v/s\}\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{c}G\{v/r,x/u\},r=s\Rightarrow G\{v/s,x/u\}\\ \cline{1-1}\cr\forall xG\{v/r\},r=s\Rightarrow G\{v/s,x/u\}\\ \cline{1-1}\cr\forall xG\{v/r\},r=s\Rightarrow\forall xG\{v/s\}\end{array}$$

$$\begin{array}[]{c}\Gamma\Rightarrow\Delta,F\{v/r\}\\ \cline{1-1}\cr\Gamma,r=s\Rightarrow\Delta,F\{v/s\}\end{array}$$

Full text

1 Introduction

The most common way of treating equality in sequent calculus is to add to Gentzen’s system appropriate sequents with which derivations can start, beside the logical axioms of the form $F\Rightarrow F$ (see for example [1], [16], [17]) and [3]). In this way equality is considered and treated as a mathematical relation subject to specific axioms. For such kind of calculi Gentzen’s cut elimination theorem can hold at most in a weakened form: every derivation can be transformed into one which contains only cuts whose cut formula is an equality. That doesn’t allow to obtain directly the wealth of applications that full cut elimination has, such as the conservativity of first order logic with equality over first order logic without equality, or the disjunction and existence property for intuitionistic logic with equality. As shown in [7], the initial sequents that concern equality can be replaced by nonlogical rules in order to obtain sequent calculi for which all the structural rules, including the cut rule, are admissible. However the above nonlogical rules can eliminate equalities, so that obtaining the mentioned applications of cut elimination is not entirely straightforward (see [7], [11] or [18], for the additional work required to obtain the conservativeness of first order logic with equality over first order logic without equality). Our purpose is to overcome this difficulty by introducing a sequent calculus for which full cut elimination holds and none of the rules, other than the cut rule, eliminates equalities or any other logical constant, and moreover, to remain as close as possible to Gentzen’s system, retains the separation between structural and logical rules.

For notational semplicity and to add evidence to the logical definability of equality, throughout this introduction and the next section, we will restrict attention to intuitionistic logic.

To begin with, we observe that equality can be regarded as a logical constant, defined, according to Leibnitz’s indiscernibility principle, by letting $a=b$ to mean $\forall X(X(a)\leftrightarrow X(b))$. However, in the framework of intuitionistic second order logic, thanks to the rules for $\forall$ and $\rightarrow$, $\forall X(X(a)\leftrightarrow X(b))$ is equivalent to $\forall X(X(a)\rightarrow X(b))$. In fact $\forall X(X(b)\rightarrow X(a))$ can be deduced from $\forall X(X(a)\rightarrow X(b))$ by instantiating the bound predicate variable $X$ by the lambda term $\lambda v(Z(v)\rightarrow Z(a))$, where $Z$ is a free predicate variable, so as to obtain $(Z(a)\rightarrow Z(a))\rightarrow(Z(b)\rightarrow Z(a))$. Then, given the deducibilty, by $\rightarrow$-introduction, of $Z(a)\rightarrow Z(a)$, an $\rightarrow$-elimination followed by a $\forall$-introduction yields $\forall X(X(b)\rightarrow X(a))$ as desired. Thus as the definition of $a=b$ we can simply take $\forall X(X(a)\rightarrow X(b))$. On that respect equality stands on a par with the definition of $\wedge,\vee,\neg,\exists$ in terms of universal quantification and implication, spelled out, for example, in [12]) pg. 67. Given this definition of $=$, from the rules of Gentzen’s sequent calculus for $\forall$ and $\rightarrow$, the following left and right introduction rules for $=$:

[TABLE]

can be derived. Here and in the following $F\{v/r\}$ ($F\{v/s\}$) denotes the result of the simultaneous replacement in $F$ of all the occurrences of the free object variable $v$ by $r$ ($s$) and $Z$ is a free predicate variable that does not occur in $\Gamma$, and $|\Delta|\leq 1$. Conversely the sequents $r=s\Rightarrow\forall X(X(r)\rightarrow X(s))$ and $\forall X(X(r)\rightarrow X(s))\Rightarrow r=s$ are derivable by using the rules $=^{(2)}\Rightarrow$ and $\Rightarrow=^{(2)}$ (the details of such derivations as well as of a few others to be mentioned in this Introduction are provided in the next section of the paper). Granted Leibniz’s definition of equality, we can therefore claim that the second order version of $LJ$ supplemented by the rules $=^{(2)}\Rightarrow$ and $\Rightarrow=^{(2)}$, that we denote by $LJ^{(2)=}$, is an adequate sequent calculus to deal with equality in second order logic. The right introduction rule $\Rightarrow=^{(2)}$ turns out to be equivalent to the Reflexivity Axiom $\Rightarrow r=r$. Thus a sequent calculus for first order logic with equality can be obtained from $LJ^{(2)=}$ by replacing $\Rightarrow=^{(2)}$ by the Reflexivity Axiom and requiring that all the formulae and terms involved be first order formulae and terms.

We will denote by $=\Rightarrow$ and $\Rightarrow=$ the rule and axiom obtained in that way, and by $LJ^{(1)=}$ the sequent calculus that is obtained by adding them to Gentzen’s $LJ$. $LJ^{(1)=}$ shares with $LJ$ the distinction between structural and logical rules and the latter introduce a logical constant as the outermost symbol of exactly one formula, the so called principal formula, while the other formulae in the conclusion are those present in a determined position in the premiss or premisses and are independent from the principal one.

As we will see, full cut elimination holds for $LJ^{(1)=}$, however $LJ^{(1)=}$ is far from being a satisfactory sequent calculus for first order logic with equality, since the application of the rule $=\Rightarrow$ eliminates the formulae $F\{v/r\}$ and $F\{v/s\}$, hence all the logical constants they may contain.

Our task is therefore to find a calculus equivalent to $LJ^{(1)=}$ in which the cut rule is eliminable and all the other rules do not eliminate occurrences of logical constants. Following the lines of Gentzen’s transition from the axiomatic systems to natural deduction and then to the sequent calculus (see [9] and [10] for a detailed historical reconstruction), our starting point will be the following natural deduction elimination rule for $=$:

[TABLE]

together with the rule for its introduction, namely the zero premisses reflexivity rule $\overline{r=r}$, that correspond to the substitutivity axiom $\forall x\forall y(x=y\rightarrow(F\{v/x\}\rightarrow F\{v/y\})$ and to the reflexivity axiom $\forall x(x=x)$.

Let $NJ^{=}$ be the natural deduction system obtained by adding to $NJ$ the above introduction and elimination rules for $=$. We will pick the right and left introduction rules for $=$ to be added to $LJ$ so as to obtain a Gentzen-style sequent calculus equivalent to $NJ^{=}$, namely such that a formula $G$ is deducible from (assumptions that are listed in) $\Sigma$ if and only if $\Sigma\Rightarrow G$ is derivable in the calculus. Since $r=r$ is deducible from the empty $\Sigma$, the most obvious corresponding choice is to add to $LJ$, as the (zero premisses) right introduction rule, the Reflexivity Axiom $\Rightarrow r=r$ (already denoted by $\Rightarrow=$). Considering the correspondence between the natural deduction elimination rules and the left introduction rules of the sequent calculus, particularly those concerning the existential quantifier, it is quite natural to make correspond to $=_{1}^{N}$ the following rule:

[TABLE]

Actually, the most direct transformation in sequent terms of $=_{1}^{N}$ is the following rule, clearly equivalent to $=_{1}$ over the structural rules:

[TABLE]

($CNG$ for congruence), that will play a crucial role in the sequel. Given the equivalence between $=_{1}$ and $CNG$ it is straightforward that, if we let $LJ_{\circ}^{=}$ be the calculus obtained by adding $=_{1}$ and $=_{2}$ to $LJ$, then $LJ_{\circ}^{=}$ is equivalent to $NJ^{=}$. However, cut elimination for $LJ_{\circ}^{=}$ does not hold. For example the following derivable sequent $a=c,b=c\Rightarrow a=b$ cannot have any cut free derivation, if we adopt only $\Rightarrow=$ and $=_{1}$.

In order to have cut elimination we have to add also the following rule, obtained by replacing in $=_{1}$, $r=s$ by its symmetric $s=r$:

[TABLE]

corresponding to the following other natural deduction elimination rule for $=$:

[TABLE]

Letting $LJ^{=}$ be the result of adding to $LJ$ both $=_{1}$ and $=_{2}$ we will provide a very simple proof that cut elimination holds for $LJ^{=}$, based on the admissibility in the cut-free part of $LJ^{=}$ of the rule $CNG$ introduced above (which by itself would seem of scarce interest for the sequent calculus, since its application eliminates equalities). $LJ^{=}$ and $LJ^{(1)=}$ are equivalent and $=_{1}$ and $=_{2}$ are derivable in $LJ^{(1)=}$ without using the cut rule. Hence cut elimination for $LJ^{(1)=}$ follows as an immediate consequence of cut elimination for $LJ^{=}$.

In the light of the derivability of $=_{1}$ and $=_{2}$ in $LJ^{(1)=}$, it is quite natural to consider also the following rules: $=_{1}^{l}$ and $=_{2}^{l}$:

[TABLE]

The four equality rules $=_{1}$, $=_{2}$, $=_{1}^{l}$ and $=_{2}^{l}$ turn out to be equivalent to $=\Rightarrow$, hence to each other, over the structural rules and $\Rightarrow=$.

We will show that cut elimination holds for the systems, to be denoted by $LJ_{1}^{=}$ and $LJ_{2}^{=}$, that are obtained from $LJ$ by adding $\Rightarrow=$, $=_{1}$ and $=_{1}^{l}$ or $\Rightarrow=$, $=_{2}$ and $=_{2}^{l}$. In fact we will show that the rule $=_{2}$ is admissible in $LJ^{=}_{1}$ deprived of the cut rule and, similarly, that $=_{1}$ is admissible in $LJ^{=}_{2}$ deprived of the cut rule, so that cut elimination for both systems follows form cut elimination for $LJ^{=}$.

Despite the similarity of the pair of rules $=_{1}$ and $=_{2}$ and the pair $=_{1}^{l}$ and $=_{2}^{l}$ with respect to $LJ^{(1)=}$, the system obtained from $LJ$ by adding $\Rightarrow=$ and both $=_{1}^{l}$ and $=_{2}^{l}$ does not satisfy cut elimination. That turns out to be the case also for the systems that are obtained from $LJ$ by adding $\Rightarrow=$ together with $=_{1}$ and $=_{2}^{l}$ or $\Rightarrow=$ together with $=_{1}^{l}$ and $=_{2}$.

Furthermore we will show that if all the four equality rules are adopted, then we obtain a system $LJ^{=}_{12}$ for which cut elimination holds also if their application is required to be $\prec$-nonlengthening, with respect to any binary antisymmetric relation on terms $\prec$. We recall from [5], that an equality-inference as represented above is said to be $\prec$- nonlengthening if $s\not\prec r$. Actually we will show that cut elimination holds for the system in which all the equality-inferences are required to be $\prec$-nonlengthening and all the $=_{1}$ and $=_{1}^{l}$-inferences are required to be $\prec$-shorthening, namely to satisfy the stronger condition $r\prec s$. Alternatively we can require that all the equality-inferences be $\prec$-nonlengthening and all the $=_{2}$ and $=_{2}^{l}$-inferences be $\prec$-shorthening.

All the above results hold without any essential change for the classical version of the calculi considered, in particular for the classical version $LK^{=}$ of $LJ^{=}$.

The union $LK^{=}_{12}$ of the systems $LK^{=}_{1}$ and $LK^{=}_{2}$ is equivalent, on the ground of the exchange and contraction rules only, to the system $G^{e}$ in [5], that was motivated by the calculus free of structural rules introduced in [4], for efficient proof search purposes. Therefore we have a proof that, as announced in [5], $G^{e}$ satisfies cut elimination. Finally, improving the result stated in [8], for any antisymmetric relation $\prec$ on terms, we will show that any derivation in $LK^{=}_{12}$, can be transformed into a cut-free derivation in the same system of its endsequent, whose equality inferences are $\prec$-nonlengthening or $\prec$- shortening, as explained above for the intuitionistic case.

1.1 Basic Derivations

Having defined $r=s$ as $\forall X(X(r)\rightarrow X(s)$, the conclusion of the rule $=^{(2)}\Rightarrow$, namely

[TABLE]

can be derived from its premisses by applying first the left introduction rule for $\rightarrow$ and then the second order left introduction rule for $\forall$, while the conclusion of $\Rightarrow=^{(2)}$, namely

[TABLE]

can be derived from its premiss by applying first the right introduction rule for $\rightarrow$ and then the second order right introduction rule for $\forall$.

Conversely the sequents $r=s\Rightarrow\forall X(X(r)\rightarrow X(s)$ and $\forall X(X(s)\rightarrow X(r)\Rightarrow r=s$ can be derived by means of $=^{(2)}\Rightarrow$ and $\Rightarrow=^{(2)}$ as follows:

[TABLE]

where we have omitted the applications of the exchange rule, as we will do throughout the paper.

$\Rightarrow r=r$ is immediately derived by $\Rightarrow=^{(2)}$ applied to the logical axiom $Z(r)\Rightarrow Z(r)$ and, conversely, $\Rightarrow=^{(2)}$, can be derived from $\Rightarrow r=r$, by using the cut rule, as follows:

[TABLE]

Concerning the equivalence between $LJ^{=}$ and $LJ^{(1)=}$ we note that both $=_{1}$ and $=_{2}$ are derivable from $=\Rightarrow$, without using the cut rule. In fact we have the following derivations of $=_{1}$ and $=_{2}$ respectively:

[TABLE]

[TABLE]

where the last inference is a correct application of $=\Rightarrow$ in which the place of $F$ is taken by $v=s$. Conversely, by using the cut rule, $=\Rightarrow$ can be derived from $=_{1}$ and also from $=_{2}$ as follows:

[TABLE]

[TABLE]

Therefore it would suffice to add $\Rightarrow=$ and $=_{1}$ or $\Rightarrow=$ and $=_{2}$ to $LJ$ in order to have a system equivalent to $LJ^{(1)=}$.

As for $=_{1}^{l}$ and $=_{2}^{l},$ namely:

[TABLE]

we have the following derivations in $LJ^{(1)=}$:

[TABLE]

and

[TABLE]

Conversely the rule $=\Rightarrow$ can be derived from $=_{2}^{l}$ or $\Rightarrow=$ and $=_{1}^{l}$ as follows:

[TABLE]

[TABLE]

Therefore $=_{1}$, $=_{2}$, $=_{1}^{l}$ and $=_{2}^{l}$ are all equivalent to $=\Rightarrow$, and therefore to each other, over $\Rightarrow=$ and the structural rules.

1.2 Transformation of derivations into separated form

In the following $LJ$ and $LK$ will denote the sequent calculi introduced by Gentzen in [2], except that, as in [16], in the left introduction rule $\forall\Rightarrow$ for $\forall$ and in the right introduction rule $\Rightarrow\exists$ for $\exists$ the free object variable is replaced by an arbitrary term. Clearly what has been said so far about $LJ$ holds for $LK$ as well, with the obvious changes in the presentation of the rules, needed to allow the possible presence of more than one formula in the succedent of the sequents.

$LJ^{=}$ and $LK^{=}$ are obtained by adding to $LJ$ and $LK$, the equality rules $=_{1}$ and $=_{2}$, namely

[TABLE]

where $v$ is a free object variable that occurs neither in $r$ nor in $s$ and, in the case of $LJ^{=}$, $\Delta=\emptyset$. Notice that the requirement on $v$ is not restrictive since $F\{v/r\}$ and $F\{v/s\}$ can always be represented as $(F\{v/v^{\prime}\})\{v^{\prime}/r\}$ and $(F\{v/v^{\prime}\})\{v^{\prime}/s\}$ for any $v^{\prime}$ that is new to $F$, $r$ and $s$. If $v$ does not occur in $F$, $=_{1}$ and $=_{2}$ reduce to a left weakening, introducing $r=s$, and are said to be trivial. $r=s$ in the presentation of $=_{1}$ and $s=r$ in the presentation of $=_{2}$, will be called the operating equality, while $F$ will be called the changing formula (in the representation) of $=_{1}$ and $=_{2}$ .

At the purely equational level, $LJ^{=}$ and $LK^{=}$ are equivalent, namely a sequent $\Gamma\Rightarrow F$ is derivable in $LJ^{=}$ without applications of logical rules, if and only if it is derivable in $LK^{=}$, without applications of logical rules. In fact a straightforward induction on the height of derivations establishes the following:

PROPOSITION 1.1

If a sequent $\Gamma\Rightarrow\Delta$ is derivable in $LK^{=}$ without applications of logical rules, then there is a formula $F$ in $\Delta$ such that $\Gamma\Rightarrow F$ has a derivation without applications of logical rules, that contains only sequents with exactly one formula in the succedent. In particular $\Gamma\Rightarrow$ is not derivable in $LK^{=}$ without applications of logical rules.

Proposition 1.1 motivates the following definition:

DEFINITION 1.1

$EQ$* is the calculus acting on sequents with one formula in the succedent, having the logical axioms $F\Rightarrow F$, the reflexivity axioms $\Rightarrow t=t$; the weak left structural rules of weakening, exchange and contraction:*

[TABLE]

the cut rule:

[TABLE]

and the equality left introduction rules $=_{1}$ and $=_{2}$:

[TABLE]

.

Our proof of cut elimination for $LJ^{=}$ and $LK^{=}$ will split into two parts. First we show that every derivation can be tranformed into one that consists of derivations in $EQ$ followed by applications of weak structural rules, namely structural rules different from the cut rule, and logical rules only, and then that cut elimination holds for $EQ$.

DEFINITION 1.2

A derivation in $LJ^{=}$ or $LK^{=}$ is said to be separated if it consists of derivations in $EQ$, followed by applications (possibly none) of logical and weak structural rules (both left and right)

In order to prove that every derivation can be transformed into a separated derivation of its endsequent, we prove first that, thanks to the cut rule, the equality rules can be derived from their special case in which the formula that they transform is atomic, and then that the cut rule is admissible over its restriction to atomic cut formulae.

LEMMA 1.1

The sequents of the following form:

• a)

$F\{v/r\},r=s\Rightarrow F\{v/s\}$**

• b)

$F\{v/r\},s=r\Rightarrow F\{v/s\}$**

have derivations whose equality inferences are atomic, manely have the form

[TABLE]

where $A$ is required to be an atomic formula.

Proof We proceed by induction on the degree of $F$. If $F$ is atomic, for $a)$ it suffices to consider

[TABLE]

As for $b)$ it suffices to replace $=_{1}$ by $=_{2}$.

If $F$ is $\neg G$, to establish $a)$, we apply the induction hypothesis $b)$ to $G$, according to which there is a derivation ${\cal D}$, whose equality inferences are atomic, of $G\{v/s\},r=s\Rightarrow G\{v/r\}$. Then the following is the desired derivation:

[TABLE]

$b)$ is established in a similar way by using the induction hypothesis $a)$ applied to $G$.

If $F$ is $G\rightarrow H$, to establish $a)$ we apply the induction hypothesis $b)$ to $G$ and $a)$ to $H$ according to which there are derivations ${\cal D}$ and ${\cal E}$ of $G\{v/s\},r=s\Rightarrow G\{v/r\}$ and $H\{v/r\},r=s\Rightarrow H\{v/s\}$ respectively, whose equality inferences are atomic. Then the following derivation establishes $a)$ for $F$:

[TABLE]

$b)$ for $F$ is established in a similar way, except that we have to use the induction hypothesis $a)$ on $G$ and $b)$ on $H$.

If $F$ is $\forall xG$, we let $u$ be any parameter not occurring in $G,r,s$ and apply the induction hypothesis $a)$ to $G\{x/u\}$ to obtain a derivation ${\cal D}$, whose equality inferences are atomic, of $G\{v/r,x/u\},r=s\Rightarrow G\{v/s,x/u\}$. Then the following derivation establishes $a)$ for $F$:

[TABLE]

$b)$ for $F$ is established in the same way except that we use the induction hypothesis $b)$, rather than $a)$, on $G\{x/u\}$.

The other cases are similar and we omit the details $\Box$

PROPOSITION 1.2

Any non atomic equality inference in a given derivation in $LJ^{=}$ or $LK^{=}$ can be replaced by a cut between its premiss and the endsequent of a derivation that uses only atomic equality inferences. In particular any derivable sequent in $LJ^{=}$ or $LK^{=}$ has a derivation whose equality inferences are all atomic.

Proof A non atomic $=_{1}$-inference of the form:

[TABLE]

can be replaced by:

[TABLE]

where ${\cal D}$ is the derivation containing only atomic equality-inferences of Lemma 1.1 $a)$ for $F$. A non atomic $=_{2}$-inference is eliminated in a similar way using Lemma 1.1 $b)$. $\Box$

Notation In the following $A$ will always denote an atomic formula and $\Gamma\sharp F$ will denote any sequence of formulae from which $\Gamma$ can be obtained by eliminating any number, possibly none, of occurrences of $F$.

PROPOSITION 1.3

If $\Gamma\Rightarrow\Delta\sharp F$ and $\Lambda\sharp F\Rightarrow\Theta$ have derivations in $LJ^{=}$ or $LK^{=}$ whose equality and cut-inferences are atomic, then also $\Gamma,\Lambda\Rightarrow\Delta,\Theta$ has a derivation in the same system whose equality and cut-inferences are atomic.

Proof Let ${\cal D}$ and ${\cal E}$ be derivations of $\Gamma\Rightarrow\Delta\sharp F$ and $\Lambda\sharp F\Rightarrow\Delta$ whose equality and cut-inferences are atomic. If $\Delta\sharp F$ coincides with $\Delta$ or $\Lambda\sharp F$ coincides with $\Lambda$, then the desired derivation of $\Gamma,\Lambda\Rightarrow\Delta,\Theta$ can be simply obtained by applying some weakenings to the end sequent $\Gamma\Rightarrow\Delta$ of ${\cal D}$ or some exchanges and weakenings to the endsequent $\Lambda\Rightarrow\Theta$ of ${\cal E}$. We can therefore assume that in $\Delta\sharp F$ there are occurrences of $F$ that are not listed in $\Delta$ and similarly for $\Lambda\sharp F$. If $F$ occurs in $\Delta$, then from $\Gamma\Rightarrow\Delta\sharp F$ we can derive $\Gamma\Rightarrow\Delta$ by means of exchanges and contractions, and from $\Gamma\Rightarrow\Delta$ we can then derive $\Gamma,\Lambda\Rightarrow\Delta,\Theta$ as in the previous case. Similarly if $F$ occurs in $\Lambda$. We can therefore assume that $F$ occurs in $\Delta\sharp F$ and in $\Lambda\sharp F$ but it does not occur in $\Delta,\Lambda$. Furthermore we can assume that $F$ does not occur in $\Gamma,\Theta$ either, for, otherwise $\Gamma,\Lambda\Rightarrow\Delta,\Theta$ can be derived by weakening ${\cal D}$, if $F$ occurs in $\Theta$, or ${\cal E}$, if $F$ occurs in $\Gamma$, and then contracting the occurrences of $F$ in $\Delta\sharp F$ with one of the occurrences of $F$ in $\Theta$ or the occurrences of $F$ in $\Lambda\sharp F$ with one of the occurrences of $F$ in $\Gamma$. Finally if $F$ is atomic it suffices to contract the occurrence in $F$ in $\Delta\sharp F$ and $\Lambda\sharp F$ into a single one, and then apply, possibly after some exchanges, a cut with the atomic cut formula $F$, in order to obtain the desired derivation.

In the remaining cases we proceed, as in Gentzen’s original proof of the cut elimination theorem, by a principal induction on the degree of $F$ and a secondary induction on the sum of the left rank $\rho_{l}(F,{\cal D})$ of $F$ in ${\cal D}$ and of the right rank $\rho_{r}(F,{\cal E})$ of $F$ in ${\cal E}$, defined as the largest number of consecutive sequents in a path of ${\cal D}$ (of ${\cal E}$) starting with the endsequent, that contain $F$ in the succedent (in the antecedent).

Besides the cases considered in Gentzen’s proof, there is also the possibility that ${\cal D}$ or ${\cal E}$ end with an atomic equality inference or with an atomic cut.

Case 1 ${\cal D}$ ends, say, with an atomic $=_{1}$-inference. Since $F$ is not atomic, $F$ is not active in such an inference and ${\cal D}$ can be represented as:

[TABLE]

where $\Gamma^{\prime},r=s$ coincides with $\Gamma$ and $\Delta^{\prime},A\{v/s\}$ coincides with $\Delta$. Since $\rho_{l}(F,{\cal D}_{0})<\rho_{l}(F,{\cal D})$, by induction hypothesis we have a derivation whose equality and cut-inferences are atomic of $\Gamma^{\prime},\Lambda\Rightarrow\Delta^{\prime},A\{v/r\},\Theta$, from which the desired derivation of $\Gamma,\Lambda\Rightarrow\Delta,\Theta$ can be obtained by applying the same $=_{1}$-inference.

Case 2 ${\cal D}$ ends with an atomic cut. Then ${\cal D}$ can be represented as:

[TABLE]

where $\Delta$ coincides with $\Delta_{1},\Delta_{2}$, so that $F$ does not occur in $\Delta-1$ nor in $\Delta_{2}$. Since $\rho_{l}(F,{\cal D}_{0})<\rho_{l}(F,{\cal D})$ and $\rho_{l}(F,{\cal D}_{1})<\rho_{l}(F,{\cal D})$, by induction hypothesis applied to ${\cal D}_{0}$ and ${\cal E}$ and to ${\cal D}_{1}$ and ${\cal E}$ there are derivations whose equality and cut-inferences are atomic of $\Gamma_{1},\Lambda\Rightarrow\Delta_{1},A,\Theta$ and $\Gamma_{2},A,\Lambda\Rightarrow\Delta_{2},\Theta$, to which it suffices to apply a cut with atomic cut formula $A$ ad then some exchanges and contraction to have the desired derivation of $\Gamma_{1},\Gamma_{2},\Lambda\Rightarrow\Delta_{1},\Delta_{2},\Theta$.

The cases in which it is ${\cal E}$ to end with an atomic equality or a cut-inference are entirely analogous. $\Box$.

From Proposition 1.2 and Proposition 1.3 it follows immediately the following:

PROPOSITION 1.4

Every derivation in $LJ^{=}$ or $LK^{=}$ can be transformed into a derivation of its endsequent, whose equality and cut-inferences are atomic.

**Remark ** For the proof of Proposition 1.3 it is crucial that the equality rules transform atomic formulae only. For example in case $\rho_{l}(F,{\cal D})=1$ and $\rho_{r}(F,{\cal E})=1$, if $F$ had the form $F^{\circ}\{v/s\}$, with $F^{\circ}$ non atomic, ${\cal D}$ ended with an equality inference transforming $F^{\circ}\{v/r\}$ into $F^{\circ}\{v/s\}$, and ${\cal E}$ by a logical inference introducing $F^{\circ}\{v/s\}$ in the antecedent, then there would be no way of applying the induction hypothesis.

Note Concerning the use of $\Gamma\sharp F$, we note that when $\Delta\sharp F$ and $\Lambda\sharp F$ take the form $\Delta,F$ and $\Gamma,F$, from Proposition 1.3, we obtain directly that the derivations having only atomic equality and cut-inferences are closed under the application of the cut rule. That is a slight simplification with respect to the use of Gentzen’s mix rule that eliminates all the occurrences of $F$, so that the use of additional weakenings and exchanges may be necessary to derive the conclusion of a cut-inference.

PROPOSITION 1.5

If $~{}\Gamma\Rightarrow\Delta\sharp A\{v/r\}$ has a separated derivation in $LJ^{=}$ or $LK^{=}$, then also $\Gamma,r=s\Rightarrow\Delta,A\{v/s\}$ and $\Gamma,s=r\Rightarrow\Delta,A\{v/s\}$ have separated derivations in the same system.

Proof Let ${\cal D}$ be a separated derivation of $\Gamma\Rightarrow\Delta\sharp A\{v/r\}$. We proceed by induction on the height $h({\cal D})$ of ${\cal D}$. In the base case ${\cal D}$ reduces to an axiom and it suffices to apply an $=_{1}$ or an $=_{2}$-inference to the axiom itself. If $h({\cal D})>0$ we have the following cases.

Case 1. ${\cal D}$ ends with a cut or an equality-inference. In this case ${\cal D}$ doesn’t contain any logical inference. If $\Delta=\Delta\sharp A\{v/r\}$, then it suffices to weaken the endsequent of ${\cal D}$. Otherwise we can contract all the occurrences of $A\{v/r\}$ not belonging to $\Delta$ into a single one and then apply an $=_{1}$ or $=_{2}$-inference.

Case 2 ${\cal D}$ ends with a weak structural inference. If such an inference involves one of the occurrences of $A\{v/r\}$ in $\Delta\sharp A\{v/r\}$ not belonging to $\Delta$, then the desired derivation is provided directly by the induction hypothesis. Otherwise the latter is obtained by applying the induction hypothesis and then the same weak structural rule.

Case 3 ${\cal D}$ ends with a logical rule. $A\{v/r\}$, being atomic, cannot be the principal formula of the inference, and the conclusion is a straightforward consequence of the induction hypothesis. For example if ${\cal D}$ has the form:

[TABLE]

where $\Gamma$ coincides with $\Gamma_{0},\Gamma_{1},F\rightarrow G$,and $\Delta$ with $\Delta_{0},\Delta_{1}$, by induction hypothesis we have separated derivation ${\cal D}^{\prime}_{0}$ and ${\cal D}_{1}^{\prime}$ of $\Gamma_{0},r=s\Rightarrow\Delta_{0},A\{v/s\},F$ and $\Gamma_{1},G,r=s\Rightarrow A\{v/s\}$. Then

[TABLE]

is a separated derivation of $\Gamma,r=s\Rightarrow\Delta,A\{v/s\}$. $\Box$

PROPOSITION 1.6

If $\Gamma\Rightarrow\Delta\sharp A$ and $\Lambda\sharp A\Rightarrow\Theta$ have separated derivations in $LJ^{=}$ or $LK^{=}$, then also $\Gamma,\Lambda\Rightarrow\Delta,\Theta$ has a separated derivation in the same system.

Proof. Let ${\cal D}$ and ${\cal E}$ be separated derivations of $\Gamma\Rightarrow\Delta\sharp A$ and $\Lambda\sharp A\Rightarrow\Theta$ respectively. If $\Delta\sharp A=\Delta$ or $\Lambda\sharp A=\Lambda$ the desired derivation can be obtained by weakening the conclusion of ${\cal D}$ or of ${\cal E}$. If both ${\cal D}$ and ${\cal E}$ end with an equality-inference of with a cut, then ${\cal D}$ and ${\cal E}$, being separated, do not contain any logical inference. Then it suffices to contract all the occurrences of $A$ in $\Delta\sharp A$ not occurring in $\Delta$ and, similarly, all those occurring in $\Lambda\sharp A$ but not in $\Lambda$, into a single one, and apply an atomic cut on $A$. If ${\cal D}$ or ${\cal E}$, say ${\cal D}$, ends with a weak structural inference or with a logical inference, we proceed by induction on the sum $h({\cal D})+h({\cal E})$ of the heights of ${\cal D}$ and ${\cal E}$.

Case 1 ${\cal D}$ ends with a weak structural inference. If such an inference involve one of the occurrences of $A\{v/r\}$ in $\Delta\sharp A\{v/r\}$ not belonging to $\Delta$, then the desired derivation is provided directly by the induction hypothesis. Otherwise the latter is obtained by applying the induction hypothesis and then the same weak structural rule.

Case 2 ${\cal D}$ ends with a logical inference. Since $A$ is atomic, $A$ is not the principal formula of such an inference. Then the conclusion follows by a straightforward induction on $h({\cal D})+h({\cal E})$. For example if ${\cal D}$ is of the form:

[TABLE]

By induction hypothesis applied to ${\cal D}_{0}$ and ${\cal E}$ and to ${\cal D}_{1}$ and ${\cal E}$ we have two separated derivations of $\Gamma^{\prime},F,\Lambda\Rightarrow\Delta,\Theta$ and $\Gamma^{\prime},G,\Lambda\Rightarrow\Delta,\Theta$, from which by a $\vee\Rightarrow$-inference we obtain the desired derivation of $\Gamma^{\prime},F\vee G\Rightarrow\Delta,\Theta$.

The cases in which it is ${\cal E}$ to end with a weak structural inference or with a cut are entirely analogous. $\Box$

PROPOSITION 1.7

Every derivable sequent in $LJ^{=}$ or $LK^{=}$ has a separated derivation in the same system,

Proof Assume we are given a non separated derivation ${\cal D}$ of $\Gamma\Rightarrow\Delta$ in $LJ^{=}$ or $LK^{=}$. By Proposition 1.4, ${\cal D}$ can be transformed into a derivation ${\cal D}^{\prime}$ whose equality and cut-inferences are atomic. Then a straightforward induction on the height of ${\cal D}^{\prime}$, based on Proposition 1.5 and Proposition 1.6 shows that ${\cal D}^{\prime}$ can be transformed into a separated derivation of $\Gamma\Rightarrow\Delta$. $\Box$

By the previous Proposition 1.7, to show that the cut rule is eliminable from derivations in $LJ^{=}$ or $LK^{=}$ it suffices to show that it can be eliminated from the derivations of the purely equational calculus $EQ$. Instrumental for that pourpose will be the following equational calculus $EQ_{N}$, where $N$ stands for natural.

DEFINITION 1.3

$EQ_{N}$* is the calculus acting on sequents with one formula in the succedent, obtained from $EQ$ by replacing the rules $=_{1}$ and $=_{2}$ with the rule $CNG$:*

[TABLE]

DEFINITION 1.4

$cf.EQ$* and $cf.EQ_{N}$ denote the systems $EQ$ and $EQ_{N}$ deprived of the cut rule.*

PROPOSITION 1.8

EQ and $EQ_{N}$ are equivalent.

Proof The following are derivations of $=_{1}$ and $=_{2}$ from $CNG$ and of $CNG$ from $=_{1}$:

[TABLE]

[TABLE]

[TABLE]

$\Box$

1.3 Cut-elimination for $EQ_{N}$

PROPOSITION 1.9

If $\Gamma\Rightarrow F$ and $\Lambda\sharp F\Rightarrow G$ are derivable in $cf.EQ_{N}$, then also $\Gamma,\Lambda\Rightarrow G$ is derivable in $cf.EQ_{N}$.

Proof Let ${\cal D}$ and ${\cal E}$ be derivations in $cf.EQ$ of $\Gamma\Rightarrow F$, and $\Lambda\sharp F\Rightarrow G$ respectively. We have to show that there is a derivation ${\cal F}$ in $cf.EQ$ of $\Gamma,\Lambda\Rightarrow G$.

If $\Lambda\sharp F$ coincides with $\Lambda$, in particular if $\Lambda\sharp F$ is empty, or $F$ occurs in $\Lambda$, then to obtain ${\cal F}$ it suffices to add to ${\cal E}$ the weakenings, exchanges and, in the latter case, contractions needed to obtain $\Gamma,\Lambda\Rightarrow G$. Otherwise we proceed by induction on the height $h({\cal E})$ of ${\cal E}$. If $h({\cal E})=0$, then ${\cal E}$ reduces to $F\Rightarrow F$ and for ${\cal F}$ we can take ${\cal D}$ itself.

If ${\cal E}$ ends with a weak structural inference that involves (at least) one of the occurrences of $F$ in $\Lambda\sharp F$, that does not occur in $\Lambda$, then the desired derivation ${\cal F}$ is provided directly by the induction hypothesis. Otherwise it suffices to apply the induction hypothesis and then the last weak structural inference of ${\cal E}$.

If ${\cal E}$ ends with a $CNG$-inference, then $G$ has the form $H\{v/s\}$ and ${\cal E}$ can be represented as:

[TABLE]

By induction hypothesis we have cut-free derivations of $\Gamma,\Lambda_{0}\Rightarrow H\{v/r\}$ and $\Gamma,\Lambda_{1}\Rightarrow r=s$, from which ${\cal F}$ is obtained by applying the same $CNG$-inference and some exchanges and contractions. $\Box$

PROPOSITION 1.10

If a sequent is derivable in $EQ_{N}$, then it is also derivable in $cf.EQ_{N}$.

Proof By the previous Proposition, applied in the specific case in which $\Lambda\sharp F$ is $\Lambda,F$, it follows that the cut rule is admissible in $cf.EQ_{N}$ and therefore eliminable from derivations in $EQ_{N}$. $\Box$

1.4 Cut elimination for $LJ^{=}_{N}$ and $LK^{=}_{N}$

From Proposition 1.7 , Proposition 1.8 and Proposition 1.10 we obtain the full cut elimination theorem for the calculi $LJ_{N}^{=}$ and $LK_{N}^{=}$, that are obtained by adding to $LJ$ and $LK$ the Reflexivity Axiom $\Rightarrow=$ and the rule $CNG$.

THEOREM 1.1

The cut rule is eliminable from derivations in $LJ_{N}^{=}$ and in $LK_{N}^{=}$.

1.5 Admissibility of $CNG$ in $cf.EQ$

PROPOSITION 1.11

The rule $CNG$ is admissible in $cf.EQ$, namely, if $\Gamma\Rightarrow F\{v/r\}$ and $\Lambda\Rightarrow r=s$ are derivable in $cf.EQ$ then also $\Gamma,\Lambda\Rightarrow F\{v/s\}$ is derivable in $cf.EQ$.

Proof Let ${\cal D}$ and ${\cal E}$ be derivations in $cf.EQ$ of $\Gamma\Rightarrow F\{v/r\}$ and $\Lambda\Rightarrow r=s$ respectively. We have to show that there is a derivation ${\cal F}$ of $\Gamma,\Lambda\Rightarrow F\{v/s\}$ in $cf.EQ$. If $r$ and $s$ coincide, to obtain ${\cal F}$ it suffices to apply to the end-sequent of ${\cal D}$ the appropriate weakenings to introduce $\Lambda$ in the antecedent of its end-sequent. Otherwise we proceed by induction on the height of ${\cal E}$, with respect to an arbitrary ${\cal D}$. In the base case ${\cal E}$ reduces to the axiom $r=s\Rightarrow r=s$. In that case as ${\cal F}$ we can take:

[TABLE]

that uses $=_{1}\Rightarrow$. If ${\cal E}$ ends with a structural rule, to obtain ${\cal F}$ it suffices to apply the induction hypothesis to ${\cal D}$ and to the immediate subderivation ${\cal E}_{0}$ of ${\cal E}$ and then the last structural rule of ${\cal E}$.

If ${\cal E}$ ends with a $=_{1}\Rightarrow$-inference, namely it is of the form:

[TABLE]

so that $r$ and $s$ are $r^{\circ}\{u/q\}$ and $s^{\circ}\{u/q\}$ respectively, and $\Lambda$ is $\Lambda^{\prime},p=q$, let ${\cal D}^{\prime}$ be the following derivation:

[TABLE]

which uses $=_{2}$. By induction hypothesis applied to ${\cal D}^{\prime}$ and ${\cal E}_{0}$ there is a derivation ${\cal F}_{0}$ of $\Gamma,p=q,\Lambda^{\prime}\Rightarrow F\{v/s^{\circ}\{u/p\}\}$. As ${\cal F}$ we can then take the following derivation:

[TABLE]

which uses $=_{1}\Rightarrow$ and a contraction.

Finally if ${\cal E}$ ends with a $=_{2}$-inference, namely it is of the form:

[TABLE]

We let ${\cal D}^{\prime}$ be :

[TABLE]

which uses $=_{1}\Rightarrow$. By induction hypothesis applied to ${\cal D}^{\prime}$ e ${\cal E}_{0}$ we obtain a derivation ${\cal F}_{0}$ of $\Gamma,q=p,\Lambda^{\prime}\Rightarrow F\{v/s^{\circ}\{u/p\}\}$. Then, as ${\cal F}$ we take the following derivation:

[TABLE]

which uses $=_{2}$ and a contraction. $\Box$

1.6 Cut elimination for $EQ$

THEOREM 1.2

Cut elimination for $EQ$.

If $\Gamma\Rightarrow F$ is derivable in $EQ$, then it is derivable also in $cf.EQ$

Proof By Proposition 1.8 a derivation ${\cal D}$ of $\Gamma\Rightarrow F$ in $EQ$ can be transformed into a derivation ${\cal D}^{\prime}$ in $EQ_{N}$ of $\Gamma\Rightarrow F$. By the eliminability of the cut-rule in $EQ_{N}$, ${\cal D}^{\prime}$ can be transformed into a derivation ${\cal D}^{\prime\prime}$ in $cf.EQ_{N}$ of $\Gamma\Rightarrow F$. Finally by the admissibility of $CNG$ in $cf.EQ$, ${\cal D}^{\prime\prime}$ can be transformed into a derivation in $cf.EQ$ of $\Gamma\Rightarrow F$. $\Box$

1.7 Cut elimination for $LJ^{=}$ and $LK^{=}$

From Proposition 1.7 and Theorem1.2 we obtain the full cut elimination theorem for $LJ^{=}$ and $LK^{=}$.

THEOREM 1.3

The cut rule is eliminable from derivations in $LJ^{=}$ and in $LK^{=}$.

1.8 Cut elimination for $LJ^{(1)=}$ and $LK^{(1)=}$

Since, the rules $=_{1}$ and $=_{2}$ are derivable in $LJ^{(1)=}$, without using the cut rule, from cut elimination for $LJ^{=}$ it follows immediately that cut elimination holds also for $LJ^{(1)=}$ and $LK^{(1)=}$:

THEOREM 1.4

The cut rule is eliminable from derivations in $LJ^{(1)=}$ and in $LK^{(1)=}$.

1.9 Admissibility of $=_{1}^{l}$ and $=_{2}^{l}$ in $cf.EQ$

Since $=_{1}^{l}$ and $=_{2}^{l}$, namely:

[TABLE]

are derivable in $EQ$ and the cut rule is eliminable from derivations in $EQ$ we immediately have the following:

PROPOSITION 1.12

The rules $=_{1}^{l}$ and $=_{2}^{l}$ are admissible in $cf.EQ$.

DEFINITION 1.5

Let $EQ_{1}$ be obtained from $EQ$ by replacing $=_{2}$ by $=_{1}^{l}$ and $EQ_{2}$ be obtained from $EQ$ by replacing $=_{1}$ by $=_{2}^{l}$ . $cf.EQ_{1}$ and $cf.EQ_{2}$ denote $EQ_{1}$ and $EQ_{2}$ deprived of the cut rule.

1.10 Admissibility of $=_{2}$ in $EQ_{1}$ and of $=_{1}$ in $EQ_{2}$

Notation In the following $E\equiv E^{\prime}$ will denote syntactic equality between the terms or formulae that are denoted by $E$ and $E^{\prime}$.

As already noted in [5] we have the following:

LEMMA 1.2

The equality rules $=_{1}$ and $=_{2}$ as well as $=_{1}^{l}$ and $=_{2}^{l}$ are derivable by means of the contraction rule from their singleton version, obtained by requiring that $v$ has exactly one occurrence in the changing formula.

Proof It suffices to deal with $=_{1}$, the other cases being entirely similar.

Given $F$ with $n$ occurrence of $v$, with $n>1$, let $F^{\prime}$ be obtained from $F$ by replacing all the occurrences of $v$ by $n$ new (to $F$, $r$ and $s$) distinct variables $v_{1},\ldots,v_{n}$, so that $F\{v/r\}\equiv F^{\prime}\{v_{1}/r,\ldots,v_{n}/r\}$ and $F\{v/s\}\equiv F^{\prime}\{v_{1}/s,\ldots,v_{n}/s\}$.

[TABLE]

is a correct application of the singleton version of $=_{1}$, since $F^{\prime}\{v_{1}/r,\ldots,v_{n-1}/r_{n-1},v_{n}/r_{n}\}\equiv F^{\prime}\{v_{1}/r,\ldots,v_{n-1}/r\}\{v_{n}/r\}$ and $F^{\prime}\{v_{1}/r,\ldots,v_{n-1}/r\}\{v_{n}/s\}\equiv F^{\prime}\{v_{1}/r,\ldots,v_{n-1}/r,v_{n}/s\}$. Similarly, since $F^{\prime}\{v_{1}/r,\ldots,v_{n-2}/r,v_{n-1}/r,v_{n}/s\}\equiv F^{\prime}\{v_{1}/r,\ldots,v_{n-2}/r,v_{n}/s\}\{v_{n-1}/r\}$ and $F^{\prime}\{v_{1}/r,\ldots,v_{n-2}/r,v_{n}/s\}\{v_{n-1}/s\}\equiv F^{\prime}\{v_{1}/r,\ldots,v_{n-2}/r,v_{n-1}/s,v_{n}/s\}$ the following it is a correct application of $=_{1}$:

[TABLE]

Proceeding in that way, with $n$ applications of the singleton $=_{1}$-rule we obtain a derivation from $\Gamma\Rightarrow F\{v/r\}$ of $\Gamma,r=s,\ldots,r=s\Rightarrow F\{v/s\}$, from which the desired derivation of $\Gamma,r=s\Rightarrow F\{v/s\}$ can be obtained by $n-1$ applications of the contraction rule. $\Box$

DEFINITION 1.6

$cf.EQ^{1}_{1}$* and $cf.EQ^{1}_{2}$, are obtained from $cf.EQ_{1}$ and $cf.EQ_{2}$ by replacing the equality rules by their singleton version.*

PROPOSITION 1.13

$=_{2}$* is admissible in $cf.EQ_{1}$ and $=_{1}$ is admissible in $cf.EQ_{2}$.*

Proof By the previous Lemma 1.2 it suffices to prove that the singleton versions of $=_{2}$ and $=_{1}$ are admissible in the systems $cf.EQ^{1}_{1}$ and $cf.EQ^{1}_{2}$, namely that:

$a)$ if $\Gamma\Rightarrow F\{v/r\}$ is derivable in $cf.EQ^{1}_{1}$, then also $\Gamma,s=r\Rightarrow F\{v/s\}$ is derivable in $cf.EQ^{1}_{1}$, and

$b)$ if $\Gamma\Rightarrow F\{v/r\}$ is derivable in $cf.EQ^{1}_{2}$, then also $\Gamma,r=s\Rightarrow F\{v/s\}$ is derivable in $cf.EQ^{1}_{2}$.

As for $a)$, let ${\cal D}$ be a derivation in $cf.EQ^{1}_{1}$ of $\Gamma\Rightarrow F\{v/r\}$. We proceed by induction on the height $h({\cal D})$ of ${\cal D}$ to show that in $cf.EQ^{1}_{1}$ there is a derivation ${\cal D}^{\prime}$ of $\Gamma,s=r\Rightarrow F\{v/s\}$. If $h({\cal D})=0$ then ${\cal D}$ reduces to $F\{v/r\}\Rightarrow F\{v/r\}$ or to $\Rightarrow t_{0}=t_{1}\{v/r\}$, with $t_{0}\equiv t_{1}\{v/r\}$ or to $\Rightarrow t_{0}\{v/r\}=t_{1}$, with $t_{0}\{v/r\}\equiv t_{1}$ In the former case as ${\cal D}^{\prime}$ we can take:

[TABLE]

If ${\cal D}$ reduces to $\Rightarrow t_{0}=t_{1}\{v/r\}$, with $t_{0}\equiv t_{1}\{v/r\}$ as ${\cal D}^{\prime}$ we can take:

[TABLE]

which is correct since $t_{0}\equiv t_{1}\{v/r\}$. The case in which ${\cal D}$ reduces to $\Rightarrow t_{0}\{v/r\}=t_{1}$, with $t_{0}\{v/r\}\equiv t_{1}$, is entirely similar.

If $h({\cal D})>0$, and ${\cal D}$ ends with a structural rule the conclusion is a straightforward consequence of the induction hypothesis. If ${\cal D}$ ends with a $=_{1}$-inference, then we distinguish the following three subcases.

Case 1. ${\cal D}$ is of the form:

[TABLE]

with $F\equiv F^{\circ}\{u/q\}$ and the unique occurrence of $v$ in $F$ does not occur in $q$ (and $\Gamma$ coincides with $\Gamma^{\prime},p=q$).

By induction hypothesis we have a derivation ${\cal D}_{0}^{\prime}$ in $EQ^{1}_{1}$ of $\Gamma^{\prime},s=r\Rightarrow F^{\circ}\{u/p,v/s\}$. As ${\cal D}^{\prime}$ we can then take:

[TABLE]

Case 2. ${\cal D}$ is of the form:

[TABLE]

with $F\equiv F^{\circ}\{u/q\}$ and the unique occurrence of $v$ in $F$ occurs in $q$.

As ${\cal D}^{\prime}$ we can then take:

[TABLE]

Case 3. ${\cal D}$ is of the form:

[TABLE]

and $r\equiv r^{\circ}\{u/q\}$. By induction hypothesis we have a derivation ${\cal D}_{0}^{\prime}$ in $EQ^{1}_{1}$ of

$\Gamma^{\prime},s=r^{\circ}\{u/p\}\Rightarrow F\{v/s\}$. As ${\cal D}^{\prime}$ we can take:

[TABLE]

If ${\cal D}$ ends with a $=_{1}^{l}$-inference, then ${\cal D}$ has the form:

[TABLE]

By induction hypothesis we have a derivation ${\cal D}_{0}^{\prime}$ in $EQ_{1}^{1}$ of $\Gamma^{\prime},G\{u/p\},s=r\Rightarrow F\{v/s\}$. As ${\cal D}^{\prime}$ we can take:

[TABLE]

The proof of $b)$ is entirely similar.$\Box$

THEOREM 1.5

Cut elimination holds for $EQ_{1}$ and $EQ_{2}$.

Proof Any derivation ${\cal D}$ in $EQ_{1}$ can be transformed (by using the cut rule) into a derivation ${\cal D}^{\prime}$ in $EQ$ of the same end sequent. By the cut elimination theorem for $EQ$, ${\cal D}^{\prime}$ can be transformed into a cut-free derivation ${\cal D}"$ in $EQ$. Since $=_{2}$ is admissible in $cf.EQ_{1}$, the applications of the $=_{2}$-rule in ${\cal D}"$ can be replaced by applications of $=_{1}$ and $=_{1}^{l}$, thus obtaining the desired cut free derivation in $EQ_{1}$ of the end sequent of ${\cal D}$. Thanks to the admissibility in $EQ_{2}$ of $=_{1}$, the same argument shows that cut elimination holds for $EQ_{2}$ as well. $\Box$

Note Since $=_{2}^{l}$ is derivable in $EQ_{1}$, from the admissibility of the cut rule in $cf.EQ_{1}$ it follows that $=_{2}^{l}$ is also admissible in $cf.EQ_{1}$. Similarly also $=_{1}^{l}$ is admissible in $EQ_{2}$.

DEFINITION 1.7

For $i=1,2$, $LJ^{=}_{i}$ and $LK^{=}_{i}$ denote the systems obtained by adding $=_{i}$ and $=_{i}^{l}$ to $LJ$ and $LK$ respectively.

As an immediate consequence of Theorem 1.5, we have the following

THEOREM 1.6

Cut elimination holds for $LJ^{=}_{1}$, $LJ^{=}_{2}$, $LK^{=}_{1}$ and $LK^{=}_{2}$.

$EQ$, $EQ_{1}$ and $EQ_{2}$ are the only systems satisfying cut elimination that can be obtained by adding to the structural rules the Reflexivity Axiom and two equality rules chosen among $=_{1}$, $=_{2}$, $=_{1}^{l}$ and $=_{2}^{l}$.

For example

$a=c,b=c\Rightarrow a=b$ has the following cut-free derivations:

[TABLE]

but it has no cut-free derivation, if $a$, $b$ and $c$ are distinct and only the use of $=_{1}$ and $=_{2}^{l}$ is allowed. More generally no sequent of the form $~{}*)~{}\Gamma\Rightarrow a=b$, where the formulae in $\Gamma$ are among $c=c$, $a=c$ and $b=c$, can have a cut free derivation using only $=_{1}$ and $=_{2}^{l}$ . In fact, $*)$ is not the conclusion of a non trivial $=_{1}$-inference, since $c$ occurs in the right-hand side of all the possible operating equalities, so that it would occur in the succedent of the conclusion of any such inference. If it is the conclusion of a $=_{2}^{l}$-inference, with operating equality $a=c$, the transformed formula must be necessarily another occurrence of $a=c$, obtained by replacing with $a$ the first occurrence of $c$ in the changing formula $c=c$, to be found in the antecedent of the premiss. The same holds if the operating equality is $b=c$. Thus the premiss of the inference is still a sequent of the form $*)$. Obviously that is the case if $*)$ is the conclusion of a weakening, exchange or contraction. Hence if $*)$ is the conclusion of an inference different from a cut, then also the premiss of the inference has the form $*)$. Assuming that $a$, $b$ and $c$ are distinct, no axiom has the form $*)$. Thus there are no derivations of height zero of sequents of that form. Furthermore, by the above discussion, if there are no derivations of height $n$ of sequents of the form $*)$, then there are no derivations of height $n+1$ of sequents of that same form either. By induction on $n$ we conclude that there are no derivations at all of sequents of the form $*)$. In particular, if $a$, $b$ and $c$ are distinct, $a=c,b=c\Rightarrow a=b$ has no cut-free derivation using only $=_{1}$ and $=_{2}^{l}$ .

Similarly $c=b,c=a\Rightarrow a=b$ has the cut-free derivations:

[TABLE]

but it has no cut-free derivation, if $a$, $b$ and $c$ are distinct and only the use of $=_{2}$ and $=_{1}^{l}$ is allowed.

Finally $a=b\Rightarrow f(a)=f(b)$ has the cut-free derivations:

[TABLE]

but, if $a$ and $b$ are distinct, it has no cut-free derivation using only $=_{1}^{l}$ and $=_{2}^{l}$. In fact, if $a$ and $b$ are distinct, no sequent of the form $\Gamma\Rightarrow f(a)=f(b)$, where the formulae in $\Gamma$ are among $a=a$, $b=b$, $a=b$ and $b=a$, can have a cut free derivation using only $=_{1}^{l}$ and $=_{2}^{l}$.

Clearly that remains the case even if we add the left symmetry rule, that leads from $\Gamma,r=s\Rightarrow\Delta$, to $\Gamma,s=r\Rightarrow\Delta$. Concerning such a rule, we note also that it has the following cut-free derivation based on $=_{1}^{l}$, $=_{2}^{l}$ and the contraction rule:

[TABLE]

while it is not even admissible in the cut-free system with $=_{1}$ and $=_{2}^{l}$. For, otherwise, also $=_{1}^{l}$ would be admissible and then cut elimination would hold, which we have shown not to be the case. Similarly the left symmetry rule is not admissible in the cut free system with $=_{1}^{l}$ and $=_{2}$. On the contrary, since it is derivable in $EQ_{1}$, $EQ_{2}$ and $EQ$ (by means of the cut rule) as shown by the derivations:

[TABLE]

[TABLE]

it is admissible in the cut-free part of any of these systems (a fact that can also be easily proved directly by induction on the height of derivations). On the other hand the left symmetry rule is not derivable in any of $cf.EQ$, $cf.EQ_{1}$ and $cf.EQ_{2}$. For $cf.EQ$ that is obvious since $=_{1}$ and $=_{2}$ add formulae in the antecedent and modify only the formula in the succedent of a sequent. As for $cf.EQ_{1}$ ($cf.EQ_{2}$) it suffices to note that all the sequents in a derivation that starts with a sequent containing $a=b$ in the antecedent, must contain an equality of the form $a=t$ ($t=b$) in the antecedent. As a consequence, for example, there cannot be any derivation in $cf.EQ_{1}$ or $cf.EQ_{2}$ of $b=a\Rightarrow c=d$ from $a=b\Rightarrow c=d$, with $a,b,c$ and $d$ distinct.

Since any of the four equality rules is derivable from any other, from the above discussion concerning the failure of cut elimination, it follows that if only one of them is added to the logical and reflexivity axioms and the structural and logical rules, then the system that is obtained is adequate for first-order logic with equality, but it does not satisfy cut elimination. On the other hand if at least three of them are added, then cut elimination holds. More precisely we have established the following result.

THEOREM 1.7

Any extension of $LJ$ or $LK$ obtained by adding the Reflexivity Axiom $\Rightarrow=$ and some of the rules $=_{1},=_{2},=_{1}^{l}$ and $=_{2}^{l}$ is adequate for intuitionistic or classical first order logic with equality, but it satisfies the cut elimination theorem if and only if it contains (at least) either both $=_{1}$and $=_{2}$, or both $=_{1}$ and $=_{1}^{l}$ or both $=_{2}$ and $=_{2}^{l}$.

1.11 The Semishortening Property

Letting $LJ^{=}_{12}$ be the union of $LJ^{=}_{1}$ and $LJ^{=}_{2}$ and, similarly, $LK^{=}_{12}$ be the union of $LK^{=}_{1}$ and $LK^{=}_{2}$, by the previous Theorem, cut elimination holds for both $LJ^{=}_{12}$ and $LK^{=}_{12}$. On the ground of the exchange and contraction rules only, $LK^{=}_{12}$ is equivalent to the system $G^{e}$ in [5], which generalizes the rules $=_{1}$ and $=_{1}^{l}$ by permitting the substitution of $r$ by $s$ in more than one formula and merges them into a single rule of the form:

[TABLE]

and, similarly, generalizes and merges the rules $=_{2}$ and $=_{2}^{l}$ into:

[TABLE]

Thus, as an immediate consequence of Theorem 1.7, cut elimination holds for $G^{e}$. Actually [5] deals only with cut-free derivations in $G^{e}$ and shows that they can be transformed into cut-free derivations that do not contain terms that are longer than those occurring in the end-sequent, under various notion of length of a term. Clearly a cut-free derivation may contain terms longer than those occurring in the endsequent only if it contains some equality inference that is lengthening in the sense that the term $r$ in the premiss is longer that the term $s$ by which it is replaced in the conclusion of the inference. If we let $s\prec r$ to mean that $r$ is longer that $s$, the result in [5] applies to all the binary relation $\prec$ on terms that are strict partial orders congruent with respect to substitution, namely $r\prec s$ entails $t\{v/r\}\prec t\{v/s\}$, for any term $r$, $s$ and $t$. [8] states that it suffices to require that $\prec$ be antireflexive. We will base our definitions on such a weaker requirement and prove a stronger result, namely that any derivation in $LJ^{=}_{12}$ or $LK^{=}_{12}$ can be transformed into one whose equality inferences are all non lengthnening, while those of the form $=_{1}$ and $=_{1}^{l}$, or, alternatively, those of the form $=_{2}$ and $=_{2}^{l}$, are actually shortening, namely satisfy the stronger condition $r\prec s$. It will suffice to deal with the former case, since the latter is completely symmetric. In the following $\prec$ will be a fixed, but arbitrary binary antireflexive relation on terms, namely for any term $r$ and $s$, $r\prec s$ entails $s\not\prec r$.

DEFINITION 1.8

An application of an $=_{1}$-inference or of an $=_{1}^{l}$-inference with operating equality $r=s$ (or of an application of an $=_{2}$-inference or of an $=_{2}^{l}$-inference with operating equality $s=r$) is said nonlengthening if $s\not\prec r$ and shortening if $r\prec s$. A derivation is said to be nonlengthening if all its equality inferences are nonlengthening and semishortening if it is nonlengthening and, furthermore, all its $=_{1}$ and $=_{1}^{l}$-inferences are shortening.

PROPOSITION 1.14

The equality rules $=_{1}$ and $=_{2}$ are admissible in $cf.EQ_{12}$ restricted to semishortening derivations. More precisely, there are two effective operations ${\cal G}_{1}$ and ${\cal G}_{2}$ such that:

• a)

if ${\cal D}$ is a semishortening derivation in $cf.EQ_{12}$ of $\Gamma\Rightarrow F\{v/r\}$, then for any term $s$, ${\cal G}_{1}({\cal D},r,s)$ is a semishortening derivation in $cf.EQ_{12}$ of

$\Gamma,r=s\Rightarrow F\{v/s\}$* and*

• b)

if ${\cal D}$ is a semishortening derivation in $cf.EQ_{12}$ of $\Gamma\Rightarrow F\{v/r\}$, then for any term $s$, ${\cal G}_{2}({\cal D},r,s)$ is a semishortening derivation in $cf.EQ_{12}$ of

$\Gamma,s=r\Rightarrow F\{v/s\}$.

Proof To be more accurate, ${\cal G}_{1}$ and ${\cal G}_{2}$ actually have four arguments, i.e. ${\cal D}$, $F$, $\{v/r\}$ and $s$ and their definition requires that $F\{v/r\}$ coincides with the succedent of the endsequent of ${\cal D}$. However, since it will be clear from the context what $F$ and $\{v/r\}$ are, there is no harm in using the simplified notations ${\cal G}_{1}({\cal D},r,s)$ and ${\cal G}_{2}({\cal D},r,s)$.

By Lemma 1.2, it suffices to deal with derivations in $cf.EQ_{12}^{1}$. If $r\prec s$ then ${\cal G}_{1}({\cal D},r,s)$ is obtained by applying to ${\cal D}$ an $=_{1}$-inference with operating equality $r=s$ and if $s\not\prec r$ (in particular if $r\prec s$), ${\cal G}_{2}({\cal D},r,s)$ is obtained by applying to ${\cal D}$ an $=_{2}$ inference, with operating equality $s=r$. Hence in defining ${\cal G}_{1}$ we may assume that $r\not\prec s$, while in defining ${\cal G}_{2}$ we may assume that $s\prec r$.

${\cal G}_{1}({\cal D},r,s)$ and ${\cal G}_{2}({\cal D},r,s)$ are defined simultaneously by recursion on the height $h({\cal D})$ of ${\cal D}$, for arbitrary $s$.

If $h({\cal D})=0$ we have the following cases.

Case 0.1 ${\cal D}$ reduces to $F\{v/r\}\Rightarrow F\{v/r\}$. As ${\cal G}_{1}({\cal D},r,s)$ we can take

[TABLE]

which is nonlengthening, since we are assuming that $r\not\prec s$, and as ${\cal G}_{2}({\cal D},r,s)$ we can take:

[TABLE]

which is shortening, since we are assuming that $s\prec r$. Thus in both cases we have obtained a semishortening derivation, as required.

Case 0.2 ${\cal D}$ reduces to $~{}~{}\Rightarrow t_{0}=t\{v/r\}$ with $t_{0}\equiv t\{v/r\}$. As ${\cal G}_{1}({\cal D},r,s)$ we can take:

[TABLE]

which is nonlengthening, and as ${\cal G}_{2}({\cal D},r,s)$ we can take:

[TABLE]

which is shortening.

Case 0.3 ${\cal D}$ reduces to $~{}~{}\Rightarrow t\{v/r\}=t_{0}$ with $t_{0}\equiv t\{v/r\}$. The definition of ${\cal G}_{1}({\cal D},r,s)$ and ${\cal G}_{2}({\cal D},r,s)$ is essentially the same as in case 0.2.

If $h({\cal D})>0$ and ${\cal D}$ ends with a structural rule and has the form:

[TABLE]

${\cal G}_{1}({\cal D},r,s)$ and ${\cal G}_{2}({\cal D},r,s)$ are obtained by applying the same structural rule and some exchanges to the endsequent of ${\cal G}_{1}({\cal D}_{0},s)$ and ${\cal G}_{2}({\cal D}_{0},s)$ that, by induction hypothesis, are semishortening derivations in $cf.EQ_{12}^{1}$ of $\Gamma^{\prime},r=s\Rightarrow F\{v/s\}$ and $\Gamma^{\prime},s=r\Rightarrow F\{v/s\}$ respectively.

Otherwise we have the following four cases depending on the ending equality inference of ${\cal D}$.

Case 1. ${\cal D}$ ends with an $=_{1}$-inference. Then we have the following three subcases:

Case 1.1. ${\cal D}$ has the form:

[TABLE]

with $F\equiv F^{\circ}\{u/q\}$ and $v$ does not occurs in $q$. Since ${\cal D}$ is semishortening, $p\prec q$. By induction hypothesis ${\cal G}_{1}({\cal D}_{0},r,s)$ is a semishortening derivation of $\Gamma^{\prime},r=s\Rightarrow F\{u/p,v/s\}$ and we can let ${\cal G}_{1}({\cal D},r,s)$ be:

[TABLE]

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that ${\cal G}_{1}({\cal D}_{0},r,s)$ and $r=s$ in the endsequent are replaced by ${\cal G}_{2}({\cal D}_{0},r,s)$ and $s=r$ respectively.

Case 1.2 ${\cal D}$ has the form:

[TABLE]

with $F\equiv F^{\circ}\{u/q\}$ and $v$ occurs in $q$. By induction hypothesis there is a semishorthening derivation ${\cal G}_{1}({\cal D}_{0},p,q\{v/s\})$ of $\Gamma^{\prime},p=q\{v/s\}\Rightarrow F^{\circ}\{u/q\{v/s\}\}$ and we can let ${\cal G}_{1}({\cal D},r,s)$ be:

[TABLE]

which is semishortening, since its ending $=_{2}^{l}$-inference is nonlengthening, given that in defining ${\cal G}_{1}$, we are assuming that $r\not\prec s$.

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that $=_{2}^{l}$ and $r=s$ in the endsequent are replaced by $=_{1}^{l}$ and $s=r$ respectively. In fact the ending $=_{1}^{l}$-inference of the derivation so obtained is shortening since, in defining ${\cal G}_{2}$, we are assuming that $s\prec r$. Notice that in this case the definition of ${\cal G}_{2}({\cal D},r,s)$ depends on ${\cal G}_{1}({\cal D}_{0},p,q\{v/s\})$.

Case 1.3 $r$ has the form $r^{\circ}\{u/q\}$ and ${\cal D}$ the form:

[TABLE]

with $p\prec q$. By induction hypothesis there is a semishortening derivation ${\cal G}_{1}({\cal D}_{0},r^{\circ}\{u/p\},s)$ of $\Gamma^{\prime},r^{\circ}\{u/p\}=s\Rightarrow F\{v/s\}$ and we can let ${\cal G}_{1}({\cal D},s)$ be:

[TABLE]

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that ${\cal G}_{1}({\cal D}_{0},r^{\circ}\{u/p\},s)$, $r^{\circ}\{u/p\}=s$ and $r^{\circ}\{u/q\}=s$ are replaced by ${\cal G}_{2}({\cal D}_{0},r^{\circ}\{u/p\},s)$, $s=r^{\circ}\{u/p\}$ and $s=r^{\circ}\{u/q\}$ respectively.

Case 2 ${\cal D}$ ends with an $=_{2}$ inference.

Case 2.1 ${\cal D}$ has the form:

[TABLE]

with $F\equiv F^{\circ}\{u/q\}$ and $v$ does not occur in $q$. Since ${\cal D}$ is semishortening, $q\not\prec p$. By induction hypothesis we have a semishortening derivation ${\cal G}_{1}({\cal D}_{0},r,s)$ of $\Gamma^{\prime},r=s\Rightarrow F^{\circ}\{u/p,v/s\}$ and as ${\cal G}_{1}({\cal D},r,s)$ we can take:

[TABLE]

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that ${\cal G}_{1}({\cal D}_{0},r,s)$ and $r=s$ in the endsequent are replaced by ${\cal G}_{2}({\cal D}_{0},r,s)$ and $s=r$ respectively.

Case 2.2 ${\cal D}$ has the form:

[TABLE]

with $F\equiv F^{\circ}\{u/q\}$ and $v$ occurs in $q$. By induction hypothesis there is a semishortening derivation ${\cal G}_{2}({\cal D}_{0},p,q\{v/s\})$ of $\Gamma^{\prime},q\{v/s\}=p\Rightarrow F^{\circ}\{u/q\{v/s\}\}$ and we can let ${\cal G}_{1}({\cal D},r,s)$ be:

[TABLE]

which is semishortening, since its ending $=_{2}^{l}$-inference is nonlengthening, given that in defining ${\cal G}_{1}$, we are assuming that $r\not\prec s$. Notice that in this case the definition of ${\cal G}_{1}({\cal D},r,s)$ depends on ${\cal G}_{2}({\cal D}_{0},p,q\{v/s\})$.

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that $=_{2}^{l}$ and $r=s$ in the endsequent are replaced by $=_{1}^{l}$ and $s=r$ respectively .

Case 2.3 $r$ has the form $r^{\circ}\{u/q\}$ and ${\cal D}$ the form:

[TABLE]

with $q\not\prec p$. By induction hypothesis, ${\cal G}_{1}({\cal D}_{0},r^{\circ}\{u/p\},s)$ is a semishorthening derivation of $\Gamma^{\prime},r^{\circ}\{u/p\}=s\Rightarrow F\{v/s\}$ and we can let ${\cal G}_{1}({\cal D},r,s)$ be:

[TABLE]

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that ${\cal G}_{1}({\cal D}_{0},r^{\circ}\{u/p\},s)$ and $r^{\circ}\{u/q\}=s$ are replaced by ${\cal G}_{2}({\cal D}_{0},r^{\circ}\{u/p\},s)$ and $s=r^{\circ}\{u/q\}$ respectively.

Case $1^{l}$ ${\cal D}$ ends with an $=_{1}^{l}$-inference, i.e. it has the form:

[TABLE]

with $p\prec q$. By induction hypothesis ${\cal G}_{1}({\cal D}_{0},r,s)$ is a semishortening derivation of $\Gamma^{\prime},G\{u/p\},r=s\Rightarrow F\{v/s\}$ and we can let ${\cal G}_{1}({\cal D},r,s)$ be:

[TABLE]

The definition of ${\cal G}_{2}({\cal D},r,s)$ is the same, except that ${\cal G}_{1}({\cal D}_{0},r,s)$ and $r=s$ in the endsequent are replaced by ${\cal G}_{2}({\cal D}_{0},r,s)$ and $s=r$ respectively.

Case $2^{l}$ ${\cal D}$ ends with a $=_{2}^{l}$-inference, namely $p=q$ is replaced by $q=p$ in the endsequent of ${\cal D}$ as represented in Case $1^{l}$. Then ${\cal G}_{1}({\cal D},r,s)$ and ${\cal G}_{2}({\cal D},r,s)$ are defined as in Case $1^{l}$, except that $p=q$ is replaced by $q=p$. $\Box$

THEOREM 1.8

Any derivation in $EQ_{12}$ can be tranformed into a cut-free semishortening derivation in $EQ_{12}$ of its endsequent.

Proof Every derivation in $EQ_{12}$ can be effectively transformed into a derivation in $EQ$, henceforth, by Theorem 1.2, into a cut free derivation in $EQ$ of its endsequent. The conclusion follows by the admissibility of the equality rules $=_{1}$ and $=_{2}$ in $cfEQ_{12}$ restricted to semishortening derivations, established in the previous Proposition 1.14. $\Box$

COROLLARY 1.1

Any derivation in $LJ_{12}$ or $LK_{12}$ can be tranformed into a cut-free semishortening derivation in the same calculus of its endsequent.

Remark Since the semishortening derivations are nonlengthening, an immediate consequence of Theorem 1.8 is that every derivation in $EQ_{12}$ can be transformed into a cut-free nonlengthening derivation of its endsequent. That can also be established by observing that if semishortening is replaced by nonlengthening, then Proposition 1.14 still hold with essentially the same proof.

Remark Since $=_{1}^{l}$ and $=_{2}^{l}$ are derivable in $EQ$, from the admissibility of the cut rule in $cf.EQ$, it follows that $=_{1}^{l}$ and $=_{2}^{l}$ are admissible in $cf.EQ$. Hence from Proposition 1.14 it follows that also $=_{1}^{l}$ and $=_{2}^{l}$ are admissibile in $cf.EQ_{12}$ restricted to semishortening derivations. As it results from [5], in the case of nonlengthening derivations, a direct inductive proof of this admissibility result is possible, but it requires the additional assumption that $\prec$ be a strict partial order congruent with respect to substitution. It is the admissibility of $=_{1}^{l}$ and $=_{2}^{l}$ in $cf.EQ$, unnoticed in [5], that allows for the weakening of such assumption to the requirement that $\prec$ be simply antisymmetric.

1.12 Related work

Beside the references already given in the introduction, we add that the restriction $=_{0}\Rightarrow$ of the rule $=\Rightarrow$ to atomic $F$ had been considered in [6] in conjunction with the following left reflexivity elimination rule:

[TABLE]

in the framework of $LJ$ and $LK$. We point out that for the resulting systems, cut elimination is a trivial matter as any formula $H$ can be seen (in many ways) as $H^{\circ}\{v/t\}$, so that the cut rule can be derived from $=\Rightarrow$ and the left reflexivity elimination rule, as follows:

[TABLE]

Despite the fact that the left reflexivity elimination rule eliminates equalities, [6] uses such systems to prove the conservativity of first order logic with equality over first order logic without equality. A calculus similar to $LK_{N}^{=}$, but without $\vee$ and $\exists$ and with $CNG$ restricted from the start to atomic formulae is considered in [14], which establishes the eliminabilty of the cut rule without going through the reduction of derivation to separated form. The idea of using the admissibility of the rule $CNG$ in $EQ_{N}$ to prove Theorem 1.3 first appeared in [13]. However the proof of admissibility and the way of deriving the cut elimination theorem for the $LJ^{=}$ and $LK^{=}$ systems given in this paper are a substantial improvement of those to be found in [13].