PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 86(100) (2009), 27–34 DOI: 10.2298/PIM0900027B

NORMALIZATION AS A CONSEQUENCE OF CUT ELIMINATION

Mirjana Borisavljević

Communicated by Žarko Mijajlović

Abstract. Pairs of systems, which consist of a system of sequents and a natural deduction system for some part of intuitionistic logic, are considered. For each of these pairs of systems the property that the normalization theorem is a consequence of the cut-elimination theorem is presented.

1. Introduction

In [3] Gentzen introduced the system of sequents and the natural deduction system for intuitionistic logic (the systems LJ and NJ) and classical logic (the systems LK and NK). The main theorem of the systems of sequents is the cut-elimination theorem, and in the natural deduction systems the normalization theorem is the central one. In the systems of sequents cut-free derivations, i.e., derivations without cuts, are the most important derivations, and the most important natural deduction derivations are normal derivations, i.e., derivations without maximum formulae and maximum segments.

Transformations of derivations and mapping which connect derivations from the systems of sequents and natural deduction systems were introduced in [3] and [8] (see the Introduction in [11] for details). In the papers [2, 3, 5, 7, 8, 11] a system of sequents and a natural deduction system for some fragments of intuitionistic logic were considered. In each of these papers the similarities and differences between the system of sequents and the natural deduction system were presented. One of the main goals of almost all the papers mentioned above was to study the connection between the cut-free derivations and the normal derivations. There are two levels of that connection. The first level is the connection between these derivations. The second level is the correspondence between the cut-elimination procedure in systems of sequents and the normalization procedure in natural deduction systems.

If we want to present a connection between the cut-elimination procedure in a system of sequents and the normalization procedure in a natural deduction system for intuitionistic logic, then that connection should have some of the following characteristics:

2000 Mathematics Subject Classification: Primary 03F05.

Key words and phrases: cut elimination, normalization.

(1) the system of sequents and the natural deduction system almost coincide with Gentzen’s systems LJ and NJ, respectively;

(2) the set of reductions of the cut-elimination procedure (i.e., a set of transformations of sequent derivations) contains transformations of sequent derivations which are necessary in that procedure, and these transformations are standard transformations from the well-known proofs of cut-elimination or mix-elimination theorems (see for example [3]);

(3) the set of reductions of the normalization procedure contains transformations of natural deduction derivations which are necessary in that procedure, and these transformations are standard transformations from the well-known proofs of normalization theorems (see for example [8]);

(4) these sets of reductions of both procedures contain other possible transformations of derivations.

The problems of the connection between reductions which constitute cut-elimi-nation and normalization procedures are well known (see the Introduction in [11] and Subsection 2.3 below). In [1], [2], [7] and [11] different pairs of systems of sequents and natural deduction systems were considered, and their cut-elimination and normalization procedures were connected. The natural deduction systems from [2], [7] and [11] have the following property: its normalization theorem is a consequence of the cut-elimination theorem of the corresponding system of sequents. In this paper we show that the natural deduction system from [1] has the same property.

In Sections 2 and 3 we briefly present the results from [2], [7] and [11] and their characteristics. In Section 4 we consider the system of sequents and the natural deduction system from [1], the systems SE and N E, and we show that the normalization theorem of the system N E is a consequence of the cut-elimination theorem of the system SE.

2. Connections between standard reductions of cut elimination and standard reductions of normalization

In [11] Zucker defined a system of sequents, the system S, and a natural deduction system, the system N, which cover full intuitionistic predicate logic, and which are very similar to Gentzen’s systems LJ and NJ, respectively. He also defined the map φ which connects derivations from S and N. Zucker’s conversions of derivations in the system S (which make the set of reductions of the cut-elimination procedure) and conversions of derivations in the system N (which make the set of reductions of the normalization procedure) are standard. Moreover, the set of reductions in the system S contains all possible conversions of derivations in the system S.

2.1. The systems S and N. Now we present only Zucker’s system S. (His system N is a standard natural deduction system, i.e., Gentzen’s system NJ with explicit contraction (see Section 2.3 in [11] for details).)

