PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 87(101) (2010), 59–74 DOI: 10.2298/PIM1001059B

MAXIMUM CUTS IN EXTENDED NATURAL DEDUCTION

Mirjana Borisavljević

Communicated by Žarko Mijajlović

Abstract. We consider a standard system of sequents and a system of extended natural deduction (which is a modification of natural deduction) for intuitionistic predicate logic and connect the special cuts, maximum cuts, from sequent derivations and maximum segments from derivations of extended natural deduction. We show that the image of a sequent derivation without maximum cuts is a derivation without maximum segments (i.e., a normal derivation) in extended natural deduction.

1. Introduction

In [6] Gentzen introduced a system of sequents for intuitionistic predicate logic, the system LJ, and a natural deduction system for intuitionistic predicate logic, the system NJ. In the papers [2, 4, 6, 8, 9, 10, 11, 15] the similarities and differences between systems of sequents and systems of natural deduction for some fragments of intuitionistic logic were presented. The main goal of most of these papers was to connect the cut-elimination theorem from systems of sequents and the normalization theorem from natural deduction systems, the most important characteristics of these systems. It is well known that there are problems to connect reduction steps of the cut-elimination procedure from a system of sequents and reduction steps of the normalization procedure from a natural deduction system when these systems cover full intuitionistic predicate logic (see, for example, the part 7 in [15]). To solve these problems the authors connected some modifications of Gentzen’s systems LJ and NJ (see [2, 8, 9, 10, 15]), or they defined new reduction steps in cut-elimination and normalization procedures (see [2, 4, 10, 15]). In some papers mentioned above (see, for example, [10, 15]) it was concluded that “the cut-elimination theorem and the normalization theorem are equivalent”. It seems that cut-free derivations, i.e., derivations without cuts (from the systems of sequents) correspond to normal derivations, i.e., derivations without maximum segments (from the systems of natural deduction), and vice versa. So, it seems that cuts correspond to maximum segments, and vice versa. However, the connection between cut-free and normal derivations is the following (see Theorem 3 and Theorem 4 in Section 5 from [15]):

2010 Mathematics Subject Classification: Primary 03F05; 03F07.

Key words and phrases: systems of sequents, natural deduction, cut elimination, normalization.

The image of a cut-free derivation is a normal derivation,

but

if a normal derivation is the image of a sequent derivation, then that sequent derivation can have some cuts which can be eliminated.

Zucker’s systems for intuitionistic predicate logic (from [15]), the system of sequents S and the natural deduction system N, were considered in [5]. In derivations of the system S a special kind of cuts, maximum cuts, were defined. Roughly speaking, maximum cuts are cuts whose left cut formula is connected with a principal formula of a right rule (i.e., an introduction rule of a connective or a quantifier) and its right cut formula is connected with a principal formula of a left rule (i.e., an elimination rule of the connective or the quantifier). It was shown that the image of a sequent derivation without maximum cuts from the system S is a normal derivation in the system N, and the sequent image of a normal derivation from the system N is a derivation without maximum cuts in the system S.

In this paper a new pair systems will be considered. Our systems will be the systems from [2] which cover intuitionistic predicate logic: the system of sequents SE and the natural deduction system N E. It will be shown that the image of a sequent derivation without maximum cuts from the system SE is a normal derivation in the system N E.

The system SE is the system δE from [2] whose formulae have only upper indices. The system N E is a modification of the following systems: Gentzen’s system NJ from [6] (i.e., Prawitz’s system from [11]) and Zucker’s system N from [15]. In the system N E the introduction rules are introduction rules from a standard natural deduction system (i.e., Gentzen’s system NJ). 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 rules of ∨ and ∃ in a standard natural deduction system. These rules were introduced in the system in [13] which was called a natural extension of natural deduction, so our system N E (which is the system from [1] with different denotation) is called extended natural deduction. We note that the system N E is very similar to the system from [9] (see Note 5 in Section 2.3 in [2]). To connect derivations of the systems SE and N E we will use the map ψ from the set of derivations of SE onto the set of derivations of N E (which was also defined in [2]). The definition of maximum cuts in derivations of the system SE will be the definition of maximum cuts in derivations of the system S from [5]. In the system N E elimination rules for all connectives and quantifiers have form as the elimination rules of ∨ and ∃ in a standard natural deduction system, so all elimination rules of the system N E can make maximum segments. Thus, maximum segments in derivations of the system N E and maximum segments in derivations of a standard natural deduction system are different. We will show that maximum cuts from the system SE, which is a standard system of sequents, correspond to maximum segments from the system N E, which is one no standard natural deduction system.

In Section 2 the systems SE and N E and the map ψ, which connects their derivations, will be presented. In the parts 3.1 and 3.2 of Section 3 we will define maximum cuts and maximum segments in the system SE and the system N E, respectively. Finally, in the part 3.3 we will show the following: if D is a derivation without maximum cuts from the system SE, then ψD is a normal derivation in the system N E.

2. The systems SE and N E

Our language will be the language of the first order predicate calculus, i.e., it will have the logical connectives ∧, ∨ and ⊃, quantifiers ∀ and ∃, and a propositional constant ⊥ (for absurdity). Bound variables will be denoted by x, y, z, …, free variables by a, b, c, …, and individual terms by r, s, t, . . .. Letters P, Q, R, … will denote atomic formulae and A, B, C, … will denote formulae.