A sequent of the system S has the form Γ → A, where Γ is a finite set of indexed formulae and A is one unindexed formula. We only repeat the following about indices of formulae from [11] (for all other definitions see [11]): a finite nonempty sequence of natural numbers will be called a symbol, and will be denoted by σ, τ, …; a finite non-empty set of symbols will be called an index, and will be denoted by α, β, … There are two operations on indices: the union of two indices α and β, α ∪ β, is again an index and it is simply a set-theoretical union; and the product of α and β is α × β =_{df} {σ ∗ τ : σ ∈ α, τ ∈ β}, where ∗ is the concatenation of sequences.

Postulates for the system S.

Logical initial sequents: A_{i} → A. ⊥-initial sequents: ⊥_{i}→ P, where P is any atomic formula different from ⊥. Inference rules

structural rules

(contraction ) \frac{A_{α} , A_{β} , Γ → C}{A_{α∪β} , Γ → C}

(cut) \frac{Γ → A A_{α} , Δ → C}{Γ_{×α} , Δ → C}

logical rules (i.e., operational rules)

left rules  right rules
(⊃L) \frac{Γ → A  B_{β} , Δ → C}{Γ_{×β} , A ⊃ B_{β} , Δ → C}  (⊃R) \frac{(A_{α} ), Γ → B}{Γ → A ⊃ B}
(∧L_{1}) \frac{A_{α} , Γ → C}{A ∧ B_{α} , Γ → C}  (∧L_{2}) \frac{B_{α} , Γ → C}{A ∧ B _{α} , Γ → C}  (∧R) \frac{Γ → A  Δ → B}{Γ, Δ → A ∧ B}
(∨L) \frac{(A_{α} ), Γ → C  (B_{β}), Δ → C}{A ∨ B_{i}, Γ, Δ → C}  (∨R_{1}) \frac{Γ → A}{Γ → A ∨ B}  (∨R_{2}) \frac{Γ → B}{Γ → A ∨ B}
(∀L) \frac{F t_{α} , Γ → C}{∀xF x_{α} , Γ → C}  (∀R) \frac{Γ → F a}{Γ → ∀xF x}
(∃L) \frac{(F a_{α} ), Γ → C}{∃xF x_{i}, Γ → C}  (∃R) \frac{Γ → F t}{Γ → ∃xF x}

In the rules (∀R) and (∃L) the variable a has to satisfy the well-known restrictions on variables (see 2.3.8.(b) in [11]).

2.2. The connection between the systems S^{−} and N^{−} . In [11] Zucker presented standard reductions of the cut-elimination procedure in the system S and standard reductions of the normalization procedure in the system N. He solved the problem of the connection between reductions of the cut-elimination procedure in the system S^{−} and reductions of the normalization procedure in the system N^{−} , where the systems S^{−} and N^{−} are the parts of the systems S and N which cover (∧, ⊃, ∀, ⊥)-fragment of intuitionistic logic. By using that connection Zucker showed the following (see Theorem 3(a) from 6.8.2 in [11]):

The normalization theorem in the system N^{−} is a consequence of the cutelimination theorem in the system S^{−} .

2.3. The problems of connections between standard reductions of cut elimination and standard reductions of normalization. In [11] Zucker presented difficulties of the connection between the usual reductions in the full systems S and N, i.e., the problems with ∨ and ∃ (see the part 7 in [11]). When a derivation D in the system S has the following form

\frac{{D_{1} \atop Γ → A} {D_{2} \atop A_{α} , Δ → C}}{Γ_{×α} , Δ → C} cut

where the last rule of derivation D_{1} is a left rule r_{1} and the last rule of the derivation D_{2} is a left rule r_{2} which makes the cut formula A_{α}, then there is a very natural conversion in the system S:

(c*)  the rule r_{1}, i.e., the last rule of D_{1}, permutes with the cut,

and a new derivation C is obtained. So,

(*)  the derivation D is transformed into the derivation C

and (*) can be a reduction of the cut-elimination procedure in the system S.

However, Zucker showed that the image of such reduction from the system S does not have the corresponding reduction in the natural deduction system N. In fact, there are three cases.

(i) If r_{1} is a left rule which introduces ∧, ⊃ or ∀ and r_{2} is an arbitrary left rule which makes A_{α}, then the derivations D and C have the same images in the natural deduction system N, (i.e., in the system N one derivation corresponds to both derivations D and C).

(ii) If r_{1} is a left rule which introduces ∨ or ∃ and r_{2} is a left rule which also introduces ∨ or ∃ (i.e., the main sign of the formula A_{α} is ∨ or ∃), then the naturaldeduction images of D and C are connected by a reduction for maximum segments of the normalization procedure in the system N. Thus, in this case the reduction (*) of the cut-elimination procedure in the system S has the corresponding reduction of the normalization procedure in the system N. Finally,