2.1. The system SE. A sequent of the system SE has the form Γ → A, where Γ is a finite set of formulae with upper indices (i.e., indices) and A is one unindexed formula. The upper indices are defined as indices in [15]: a finite nonempty sequence of natural numbers will be called symbol; and a finite non-empty set of symbols will be called an upper index (i.e., index). Symbols will be denoted by s, t and indices by a, b, c, … An index consisting of one symbol s, {s}, will be denoted just by s. For any number i, the index {i} (containing the single symbol i of length 1) will be called an unary index, and will be denoted just by i. Moreover, there are the following operations on indices, which are completely the same as the operations on indices in [15]: (i) the union of two indices a and b, a ∪ b, is again an index and it is simply a set-theoretical union; (ii) the product of a and b is a × b =_{df} {s ∗ t : s ∈ a, t ∈ b}, where ∗ is the concatenation of sequences.

An indexed formula will be denoted by A^{a}, and a set of indexed formulae will be denoted by Γ^{a}. (However, the indices of sets of formulae will usually be omitted.) For a set of indexed formulae Γ we will make the set Γ^{×a} in the following way Γ^{×a} = {C^{c×a} : C^{c} ∈ Γ}. A sequent representation such as A^{a}, A^{b}, Γ implies that a ≠ b, and A^{a} ∉ Γ and A^{b} ∉ Γ, but possibly A^{c} ∈ Γ for some c ≠ a and c ≠ b.

Postulates for the system SE.

Initial sequents i-sequents: A^{j} → A. ⊥-sequents: ⊥^{j} → P, where P is any atomic formula different from ⊥. Inference rules structural rules:

(contraction ) \frac{A^{a}, A^{b}, Γ → C}{A^{a∪b} , Γ → C}

(cut) \frac{Γ → A A^{a}, Δ → C}{Γ^{×a} , Δ → C}

operational rules (i.e., rules for connectives):

left rules  right rules
(⊃L ) \frac{Γ → A  B^{b}, Δ → C}{Γ, A ⊃ B^{i} , Δ → C}  (⊃R ) \frac{(A^{a}), Γ → B}{Γ → A ⊃ B}
(∧L_{1}) \frac{A^{a}, Γ → C}{A ∧ B^{i} , Γ → C}  (∧L_{2}) \frac{B^{b}, Γ → C}{A ∧ B ^{i}, Γ → C}  (∧R ) \frac{Γ → A  Δ → B}{Γ, Δ → A ∧ B}
(∨L ) \frac{(A^{a}), Γ → C  (B^{b}), Δ → C}{A ∨ B ^{i}, Γ, Δ → C}  (∨R_{1}) \frac{Γ → A}{Γ → A ∨ B} (∨R_{2}) \frac{Γ → B}{Γ → A ∨ B}

(∀L) \frac{F t^{a}, Γ → C}{∀xF x^{i}, Γ → C} (∀R) \frac{Γ → F a}{Γ → ∀xF x}

(∃L) \frac{(F a^{a}), Γ → C}{∃xF x^{i}, Γ → C} (∃R) \frac{Γ → F t}{Γ → ∃xF x}

The unary indices i, j, dots from the initial sequents and the lower sequents in the left rules are called initial indices (as Zucker’s unary indices, see 2.2.1 in [15]), and they have to satisfy the restrictions on indices: in any derivation, all initial indices have to be distinct. (In the examples below initial indices will be denote by i, j, k, l, m, n, h, f, . . ..) The notation (C^{c}), Θ → D, which is used in the rules (⊃R), (∨L) and (∃L), is interpreted as C^{c}, Θ → D, if c ≠ ∅, and Θ → D, if c = ∅ (and hence not strictly an index, by our definition, see 2.2.8.(b) in [15]). So, (C^{c}), Θ → D denotes either the sequent C^{c}, Θ → D or the sequent Θ → D.

In the rules (∀R) and (∃L) the variable a is called the proper variable of these rules, and, as usual, has to satisfy the restrictions on variables: in (∀R) the variable a does not occur in formulae Γ ∪ {∀xF x}; and in (∃L) the variable a does not occur in formulae Γ ∪ {∃xF x, C}.

The new formula explicitly shown in the lower sequent of an operational rule is the principal formula, and its subformulae from the upper sequents are the side formulae of that rule. The formula A^{a∪b} is the principal formula, and A^{a} and A^{b} are the side formulae of the contraction. The formulae A and A^{a} from the upper sequents of the cut are the cut formulae. In any inference rule, formulae which are not side, principal or cut formulae, are passive formulae of that rule.

C, D, D′, D_{1} … will denote derivations in the system SE. All formulae making up sequents in a derivation D of the system SE will be called d-formulae of D.

{D \atop Γ → A} will denote the derivation D with the end sequent Γ → A, and ^{\frac{{D \atop Γ′ → A′}}{Γ → A}} r

will denote the derivation C with the last rule r, the end sequent Γ → A and the subderivation D.

A derivation D of the system SE has the proper variable property (PVP) if in D the proper variable of each operational rule (∀R) or (∃L) occurs only above the lower sequent of that operational rule.

Remark 2.1. The proper variable property is a well-known property of derivations from systems of sequents from [6]. Moreover, each derivation can be effectively transformed into one with PVP (see III, 3.10 in [6] for details). Then we assume that our derivations in the system SE have PVP.

Remark 2.2. It is important to note that we will not make distinction between derivations just on the basis of how their initial indices were chosen (see 2.2.12 in [15]).

2.2. The system N E. In the system N E (as in Zucker’s system N in [15]) the indices will be used as a meta-level in a derivation of N E: each occurrence of an assumption formula is associated with a distinct symbol, and each assumption class, i.e., not-empty set of occurrences of the same formula, is associated with an index. For example, A^{s} will denote an assumption occurrence of a formula A; and A^{a} will denote an assumption class of formulae A.

π, \overline{π}, π_{1}, π′, … will denote derivations of the system N E, and Γ, Δ, … will denote finite sets of assumption classes in the derivations of the system N E.

{Γ, (A^{a}), (A^{b}) \atop π} ; C will denote the derivation π, i.e., the derivation of C from Γ ∪

{A^{a}, A^{b}}. As in Zucker’s system N from [15] the set of all assumption classes of π is Γ ∪ {A^{a}, A^{b}}, if a ≠ ∅ and b ≠ ∅; or Γ ∪ {A^{b}}, if a = ∅; or Γ ∪ {A^{a}}, if b = ∅ (see 2.3.3(a) in [15]).

In the derivations of N E we will have the following operations with assumption classes:

Contraction. Two assumption classes of the same formula are replaced by their

union. From the derivation π, {Γ, A^{a}, A^{b} \atop π} ; C , by a contraction of A^{a} and A^{b}, we obtain the

derivation π′. The assumption classes of the same formulae which are contracted

will have stars as supindex. So, the derivation π′ has the form {Γ, A^{a} ^{∗}, A^{b}^{∗} \atop π} ; C .

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

Discharging an assumption class (See the explanation below logical inference rules.)

Postulates in the system N E.

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

Structural rule, contraction: If {Γ, A^{a}, A^{b} \atop π} ; C is a derivation, then so is {Γ, A^{a} ^{∗}, A^{b}^{∗} \atop π} ; C .

Inference rules

elimination rules introduction rules

\begin{aligned}{π_{1} \atop A ⊃ B} & {π_{2} \atop A} & {[B^{b}] \atop π_{3}} ; C \\ & C \end{aligned}(⊃EE)  {[A^{a}] \atop π} ; B ; A ⊃ B (⊃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})  \begin{matrix}A & B \\ A ∧ B \end{matrix} (∧IE)

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

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

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

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

In each of the rules (⊃EE), (⊃IE), (∧EE_{1}), (∧EE_{2}), (∨EE), (∀EE) and (∃EE) (as in Zucker’s system N, see 2.3.8.(a) in [15]) in the brackets [ ] there is the assumption class which is discharged by that rule if its index is not empty, and if it is empty, then nothing is discharged by that rule. Moreover, there may be other assumption classes of the same formula (like the one discharged), and these are not discharged by that rule.

In the rules (∀IE) and (∃EE) the variable a is the proper variable of these rules, and it has to satisfy the well known restrictions on variables, which is similar to the restrictions on variables in the system SE (see also 2.3.8(b) in [15]).

In the system N E for elimination rules of all connectives and quantifiers we have the notions of minor and major premisses which are defined analogously to these notions in [11]. For the rule (⊃EE) the formula A⊃B is the major premiss, the formula A is the first minor premiss and the formula C is the second minor premiss of that rule. We also have the notion of a connection in a derivation π (for details see 2.5.1.(a),(b) in [15]), which is in fact Prawitz’s notion from [11, pp. 28–29].

In the system N E (by using the notions above) we can define the proper variable property (PVP) of a derivation π which is very similar to PVP in the system SE (see 2.5.1(c) in [15] or p. 28 in [11]).

2.3. The map which connects derivations of SE and N E. The map ψ from [2] connects the set of derivations of the system SE, Der(SE), and the set of derivations of the system N E, Der(N E):

ψ : Der(SE) −→ Der(N E)

The map ψ has the property that the image of a derivation D with the end sequent Γ → A is the derivation ψD of the formula A from the set of assumption classes Γ:

ψ( {D \atop Γ → A} ) = {Γ \atop ψD} ; A

The lengths of derivations D and π, lD and lπ, will be defined in the usual way, as the number of all inferences rules in these derivations. The last rules of derivations D and π will be denoted by rD and rπ, respectively.

MAXIMUM CUTS IN EXTENDED NATURAL DEDUCTION 65

The map ψ will be define by an induction on the length of the derivation D, lD. There are several cases which depend on the last rule of the derivation D, rD.

rD  D  ψD
A^{i} → A A^{i}
⊥  ⊥^{i} → P  {⊥^{i} \atop P}
cut  \frac{{D_{1} \atop Γ → A} {D_{2} \atop A^{a}, Δ → C}}{Γ^{×a} , Δ → C}  {Δ, {Γ^{×a} \atop ψD_{1}} ; (A^{a}) \atop ψD_{2}} ; C
contraction  \frac{{D_{1} \atop A^{a}, A^{b}, Γ → C}}{A^{a∪b} , Γ → C}  {A^{a∗} , A^{b∗}, Γ \atop ψD_{1}} ; C
⊃R  \frac{{D_{1} \atop (A^{a}), Γ → B}}{Γ → A ⊃ B}  {Γ, [A^{a}] \atop ψD_{1}} ; B ; A ⊃ B
⊃L  \frac{{D_{1} \atop Γ → A} {D_{2} \atop B^{b}, Δ → C}}{Γ, A ⊃ B^{i}, Δ → C}  \begin{aligned}A ⊃ B^{i} & {Γ \atop ψD_{1}} ; A & {[B^{b}], Δ \atop ψD_{2}} ; C \\ & C \end{aligned}
∧R  \frac{{D_{1} \atop Γ → A} {D_{2} \atop Δ → B}}{Γ, Δ → A ∧ B}  \begin{aligned}{Γ \atop ψD_{1}} ; A & & {Δ \atop ψD_{2}} ; B \\ & A ∧ B \end{aligned}
∧L_{1}  \frac{{D_{1} \atop A^{a}, Γ → C}}{A ∧ B^{i}, Γ → C}  \begin{aligned}A ∧ B^{i} & & {[A^{a}], Γ \atop ψD_{1}} ; C \\ & C \end{aligned}

∧L_{2} The case when rD is ∧L_{2} is similar to the case when rD is ∧L_{1}.