(iii) if r_{1} is a left rule which introduces ∨ or ∃ and r_{2} is a left rule which introduces ∧, ⊃ or ∀ (i.e., the main sign of the formula A_{α} is ∧, ⊃ or ∀), then in the system N there is not any reduction which corresponds to (*). Namely, the natural-deduction images of D and C from (*) are different derivations in the system N, but they are not connected by any reduction in the system N. More precisely, in the system N the image of D is the derivation with the maximum segment which consists of images of the cut formula A of the cut (i.e., the last rule of D), and the image of the derivation C is not the contractum of the reduction which is applied to that maximum segment of the image of the derivation D.

3. Connections between new reductions of cut elimination and standard reductions of normalization

To solve the problem from the case (iii) in 2.3 we can change reductions of cut elimination or reductions of normalization. In this section we briefly present two solutions of that problem in which reductions of cut elimination are changed.

3.1. The connection between Pottinger’s systems H_{λL} and H_{λ}. Zucker suggested (see the part 7.8.2(b) in [11]) the new reductions (i.e., conversions) for derivations in the case (iii) above, and he called these conversions “less natural”. By using these suggestions Pottinger (in [7]) connected the cut-elimination procedure in his system of sequents H_{λL} and the normalization procedure in his natural deduction system H_{λ} for intuitionistic propositional logic. The important characteristics of Pottinger’s work are that his connection does not have characteristics (1), (2) and (4) above. His systems are some kinds of λ-calculi (then they cover only propositional part of intuitionistic logic) and his system of sequents does not have contraction as an explicit rule. The set of reductions of the cut-elimination procedure in his system of sequents contains some not standard reductions i.e., Zucker’s “less natural” reductions. By using the connection between the cut-elimination procedure in H_{λL} and the normalization procedure in H_{λ} Pottinger showed the following (see Corollary 8.3 in [7]):

The normalization theorem in the system H_{λ} is a consequence of the cutelimination theorem in the system H_{λL} .

3.2. The connection between the systems S and N. In [2] Zucker’s systems for intuitionistic predicate logic from [11], the system of sequents (the system S) and the natural deduction system (the system N), were considered. The map which connects derivations from S and N was also Zucker’s map φ from [11]. The set of conversions (i.e., reductions) of derivations in the system N consists of well-known standard reductions from normalization procedures. However, the set of conversions (i.e., reductions) of derivations in the system S consists of wellknown standard reductions from mix-elimination and cut-elimination procedures, and modifications of some Zucker’s “less natural” conversions from [11]. In [2] the sets of conversions in the systems S and N and the map φ have the following characteristics:

(I) in the system S its conversions for derivations are sufficient for transforming a derivation into a cut-free one (Cut-Elimination Theorem from Section 3.2 in [2]);

(II) in the natural deduction system N the image of each conversion from the set of conversions for the cut-elimination procedure will be either a pair of equal derivations (Theorem 1 from Section 4.1 in [2]), or several conversions from the set of conversions for the normalization procedure (Theorem 2 from Section 4.2 in [2]);

(III) the map φ from the set of derivations of S into the set of derivations of N is onto (2.4.4. Proposition in [11]);

(IV) if a derivation D is a cut-free derivation in the system S, then the derivation φD is a normal derivation in the system N (Theorem 4 from Section 4.3 in [2]).

Thus, in [2] a connection between reductions of the cut-elimination procedure in the full system S and reductions of the normalization procedure in the full system N was made. Moreover, the connection from [2] has the characteristics (1) and (3) above. Zucker’s conversions, which are conversions (*) from the case (iii) above (and which make the problematical sequence of reductions in the full system S from his example in Section 7 of [11]) do not belong to the set of reductions of the cutelimination procedure in [2]. So, in that cut-elimination procedure the problem, which was presented in the case (iii), does not exist.

Finally, in [2] the normalization theorem in the full system N was proved by using the properties (I), (II), (III) and (IV) above (see Section 4.4 in [2]). So, we have the following:

The normalization theorem in the system N is a consequence of the cut-elimina-tion theorem in the system S.

4. Connections between standard reductions of cut elimination and new reductions of normalization