∨R_{1}  \frac{{D_{1} \atop Γ → A}}{Γ → A ∨ B}  {Γ \atop ψD_{1}} ; A ; A ∨ B

∨R_{2} The case when rD is ∨R_{2} is similar to the case when rD is ∨R_{1}.

∨L  \frac{{D_{1} \atop (A^{a}), Γ → C} {D_{2} \atop (B^{b}), Δ → C}}{A ∨ B^{i}, Γ, Δ → C}  \begin{aligned}A ∨ B^{i} & {[A^{a}], Γ \atop ψD_{1}} ; C & {[B^{b}], Δ \atop ψD_{2}} ; C \\ & C \end{aligned}
∀R  \frac{{D_{1} \atop Γ → F a}}{Γ → ∀xF x}  {Γ \atop ψD_{1}} ; F a ; ∀xF x

∀L  \frac{{D_{1} \atop F t^{a}, Γ → C}}{∀xF x^{i}, Γ → C}  \begin{aligned}∀xF x^{i} & & {[F t^{a}], Γ \atop ψD_{1}} ; C \\ & C \end{aligned}

∃R  \frac{{D_{1} \atop Γ → F t}}{Γ → ∃xF x}  {Γ \atop ψD_{1}} ; F t ; ∃xF x

∃L  \frac{{D_{1} \atop (F a^{a}), Γ → C}}{∃xF x^{i}, Γ → C}  \begin{aligned}∃xF x^{i} & & {[F a^{a}], Γ \atop ψD_{1}} ; C \\ & C \end{aligned}

By Remark 2.1 we can suppose that the derivation D has the proper variable property, so ψD is a correct derivation with regard to the restrictions on variables in the cases when rD is a cut.

3. Maximum cuts and maximum segments

3.1. Maximum cuts. In this section the definition of maximum cats in the system SE will be presented. (It is, in fact, the definition of maximum cats in the system S from [5].)

First we give an example of a maximum cut. In Example 3.1 below the last cut, the cut c4, is a maximum cut. Roughly speaking, its left cut formula A ∧ B is connected with the rule ∧R (the introduction of ∧), and its right cut formula A ∧ B^{ilm} is connected with the rule ∧L_{1} (the elimination of ∧).

Example 3.1. The derivation E:

\frac{\frac{\frac{_{C^{h}→C A^{q}→A}}{C^{h} , C⊃A^{f} →A} A^{e}→A}{C^{he} , C⊃A^{fe} →A} c1 B^{g}→B}{C^{he} , C⊃A^{fe} , B^{g}→A∧B} ∧R A∧B^{n} →A∧B

C^{he} , (C⊃A)∨F^{k} , B^{g} , A∧B^{n} →A∧B

\frac{\frac{_{A∧B^{i}→A∧B A∧B^{l}→A∧B}}{A∧B^{il} →A∧B} c2 \frac{\frac{A^{p}→A}{A∧B^{m} →A} ∧L_{1} B^{j} →B}{A∧B^{m} , B^{j} →A∧B}}{A∧B^{ilm} , B^{j} →A∧B}

c3

C^{heilm} , (C⊃A)∨F^{kilm} , B^{gilm} , A∧B^{nilm} , B^{j} →A∧B c4

To define a maximum cut of a derivation we need to introduce some notions which is similar to well-known notions of branches and paths from natural deduction and clusters from systems of sequents (see Remark 3.1 and Remark 3.3 below).

First we consider a formula F. One of its subformulae, a subformula C, will be called a d-subformula C of F, when the form of C and the place of its appearance in the formula F will be important. For example, the formula F ≡ (C ⊃ D) ∧ C has two different d-subformulae C. We note that the relation ”… is a d-subformula of … ” is reflexive and transitive. A d-subformula of a formula F will be called a proper d-subformula when it is not that formula F itself. We also note that in a derivation, two d-formulae of the same form have the same d-subformulae which constitute them. (In the definition of a d-branch below we will use the following convention: the indices of d-formulae will denote their place in a sequence of dformulae where these formulae can or cannot be indexed formulae.)

Let F be a d-formula from a derivation D. A d-branch of the d-formula F in the derivation D will be a sequence of d-formulae F_{1}, …, F_{n}, n ≥ 1, where F_{1} is that d-formula F, and for each i, i ≥ 1, if the d-formula F_{i} is

(i) either a passive formula in the lower sequent of a rule, or a principal formula of a contraction, then F_{i+1} is the corresponding passive formula from one of the upper sequents of that rule or one of the corresponding side formulae from the upper sequent of that contraction, respectively;

(ii) a principal formula in the lower sequent of an operational rule, then F_{i+1} is one of the side formulae (if they exist) from the upper sequents of the rule (which need not be on the same side of → as F_{i});

(iii) a d-formula from an initial sequent, or the principal formula of a rule which does not have one of side formulae, then i = n.

In Example 3.1 above the d-formula (C ⊃ A) ∨ F^{kilm} has the following dbranches:

b : (C ⊃A)∨F^{kilm} , (C ⊃A)∨F^{k}, C ⊃A^{fe} , C ⊃A^{fe} , C ⊃A^{f} , C; b′: (C ⊃A)∨F^{kilm} , (C ⊃A)∨F^{k}, C ⊃A^{fe} , C ⊃A^{fe} , C ⊃A^{f} , A^{q}; and b′′: (C ⊃A)∨F^{kilm} , (C ⊃A)∨F^{k}.

Remark 3.1. Our notion of a d-branch is very similar to the notion of the path in a derivation from natural deduction (see [11, p. 52]).

In a derivation D the d-branch b of a d-formula F which is not a part of dbranches of any other d-formula from D will be called a long d-branch of that d-formula F. The d-branches b, b′ and b′′mentioned above are the long d-branches of the d-formula (C ⊃A) ∨ F^{kilm} .

Remark 3.2. If in a derivation D the d-branch b is a long d-branch of a dformula F, then the d-formula F is either a cut formula or a formula from the end sequent of the derivation D.

In a derivation D for a d-branch b of a d-formula F we define a branch of the d-formula F in D as the sequence of consecutive d-formulae (equal to F) from b whose first formula is the first formula of b, the d-formula F, and the last formula is a d-formula from b such that the next d-formula from b (if it exists) is different from F.

In Example 3.1 the part of the d-branches b, b′ and b′′: (C ⊃ A) ∨ F^{kilm} , (C ⊃A)∨F^{k} is the branch of the d-formula (C ⊃A)∨F^{kilm} .

Remark 3.3. All branches of a d-formula in a derivation form Gentzen’s cluster (see [7, p. 267]) of that d-formula in the derivation.

In Example 3.1 the left cut formula of the cut c4 has the d-branch b_{l1} (which is also the branch of that d-formula): A ∧ B (the left cut formula of the cut c4 itself), A ∧ B (from the sequent A ∧ B^{n} → A ∧ B); and the branch b_{l2}: A ∧ B (the left cut formula of the cut c4 itself), A ∧ B (the principal formula of ∧R). On the other hand, the right cut formula of the cut c4 has the d-branch b_{r}: A ∧ B^{ilm} , A ∧ B^{il}, A ∧ B^{i} (which is also the branch of A ∧ B^{ilm} ). The branch b_{l2} connects the left cut formula of the cut c4 with the rule ∧R, but the d-branch b_{r} does not connect the right cut formula of the cut c4 with the rule ∧L_{1}. To make that connection we need to define the notion of the o-tree of a d-formula. In Example 3.1 the sequences of the bold emphasized d-formulae are the o-trees of the left and right cut formula of the cut c4. The o-tree tr_{r} : t_{1}t_{2}t_{3}t_{4}t_{5} of the d-formula A ∧ B^{ilm} consists of the following parts: t_{1} is b_{r}; t_{2} is the inverted long d-branch (i.e., the long d-branch written in the inverse order) of the left cut formula A ∧ B of the cut c2, which is that d-formula itself; t_{3} is the d-branch of the right cut formula A∧B^{l} of the cut c2, which is that d-formula itself; t_{4} is the inverted long d-branch of the d-formula A∧B from A ∧ B^{il} → A ∧ B which consists of that d-formula and the d-formula A ∧ B from A∧B^{l} → A∧B; t_{5} is the right cut formula A∧B^{m} of the cut c3. On the other hand, the left cut formula of the cut c4 has two o-trees tr_{l1} and tr_{l2}. The o-tree tr_{l1} is t_{1}^{l1}t_{2}^{l1}, where t_{1}^{l1} is b_{l1} and t_{2}^{l1} is the inverted long d-branch of the d-formula A ∧ B^{nilm} : A ∧ B^{n}, A ∧ B^{n}, A ∧ B^{nilm} . The o-tree tr_{l2} is the branch b_{l2}. Roughly speaking, in a derivation one o-tree of a d-formula F will consist of its branch and d-branches and inverted long d-branches of some d-formulae, alternately. The first part of an o-tree of a d-formula F will be one branch of that d-formula F. The next parts (if they exist) which make that o-tree will be the d-branches of cut formulae and inverted long d-branches of cut formulae, alternately. The last part of that o-tree can be: the branch of the d-formula F which ends with the principal formula of an operational rule (see tr_{l2} above); a cut formula (see tr_{r} above); the inverted long d-branch of a d-formula from the end sequent of the derivation (see tr_{l1} above); or a d-formula from an initial sequent.

Now we define the notion of the o-tree of a d-formula in a derivation.

First, for a d-branch b : F_{1}, …, F_{n} of a d-formula F and one d-subformula of F, the d-subformula C, we define the following notions: (i) the sequence of dformulae b^{−1} is F_{n}, …, F_{1}; (ii) the d-branch b is a part of C when F_{n} is a proper d-subformula of C; (iii) C is a part of the d-branch b when C is a d-subformula of F_{n}.

Let F be a d-formula from a derivation D. An o-tree of the d-formula F in the derivation D (a D-tree of F) will be a sequence t_{1} …t_{n} (n ≥ 1), where t_{1} is a branch of the d-formula F in D, and t_{i}, i > 1, are some sequences of d-formulae from D which are made in the following way.

− If the last d-formula of t_{1} is a principal formula of an operational rule, then n = 1.

− If the last d-formula of t_{1} belongs to an initial sequent, then n > 1 and for each k, k ≥1:

If the last d-formula of t_{2k−1} is

(i) one d-formula of an i-sequent and C_{m} is other d-formula of that i-sequent, then t_{2k} is b^{−1} , where b : C_{1}, …, C_{m} is a long d-branch which ends in C_{m};

(ii) a d-formula from a ⊥-sequent, then t_{2k} is the other d-formula from that ⊥-sequent and n is 2k.

If the last d-formula of t_{2k} is

(i) a d-formula from the end sequent of D, then n is 2k;

(ii) the d-formula C_{1}, which is a cut formula of a cut whose other cut formula is C (C_{1} and C have the same form), then t_{2k+1} can be (a) only the d-formula C, when there is a d-branch of C which is a part of F

and n = 2k + 1;

(b) a d-branch of C which ends in an initial sequent and whose part is F (if it exists);

(c) one empty sequence, i.e., n = 2k, and t_{2k} has to be changed, it becomes only its first d-formula, otherwise.