In [1] a new solution of the problem with the conversion (c*) was presented. That solution is not to change (c*), but to define a new natural deduction system, the system N E, whose normalization procedure has the reductions corresponding to the reductions (*) from the system S for each left rule r_{1} and each left rule r_{2} which makes A_{α}. In [1] the system of sequents is the system SE, which is Zucker’s system S with upper indices (see Section 2.1 from [1] for details), and the natural deduction system is the system N E.

4.1. The natural deduction system N E. We present the system N E from [1]. Postulates in the system N E (see Section 2.3 from [1] for details).

Trivial derivation of A from A itself, A or A^{i}, where i is any unary index.

Substitution. From {Δ \atop π_{1}} ; A and {Γ, A^{a} \atop π_{2}} ; C we define a derivation {Γ, {Δ^{×a} \atop π_{1}} ; (A^{a}) \atop π_{2}} ; C. .

Contraction: From {Γ, A^{a}, A^{b} \atop π} ; C we make {Γ, A^{a} ^{∗}, A^{b}^{∗} \atop π} ; C , where ∗ means that A^{a} and A^{b} are contracted. Logical inference rules introduction rules elimination rules

{[A^{a}] \atop π} ; B ; A ⊃ B (⊃IE)  \begin{aligned}{π_{1} \atop A ⊃ B} & {π_{2} \atop A} & {[B^{b}] \atop π_{3}} ; C \\ & C \end{aligned}(⊃EE)

\begin{matrix}A & B \\ A ∧ B \end{matrix} (∧IE)  \begin{aligned}{π_{1} \atop A ∧ B} & & {[A^{a}] \atop π_{2}} ; C \\ & C \end{aligned}(∧EE_{1})  \begin{aligned}{π_{1} \atop A ∧ B} & & {[B^{b}] \atop π_{2}} ; C \\ & C \end{aligned}(∧EE_{2})

{A \atop A ∨ B} (∨IE_{1})  {B \atop A ∨ B} (∨IE_{2})  \begin{aligned}{π_{1} \atop A ∨ B} & {[A^{a}] \atop π_{2}} ; C & {[B^{b}] \atop π_{3}} ; C \\ & C \end{aligned}(∨EE)

{F a \atop ∀xF x} (∀IE)  \begin{aligned}{π_{1} \atop ∀xF x} & & {[F t^{a}] \atop π_{2}} ; C \\ & C \end{aligned} ; (∀EE)

{F t \atop ∃xF x} (∃IE)  \begin{aligned}{π_{1} \atop ∃xF x} & & {[F a^{c}] \atop π_{2}} ; C \\ & C \end{aligned} ; (∃EE)

⊥−rule

{⊥ \atop P} (⊥) , P is an atomic formula different from ⊥.

In the rules (∀IE) and (∃EE) the variable a has to satisfy the well-known restrictions on variables. In each of the rules (⊃IE), (⊃EE), (∧EE_{1}), (∧EE_{2}), (∨EE), (∀EE) and (∃EE) in the brackets [ ] there is the assumption class which is discharged by that rule.

The most important characteristic of the system N E is that elimination rules for all connectives and quantifiers are of the same form as the elimination rule of ∨ and ∃ in natural deduction, so all elimination rules make maximum segments. With regard to introduction rules of the system N E, they are standard introduction rules from natural deduction. (The system N E is similar to the systems from [6] and [10].)

4.2. The connection between the systems SE and N E. The map ψ by which each derivation from the system SE is connected with a derivation in the system N E was defined (see Section 4 from [1] for details). In the system SE the set of conversions (i.e., reductions) consists of the reductions (*) for the rules r_{1} and r_{2} mentioned above and other standard reductions from the well-known cutelimination theorems. In the system N E the set of conversions (i.e., reductions) consists of the standard reductions from the well-known normalization theorems and new reductions for the elimination of maximum segments which are made by the elimination rules of ∧, ⊃ or ∀. Now we present one such new reduction, when the elimination rule of ∧ makes a maximum segment. (All other reductions are presented in Section 5.3 in [1].)

The redex π and the contractum \overline{π} are