Remark 3.4. In a derivation D we have the following picture: if a d-formula F has an o-tree tr: t_{1} …t_{n} where n is an odd number, then either n = 1, i.e., the last formula of t_{1} is the principal formula of an operational rule, or n = 2k + 1 (for some k, k ≥ 1), i.e., t_{n} is a cut formula whose d-branch contains the principal formula (which is equal to F) of an operational rule. So, if n is an odd number, then we conclude that the d-formula F is connected with a rule which makes F (i.e., an operational rule whose principal formula is equal to F).

In a derivation D an o-tree tr: t_{1} …t_{n} of a d-formula F is solid if n is an even number, otherwise the o-tree tr is not solid.

Lemma 3.1. Let A be a d-formula in a derivation D and tr: t_{1} …t_{n} be an o-tree of the d-formula A.

(1) n is an even number iff the last d-formula of the o-tree tr belongs to the end sequent of D or an initial sequent.

(2) n is an odd number iff the last d-formula of the o-tree tr is either the principal formula of an operational rule or a cut formula whose one d-branch contains the principal formula A of an operational rule.

Proof. By the definition of o-trees of a d-formula in a derivation. □

In Example 3.1 the left cut formula of the cut c4 has one no solid o-tree, the o-tree tr_{l2} and one solid o-tree, the o-tree tr_{l1}.

All possible o-trees of a d-formula F in a derivation D form the origin of the d-formula F in the derivation D. A d-formula F has the safe origin in a derivation D if all its o-trees are solid; otherwise that d-formula F has no safe origin in that derivation.

Lemma 3.2. A d-formula A has the safe origin in a derivation D iff the last d-formula of each o-tree of A in D belongs to either the end sequent of D or one initial sequent.

Proof. By the definition of the safe origin and Lemma 3.1. □

Lemma 3.3. Let A be a d-formula from the end sequent of a derivation D which has the corresponding d-formula in an upper sequent of the last rule of D. If the d-formula A has the safe origin in D, then its corresponding d-formula from the upper sequent has the safe origin in the subderivation of D which ends with that sequent.

Proof. There are several cases which depend on the last rule of the derivation D. It can be either a rule with the d-formula A as its passive formula, or a contraction whose principal formula is the d-formula A. We will only consider the most interesting case when the last rule of D is a cut. (The other cases are similar and

easier.) The derivation D is ^{\frac{\begin{matrix}D_{1} \\ A, Γ → B \end{matrix}  \begin{matrix}D_{2} \\ B^{b}, Δ → C \end{matrix}}{A^{×b} , Γ^{×b} , Δ → C}}  cut. We consider the d-formula

A^{×b} from the end sequent of D with the safe origin in D, and its corresponding d-formula A from the left upper sequent of the last rule in D, the sequent A, Γ→B. We should show that A from the sequent A, Γ→B has the safe origin in the derivation D_{1}. By Lemma 3.2, each D-tree of A^{×b} ends in A^{×b} , Γ^{×b} , Δ → C or in an initial sequent from D (from D_{1} or D_{2}). So, by the definition of o-trees each D-tree of A^{×b} of the first kind and each D-tree of A^{×b} of the second kind which ends in D_{2} can contain the d-formulae B from A, Γ → B and B^{b} from B^{b}, Δ → C. On the other hand, each D_{1}-tree of A from A, Γ → B has to be one part of one D-tree of A^{×b} . Thus, D-trees of A^{×b} make all D_{1}-trees of the d-formula A from A, Γ→B, and there are the following cases: (i) if one D-tree of A^{×b} ends in an initial sequent from D_{1}, then that D-tree without the d-formula A^{×b} is one D_{1}-tree of the d-formula A from A, Γ→B; (ii) if one D-tree of A^{×b} ends in an initial sequent from D_{2} or in the end sequent of D, then the part of that D-tree which ends in A, Γ → B and does not contain A^{×b} is one D_{1}-tree of the d-formula A from A, Γ→B. So, all D_{1}-trees of that d-formula A from A, Γ → B end either in an initial sequent from D_{1}, or in A, Γ→B. Thus, by Lemma 3.2, the d-formula A from A, Γ→B has the safe origin in the derivation D_{1}. □

Let ^{\frac{\begin{matrix}D_{1} \\ Γ → A \end{matrix}  \begin{matrix}D_{2} \\ A^{a}, Δ → D \end{matrix}}{Γ^{×a} , Δ → D}}  cut be a subderivation of a derivation D. The last

rule of that subderivation, will be called a maximum cut of the derivation D (one m-cut of D) if neither the d-formula A from Γ → A nor the d-formula A^{a} from A^{a}, Δ → D has safe origin in the derivation D.

In the Example 3.1 the cuts c2, c3 and c4 are m-cuts of the derivation E. However, the cut c1 is not m-cut of E.

Example 3.2. The derivation D:

\frac{\frac{\frac{\frac{\frac{\frac{C^{f} →C}{E∧C^{h}→C} ∧L_{2}}{E∧C^{h}→C∨D} ∨R_{1} C∨D^{e}→C∨D}{E∧C^{he} →C∨D}  c1 B^{l}→B}{E∧C^{he} , B^{l}→(C∨D)∧B} ∧R (C∨D)∧B^{n} →(C∨D)∧B}{(E∧C)∨F^{k} , B^{l} , (C∨D)∧B^{n} →(C∨D)∧B}  ∨L \frac{\frac{C∨D^{m} →C∨D E^{g}→ E}{C∨D^{m} , (C∨D)⊃E^{i}→E}  ⊃L}{(C∨D)∧B^{j} , (C∨D)⊃E^{i}→E} ∧L_{1}}{(E∧C)∨F^{kj} , B^{lj} , (C∨D)∧B^{nj} , (C∨D)⊃E^{i}→E} c2