\begin{matrix}\begin{aligned}{Γ \atop π_{1}} ; A ∧ B & {[A^{a}], Δ \atop π_{2}} ; C ∧ D \\ & C ∧ D \end{aligned}  ∧EE_{1} & {[D^{d}], Λ \atop π_{3}} ; G \\ G \end{matrix} ; ∧EE_{2} and \begin{aligned}{Γ \atop π_{1}} ; A ∧ B & \begin{aligned}{[A^{a}], Δ \atop π_{2}} ; C ∧ D & & {[D^{d}], Λ \atop π_{3}} ; G \\ & G \end{aligned} ; ∧EE_{2} \\ & G \end{aligned} ; ∧EE_{1}

where in the derivation π the formulae C ∧ D belong to a maximum segment (see Section 5.3 in [1] for details).

In the systems SE and N E the sets of conversions have the following characteristics:

(I_{E}) in the system SE its conversions for derivations are sufficient for transforming a derivation into a cut-free one (the proof of this is the standard proof of a cut-elimination theorem (see Note 5.3 in Section 5.1 in [1]));

(II_{E}) in the natural deduction system N E the image of each conversion from the set of conversions of the cut-elimination procedure from SE is either a pair of equal derivations (Theorem 6.1 from Section 6 in [1]), or a member of the set of conversions for the normalization procedure (Theorem 6.2 and Theorem 6.3 from Section 6 in [1]);

(III_{E}) the map ψ from the set of derivations of SE into the set of derivations of N E is onto (the proof of this is very similar to the proof of 2.4.4. Proposition in [11]);

(IV_{E}) if a derivation D is a cut-free derivation in the system SE, then the derivation ψD is a normal derivation in the system N E (Corollary 6.5 from Section 6 in [1]).

The normalization theorem in the system N E has the following form.

Theorem 4.1. In the system N E each derivation π can be reduced to a normal derivation.

The proof of the normalization theorem in the system N E is very similar to the proof of the normalization theorem in the system N from Section 4.4 in [2]. In the system N E we consider a derivation π. By (III_{E}), the derivation π is the ψ-image of a derivation D from the system SE, i.e., π = ψD. By (I_{E}), the derivation D can be reduced to a cut-free derivation F. By (II_{E}), for each reduction from the sequence of reductions from D to F we have that the ψ-images of its redex and contractum are either the same derivations or they are connected by a reduction in the system N E. It means that these reductions make a reduction sequence from π = ψD to ψF in the system N E, where (by (IV_{E})) the derivation ψF is a normal derivation in the system N E. Thus, the derivation π is reduced to a normal derivation, the derivation ψF.

So, the system of sequents SE and the natural deduction system N E have the same property as the pairs of systems from [2], [7] and [11]:

The normalization theorem in the system N E is a consequence of the cutelimination theorem in the system SE.

References

[1] M. Borisavljević, Extended Natural Deduction Images of Conversions from the Systems of Sequents, J. Logic Comput. 14/6 (2004), 769–799.

[2] M. Borisavljević, A connection between cut elimination and normalization, Archive Math. Logic 45 (2006), 113–148.

[3] G. Gentzen, Untersuchungen über das logische Schließen, Math. Zeitschrift 39 (1935) 176– 210, 405–431 (English translation in [Gentzen 1969]).

[4] G. Gentzen, The Collected Papers of Gerhard Gentzen, M. E. Szabo (ed.), North-Holland, 1969

[5] G. E. Minc, Normal forms for sequent derivations; in: P. Odifreddi (ed.) Kreiseliana: About and Around Georg Kreisel, Peters, 1996, 469–492.

[6] J. von Plato, Natural deduction with general elimination rules, Arch. Math. Logic 40/1 (2001), 541–567.

[7] G. Pottinger, Normalization as a homomorphic image of cut elimination, Ann. Pure Appl. Logic 12 (1977), 323–357.

[8] D. Prawitz, Natural Deduction, Almquist and Wiksell, Stockholm, 1965

[9] D. Prawitz, Ideas and results in proof theory; in: J. E. Fenstad, (ed.) Proc. of the Second Scandinavian Logic Symposium, Norht-Holland, 1971, 235–307.

[10] P. Schroeder-Heister, A natural extension of natural deduction, J. Symbolic Logic 49/4 (1984), 1284–1300.

[11] J. Zucker, The correspondence between cut-elimination and normalization, Ann. Math. Logic 7 (1974), 1–112.

Faculty of Transport and Traffic Engineering (Received 27 10 2008) University of Belgrade Vojvode Stepe 305, 11000 Belgrade Serbia

mirjanab@afrodita.rcub.bg.ac.rs