In Example 3.2 the left formula of the cut c1, the d-formula C ∨ D has not safe origin. The right cut formula of the cut c1, the d-formula C ∨ D^{e}, has the safe origin which consists of the solid o-tree t_{1}t_{2}t_{3}t_{4} (the bold emphasized d-formulae), where

t_{1} : C ∨ D^{e};
t_{2} : C ∨ D, C ∨ D, (C ∨ D) ∧ B, (C ∨ D) ∧ B;

t_{3} : (C ∨ D) ∧ B^{j} , C ∨ D^{m}, C ∨ D^{m};

t_{4} : C ∨ D, (C ∨ D) ⊃ E^{i}, (C ∨ D) ⊃ E^{i}, (C ∨ D) ⊃ E^{i}. So, the cut c1 is not m-cut of the derivation D. The following lemma is a simple consequence of the definition of m-cuts.

Lemma 3.4. If D is a derivation without m-cuts, then each subderivation of D is a derivation without m-cuts.

3.2. Maximum segments. Normal derivations in the system N E will be defined in an usual way as derivations without maximum segments, where maximum segments are parts of derivations which begin with the consequence of an introduction rule for a connective (or a quantifier) and end with the major premiss of an elimination rule for that connective (that quantifier).

To define maximum segments we first need the notion of a thread in a derivation π. (It is in fact Prawitz’s notion from [?, ]. 25]DP.) A sequence A_{1}, …, A_{n} of consecutive formulae in a derivation π is a thread if (1) A_{1} is a top formula; (2) A_{i}, for each i < n, stands immediately above A_{i+1} in π; and (3) A_{n} is the end formula in the derivation π.

The most important difference between the system N E and a standard natural deduction system, (for example Prawitz’s system from [11]) is that in N E the elimination rule for each connective and quantifier has the form as the elimination rules for ∨ and ∃ from Prawitz’s system. So, the definitions of a segment in a derivation from Prawitz’s system (see [11, p. 49]) and the system N E are different. In a derivation π of the system N E a segment is a sequence of consecutive formulae C_{1}, …, C_{n} in a thread of that derivation π which are of the same form and (1) C_{1} is not the consequence of an elimination rule; (2) C_{i}, for all i < n, is either a minor premiss of an elimination rule for ∧, ∨, ∀ or ∃, or the second minor premiss of an elimination rule for ⊃; (3) C_{n} is not the minor premiss of an elimination rule. A maximum segment is a segment that begins with the consequence of an introduction rule and ends with the major premiss of an elimination rule.

Now we present one example of a maximum segment in derivations from the system N E. (All forms of maximum segments in derivations of the system N E were presented in Section 5.3 in [2].)

Example 3.3. We consider the derivation π: \begin{matrix}\begin{aligned}{Γ \atop π_{1}} ; A ⊃ B & {Δ \atop π_{2}} ; A & {[B^{b}], Λ \atop π_{3}} ; C ∧ D \\ & C ∧ D \end{aligned} ⊃ EE & {[C^{c}], Θ \atop π_{4}} ; G \\ G \end{matrix} ; ∧EE_{1},

where in the subderivation π_{3} there is an introduction rule whose consequence is a formula C ∧ D. The segment which begins with that formula and ends with the major premiss C ∧ D of the rule ∧EE_{1} is a maximum segment of the derivation π.

The notion of maximum formula is a special case of the notion of maximum segment, i.e., a maximum segment which consists of one formula is a maximum formula. Namely, if a formula is the consequence of an introduction rule and also the major premiss of an elimination rule, then that formula will be called a maximum formula.

Example 3.4. We consider the derivation π′: \begin{aligned}{[C^{c}], Γ \atop π_{1}} ; D ; C ⊃ D ⊃IE & & {Δ \atop π_{2}} ; C & {[D^{d}], Λ \atop π_{3}} ; B \\ & B \end{aligned} ; ⊃EE.

The formula C ⊃D is the consequence of the introduction rule ⊃IE and the major premiss of the elimination rule ⊃ EE, so that formula is one maximum formula of the derivation π′.

A derivation π which contains no maximum segments will be called a normal derivation in the system N E.

3.3. The connection between maximum cuts and segments.

Lemma 3.5. Let D be a derivation without m-cuts whose end sequent is Γ→A. If in the derivation D the d-formula A from Γ → A has the safe origin, then the derivation ψD does not have a segment which contains its last formula A and the consequence of an introduction rule.

Proof. By an induction on the length of the derivation D. The d-formula A has the safe origin in D, so the last rule of D cannot be a right rule. If D is an initial sequent, then the proof is trivial.

(1) The last rule of D is a left rule or a contraction. Let D end with ∧L_{1}. (The other cases when D ends with some other left rule or a contraction are completely

analogous.) The derivations D and ψD are ^{\frac{\begin{matrix}D_{1} \\ C^{c}, Λ → A \end{matrix}}{C ∧ D^{i}, Λ → A}} ∧L_{1} and {C ∧ D^{i} {[C^{c}], Λ \atop ψD_{1}} ; A \atop A}^{∧EE_{1}}

where the d-formula A from C∧D^{i}, Λ→A has the safe origin in D. By Lemma 3.4, the derivation D_{1} does not have m-cuts, and by Lemma 3.3, the d-formula A from C^{c}, Λ → A has the safe origin in D_{1}. The length of D_{1} is smaller than the length of D. So, by the induction hypothesis, the lemma holds for the derivation D_{1} and its image ψD_{1}. Thus, the lemma also holds for the derivation D and its image ψD.

(2) The case when the last rule of D is a cut which is not m-cut. The derivations

D and ψD are ^{\frac{\begin{matrix}D_{1} \\ Λ → B \end{matrix}  \begin{matrix}D_{2} \\ B^{b}, Δ → A \end{matrix}}{Λ^{×b} , Δ → A}}  cut and {Δ,{Λ^{×b} \atop ψD_{1}} ; (B^{b}) \atop ψD_{2}} ; A , where the d-formula A from

Λ^{×b} , Δ → A has the safe origin in D. By Lemma 3.4, the derivation D_{2} does not have m-cuts, and by Lemma 3.3, the d-formula A from B^{b}, Δ→A has the safe origin in D_{2}. The length of D_{2} is smaller than the length of D. So, by the induction hypothesis the lemma holds for the derivation D_{2} and its image ψD_{2}. Thus, the lemma also holds for the derivation D and its image ψD. □

Lemma 3.6. Let D be a derivation without m-cuts whose end sequent is the sequent A^{a}, Γ → B. If the d-formula A^{a} has the safe origin in D, then in the derivation ψD any A from the class A^{a} does not belong to a segment which contains the major premiss of an elimination rule.

Proof. By an induction on the length of the derivation D. The formula A^{a} has the safe origin in D, so the last rule of D cannot be a left rule with principal formula A^{a}. If D is an initial sequent, then the proof is trivial. The cases when the last rule of D is an operational rule whose principal formula is not A^{a} or a contraction are similar to the part (1) in the proof of Lemma 3.5. We consider the case when the last rule of D is a cut which is not m-cut. The derivations D and ψD are

\frac{\begin{matrix}D_{1} \\ A^{a′} , Λ → C \end{matrix}  \begin{matrix}D_{2} \\ C^{c}, Δ → B \end{matrix}}{A^{a′×c} , Λ^{×c} , Δ → B}  cut and {Δ,{A^{a′×c} , Λ^{×c} \atop ψD_{1}} ; (C^{c}) \atop ψD_{2}} ; B ,

where a is a′×c. (The case when A^{a′} belongs to the end sequent of D_{2} is analogous.) The d-formula A^{a′×c} has the safe origin in D. By Lemma 3.4, the derivation D_{1} does not have m-cuts, and by Lemma 3.3, the d-formula A^{a′} from A^{a′}, Λ → C has the safe origin in D_{1}. So, by the induction hypothesis the lemma holds for any formula from A^{a′} in the derivation ψD_{1}. Thus, the lemma also holds for any formula from A^{a′×c} in the derivation ψD. □

The following lemma is a simple consequence of the definition of maximum segments in derivations of the system N E.

Lemma 3.7. Let ψD be {Δ, {Γ^{×a} \atop ψD_{1}} ; (A^{a}) \atop ψD_{2}} ; B , where the derivations ψD_{1} and ψD_{2} are normal

derivations. The derivation ψD has one maximum segment iff

(1) the derivation ψD_{1} has a segment which contains the consequence A of an introduction rule and a formula A from the class A^{a} and

(2) in the derivation ψD_{2} a formula A from the class A^{a} belongs to a segment which contains the major premiss of an elimination rule.

The main result is the following theorem.

Theorem 3.1. If D is a derivation without m-cuts in the system SE, then ψD is a normal derivation in the system N E.

Proof. By an induction on the length of the derivation D. It is obvious that if D is an initial sequent, then ψD is a normal derivation. If the last rule of D is an operational rule or a contraction, then (by Lemma 3.4) the subderivations of D which end with the upper sequents of the last rule of D do not have m-cuts. So, by the induction hypothesis their ψ-images are normal derivations. Thus, ψD is a normal derivation (by the definition of the map ψ). The most interesting case is when the last rule of D is a cut which is not m-cut. The derivations D and ψD are

\frac{\begin{matrix}D_{1} \\ Γ → A \end{matrix}  \begin{matrix}D_{2} \\ A^{a}, Δ → B \end{matrix}}{Γ^{×a} , Δ → B}  cut and {Δ,{Γ^{×a} \atop ψD_{1}} ; (A^{a}) \atop ψD_{2}} ; B

The derivation D_{1} and D_{2} do not have m-cuts (by Lemma 3.4) and lengths of D_{1} and D_{2} are smaller than the length of D. So, by the induction hypothesis, ψD_{1} and ψD_{2} are normal derivations in the system N E. The last rule of D is not m-cut, so, the d-formula A from Γ→A has safe origin or the d-formula A^{a} from A^{a}, Δ→B has safe origin in D. By Lemma 3.3 and the definition of the o-tree: A from Γ→A has safe origin in D_{1}, or A^{a} from A^{a}, Δ→B has safe origin in D_{2}. Thus, by Lemma 3.5 and Lemma 3.6: ψD_{1} does not have a segment which contains its last formula A and the consequence of an introduction rule, or in ψD_{2} any A from the class A^{a} does not belong to a segment which contains the major premiss of an elimination rule. So, by Lemma 3.7, the derivation ψD does not have maximum segments, i.e., ψD is a normal derivation in the system N E. □

References

[1] M. Borisavljević, Sequents, natural deduction and multicategories, Ph. D. thesis, University of Belgrade, 1997 (in Serbian).

[2] M. Borisavljević, Extended natural deduction images of conversions from the systems of sequents, J. Log. Comput. 14/6 (2004), 769–799.

[3] M. Borisavljević, Maximum segments and cuts, Proc. 5th Panhellenic Logic Symp., July 25–28, University of Athens, Greece, (2005), 40–48.

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

[5] M. Borisavljević, Normal derivations and sequent derivations, J. Philos. Log. 37(6) (2008), 521–548.

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

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

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

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

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

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

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

[13] P. Schrdeder-Heister, A natural extension of natural deduction, J. Symb. Log. 49 (1984), 1284–1300.

[14] A. S. Troelstra, and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 1996.

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

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

mirjanab@afrodita.rcub.bg.ac.rs