PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 82(96) (2007), 37–53 DOI 102298/PIM0796037B

NORMAL FORM THEOREM FOR SYSTEMS OF SEQUENTS

Mirjana Borisavljević

Abstract. In a system of sequents for intuitionistic predicate logic a theorem, which corresponds to Prawitz’s Normal Form Theorem for natural deduction, are proved. In sequent derivations a special kind of cuts, maximum cuts, are defined. Maximum cuts from sequent derivations are connected with maximum segments from natural deduction derivations, i.e., sequent derivations without maximum cuts correspond to normal derivations in natural deduction. By that connection the theorem for the system of sequents (which correspond to Normal Form Theorem for natural deduction) will have the following form: for each sequent derivation whose end sequent is Γ ⊢ A there is a sequent derivation without maximum cuts whose end sequent is Γ ⊢ A.

1. Introduction

In [5] Gentzen introduced a natural deduction system for intuitionistic predicate logic, the system NJ, and a system of sequents for intuitionistic predicate logic, the system LJ. There are several papers [1, 3, 5, 7, 8, 9, 10, 13] in which natural deduction systems and systems of sequents for some fragments of intuitionistic logic are compared. The most important connection between these systems is the connection between normal derivations, i.e. derivations without maximum segments (from the systems of natural deduction) and cut-free derivations, i.e. derivations without cuts (from the systems of sequents). By that connection the following picture can be made: “normal derivations and cut-free derivations are the same”. However, the precise picture is the following (see for example Theorems 4 and 5 in [3, Section 4]):

(*)

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 has some cuts which can be eliminated.

So, derivations whose images are normal derivations are not only cut-free derivations. These derivations may contain some cuts which are cuts of the special kind. There is the following problem: the definition of cuts of that kind. In [2] and [4] Zucker’s systems for intuitionistic predicate logic from [13], the system of sequents S and the natural deduction system N, were considered. In [2] the notion of maximum cuts was introduced, and the property that images of sequent derivations without maximum cuts are normal derivations in natural deduction was proved (see Theorem in [2]). Moreover, in [4] the property that the sequent images of normal derivations are derivations without maximum cuts, was proved [4, Theorem 3]. (In this paper that property will be presented in Theorem in Section 5 below.) Thus, we have the following:

2000 Mathematics Subject Classification: Primary 03F05.

Key words and phrases: Cut-elimination theorem, normalization theorem.

(**)

The natural deduction image of a sequent derivation without maximum cuts is a normal derivation, and the sequent image of a normal derivation is a derivation without maximum cuts.

In [10] and [11] Prawitz formulated two kinds of theorems about normal derivations from natural deduction: the theorem of the first kind is Normal Form Theorem from [11] (i.e., Theorem 1 from [10, p.50]); and the theorem of the second kind is Normalization Theorem from [11]. The theorem of the first kind presents the following property:

(NF)

If Π is a derivation of A from the set of assumptions Γ,

then there is a normal derivation of A from the set of assumptions Γ.

By the theorem of the second kind, a derivation Π of A from the set of assumptions Γ can be reduced to a normal derivation of A from the set of assumptions Γ (by reductions which were defined in [11]).

By using the connection (**) above we will prove the following property for sequent derivations:

(McfF)

If there is a sequent derivation whose end sequent is Γ ⊢ A, then there is a derivation without maximum cuts whose end sequent is Γ ⊢ A.

That property for sequent derivations without maximum cuts corresponds to the property (NF) for normal derivations from natural deduction.

We will consider the system of sequents S and natural deduction system N for intuitionistic predicate logic which were introduced by Zucker in [13]. Maximum cuts for derivations from the system S, which were introduced in [2], will be defined. The connection between derivations of the systems S and N will be made by two maps: Zucker’s map φ from [13] and the map ϕ. In the system N we will present the property (NF) mentioned above as Normal Form Theorem for the system N. By using Normal Form Theorem for the system N and the second part od the property (**) above we will prove the property (McfF) for derivations of the system S as M-Cut-Free Form Theorem for the system S. That theorem corresponds to Normal Form Theorem for the system N.

In Section 2 Zucker’s systems S and N will be defined. Two maps, Zucker’s map φ and the map ϕ, which connect derivations of the system S and derivations of the system N, will be presented in Section 3. In the first part of Section 4 normal derivations of the system N will be defined, and Normal Form Theorem for the system N will be presented. In the second part of Section 4 maximum cuts in derivations of the system S will be defined, and M-Cut-Free Form Theorem for the system S will be formulated. Finally, M-Cut-Free Form Theorem for the system S will be proved in Section 5.

2. The system of sequents S and the natural deduction system N

In this section we will define the system of sequents S and the natural deduction system N for intuitionistic predicate logic, which were introduced by Zucker in [13]. The systems S and N are very similar to Gentzen’s systems from [5], the systems LJ and NJ, respectively.

The 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 S. The system S is a system of sequents for intuitionistic predicate logic which is introduced in [13]. A sequent of the system S has the form Γ → A, where Γ is a finite set of indexed formulae and A is one unindexed formula. A finite non-empty sequence of natural numbers will be called symbol, and will be denoted by σ, τ,… A finite non-empty set of symbols will be called index, and will be denoted by α, β,… \overline{α} will denote the cardinality of an index α. There are two operations on indices:

(i) the union of two indices α and β, α ∪ β, is again an index and it is simply a set-theoretical union;

(ii) the product of α and β is α × β =_{df} {σ ∗ τ : σ ∈ α, τ ∈ β}, where ∗ is the concatenation of sequences.

An indexed formula will be denoted by A_{α}, and a set of indexed formulae will be denoted by Γ_{α}. (However, the indices of sets of formulae will usually be omitted.) For a set of indexed formulae Γ we will make the set Γ_{×α} in the following way Γ_{×α} = {C_{γ×α} : C_{γ} ∈ Γ}.

Postulates for the system S are: Initial sequents (i.e., axioms):

– logical initial sequents (i.e., i-axioms): A_{i} → A.

– ⊥-initial sequents (i.e., ⊥-axioms): ⊥_{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}

operational rules (i.e., logical 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}

The indices i (i.e. Zucker’s unary indices, see 2.2.1 in [13]) in the initial sequents and the rules ∨L and ∃L are called initial indices, and they have to satisfy the restrictions on indices: In any derivation, all initial indices have to be distinct.

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: a ∉ Γ ∪ {∀xF x}; -in ∃L: a ∉ Γ ∪ {∃xF x, C}.

The notation (C_{γ}), Θ → D, which is used in rules ⊃R, ∨L and ∃L is interpreted as C_{γ}, Θ → D, if γ ≠ ∅ and Θ → D, if γ = ∅ (see 2.2.8(b) in [13] for details).

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 contracted formula A_{α∪β} will be the principal formula, and A_{α} and A_{β} are the side formulae of the contraction. The formulae A and A_{α} from the upper sequents of the cut are the cut formulae. In any rule formulae which are not side, principal or cut formulae are passive formulae of that rule.

D, E, F, D′,D_{1}…. will denote derivations in the system S. Moreover

{D \atop Γ → A} and \frac{{D \atop Γ′ → A′}}{Γ → A} r

will denote a derivation D with the end sequent Γ → A, and a derivation F with the last rule r and the end sequent Γ → A, respectively. In our paper all formulae making up sequents in a derivation D of the system S will be called d-formulae of the derivation D.

A derivation D of the system S has the proper variable property (PVP) if every occurrence in D of a proper variable of an inference ∀R or ∃L is above that inference.

Remark 1. The proper variable property is a well-known property of derivations of sequent systems from [5]. Moreover, each derivation can be effectively transformed into one with PVP (see [5, III, 3.10] for details). So, we assume that our derivations in S have PVP.

2.2. The system N. The system N is a natural deduction system for intuitionistic predicate logic, which is introduced in [13]. In the system N, like in the system S, we also use symbols and indices, but they are not part of the formal system N. They are only used as a meta-level in a derivation of N to denote the following: 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_{σ} will denote an assumption occurrence of a formula A; and A_{α} will denote an assumption class of formulae A.

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

{Γ, (A_{α}), (A_{β}) \atop Π} ; C

will denote a derivation Π, i.e., the derivation of C from Γ ∪ {A_{α}, A_{β}}. Moreover, the set of all assumption classes of Π is Γ∪{A_{α}, A_{β}}, if α ≠ ∅ and β ≠ ∅; or Γ∪{A_{β}}, if α = ∅. (For details see [13, Part 2.3.2].) The formulae from Γ ∪ {A_{α}, A_{β}} are top formulae of the derivation Π, and C is the end formula of the derivation Π.

In derivations of the system N we will have the following operations with assumption classes (for details see [13, 2.3.4, 2.3.5 and 2.3.6]):

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

union. From the derivation Π: {Γ, A_{α}, A_{β} \atop Π} ; C by a contraction of A_{α} and A_{β} we obtain

the derivation Π′: {Γ, A_{α∪β} \atop Π} ; C. But, our notation of a contraction of A_{α} and A_{β} will be

different from that in [13]. The assumption classes of the same formulae which are contracted will have stars as supindex instead of Zucker’s arrows. So the derivation

Π′ has the form {Γ, A_{α}^{∗}, A_{β}^{∗} \atop Π} ; C.

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

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

Postulates in the system N:

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

Structural rule, contraction: If {Γ, A_{α}, A_{β} \atop Π} ; Cis a derivation, then so is {Γ, A_{α}^{∗}, A_{β}^{∗} \atop Π} ; C.

Logical inference rules Introduction rules (I-rules): Elimination rules (E-rules):

{[A_{α}] \atop Π} ; B ; A ⊃ B (⊃I)  \begin{matrix}A ⊃ B & A \\ B \end{matrix} (⊃E)

\begin{matrix}A & B \\ A ∧ B \end{matrix} (∧I)  {A ∧ B \atop A} (∧E_{1})  {A ∧ B \atop B} (∧E_{2})

{A \atop A ∨ B} (∨I_{1})  {B \atop A ∨ B} (∨I_{2})  \begin{aligned}{Π_{1} \atop A ∨ B} & {[A_{α}] \atop Π_{2}} ; C & {[B_{β}] \atop Π_{3}} ; C \\ & C \end{aligned}(∨E)

{F a \atop ∀xF x} (∀I)  {∀xF x \atop F t} (∀E)

{F t \atop ∃xF x} (∃I)  \begin{aligned}{Π_{1} \atop ∃xF x} & & {[F a_{α}] \atop Π_{2}} ; C \\ & C \end{aligned} ; (∃E)

⊥-rule:

{⊥ \atop P} (⊥)

In each of the rules ⊃I, ∨E and ∃E in the brackets [ ] there is the assumption class which is discharged by that rule if its index is not ∅, and if it is ∅, then nothing is discharged by that rule. However, 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 ∀I and ∃E a is, as usual, the proper variable of these rules. Proper variables have to satisfy the well-known restrictions on variables, which are similar to the restrictions on variables in the system S [13, 2.3.8(b)].

In the system N we define minor and major premisses of elimination rules whose definitions are similar to the definitions of these notions from Prawitz’s natural deduction [10, p. 22]. In each elimination rule the emphasized formula with connective or quantifier will be called the major premisses of that rule. The rules ∨E and ∃E have minor premisses, the formulae C, which are the end formulae of Π_{2}, Π_{3}, and Π_{2}, respectively. Similarly, in the rule ⊃E the formula A is the minor premiss of that rule.

In the system N (by using the notions above) we can define the proper variable property (PVP) of a derivation Π, [13, 2.5.1(c)] or [10, p.28], which is very similar to PVP in the system S.

Remark 2. In the system N each derivation can be transformed into one with PVP [10, pp.28–29], so we assume that our derivations in N have PVP.

3. Connections between derivations

In this section we will present the definitions of two maps, maps φ and ϕ, which connect the set of all derivations from the system S, Der(S), and the set of all derivations from the system N, Der(N).

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

3.1. The map φ from derivations of S to derivations of N. The map φ sends derivations from the set of all derivations of the system S, Der(S), into the set of all derivations of the system N, Der(N):

φ : Der(S)⟶ Der(N)

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 Γ:

φ\binom{D}{Γ → A} = {Γ \atop φD} ; A

The map φ is defined by an induction on lD. There are several cases which depend on the kind of rD (for details see [13, 2.4]).

rD  D  φD

∅  A_{i} → A  A_{i}
⊥  ⊥_{i} → P  {⊥_{i} \atop P}

cut  \frac{{D′ \atop Γ → A} {D′′ \atop A_{α}, Δ → C}}{Γ_{×α}, Δ → C}  {Δ, {Γ_{×α} \atop φD′} ; (A_{α}) \atop φD′′} ; C

contraction  \frac{{D′ \atop A_{α}, A_{β}, Γ → C}}{A_{α∪β}, Γ → C}  {A_{α}^{∗}, A_{β}^{∗}, Γ \atop φD′} ; C

⊃ R  \frac{{D′ \atop (A_{α}), Γ → B}}{Γ → A ⊃ B}  {Γ, [A_{α}] \atop φD′} ; B ; A ⊃ B

⊃ L  \frac{{D′ \atop Γ → A} {D′′ \atop B_{β}, Δ → C}}{Γ_{×β}, A ⊃ B_{β}, Δ → C}  {\begin{matrix}A ⊃ B_{β} & {Γ_{×β} \atop φD′} ; A \\ (B_{β}), \end{matrix}Δ \atop φD′′} ; C

∧ R  \frac{{D′ \atop Γ → A} {D′′ \atop Δ → B}}{Γ, Δ → A ∧ B}  \begin{matrix}{Γ \atop φD′} ; A & {Δ \atop φD′′} ; B \\ A ∧ B \end{matrix}

∧ L_{1}  \frac{{D′ \atop A_{α}, Γ → C}}{A ∧ B_{α}, Γ → C}  {{A ∧ B_{α} \atop (A_{α}),}Γ \atop φD′} ; C

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

∨R_{1}  \frac{{D′ \atop Γ → A}}{Γ → A ∨ B}  {Γ \atop φD′} ; 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′ \atop (A_{α}), Γ → C} {D′′ \atop (B_{β}), Δ → C}}{A ∨ B_{i}, Γ, Δ → C}  \begin{aligned}A ∨ B_{i} & {[A_{α}], Γ \atop φD′} ; C & {[B_{β}], Δ \atop φD′′} ; C \\ & C \end{aligned}

∀R  \frac{{D′ \atop Γ → F a}}{Γ → ∀xF x}  {Γ \atop φD′} ; F a ; ∀xF x

∀L  \frac{{D′ \atop F t_{α}, Γ → C}}{∀xF x_{α}, Γ → C}  {{∀xF x_{α} \atop (F t_{α}),}Γ \atop φD′} ; C

∃R  \frac{{D′ \atop Γ → F t}}{Γ → ∃xF x}  {Γ \atop φD′} ; F t ; ∃xF x

∃L  \frac{{D′ \atop (F a_{α}), Γ → C}}{∃xF x_{i}, Γ → C}  \begin{aligned}∃xF x_{i} & & {[F a_{α}], Γ \atop φD′} ; C \\ & C \end{aligned}

3.2. The map ϕ from derivations of N to derivations of S. The map ϕ sends derivations from the set of all derivations of the system N, Der(N), into the set of all derivations of the system S, Der(S):

ϕ: Der(N) → Der(S)

The map ϕ has the following property: the image of a derivation Π of the formula A with the set of assumption classes Γ from the system N is the sequent derivation ϕΠ with the end sequent Γ → A:

ϕ(Γ Π ; A) = {ϕΠ \atop Γ → A}

The map ϕ is defined by an induction on lΠ. There are several cases which depend on the kind of rΠ.

rΠ  Π  ϕΠ
∅  A_{i}  A_{i} → A
⊥  {⊥_{i} \atop P}  ⊥_{i} → P

substitution  {Δ, {Γ_{×α} \atop Π′} ; (A_{α}) \atop Π′′} ; C  \frac{{ϕΠ′ \atop Γ → A} {ϕΠ′′ \atop A_{α}, Δ → C}}{Γ_{×α}, Δ → C}

contraction  {A_{α}^{∗}, A_{β}^{∗}, Γ \atop Π′} ; C  \frac{{ϕΠ′ \atop A_{α}, A_{β}, Γ → C}}{A_{α∪β}, Γ → C}

⊃I  {Γ, [A_{α}] \atop Π′} ; B ; A ⊃ B  \frac{{ϕΠ′ \atop (A_{α}), Γ → B}}{Γ → A ⊃ B}

⊃E  \begin{matrix}{Δ \atop Π′′} ; A ⊃ B & {Γ \atop Π′} ; A \\ B \end{matrix}  \frac{{ϕΠ′′ \atop Δ → A ⊃ B} \frac{{ϕΠ′ \atop Γ → A} \frac{A_{i} → A B_{j} → B}{A_{ij}, A ⊃ B_{j} → B}}{Γ_{×ij}, A ⊃ B_{j} → B} cut}{Γ_{×ij}, Δ_{×j} → B} cut

∧I  \begin{matrix}{Γ \atop Π′} ; A & {Δ \atop Π′′} ; B \\ A ∧ B \end{matrix}  \frac{{ϕΠ′ \atop Γ → A} {ϕΠ′′ \atop Δ → B}}{Γ, Δ → A ∧ B}

∧E_{1}  {Γ \atop Π′} ; A ∧ B ; A  \frac{{ϕΠ′ \atop Γ → A ∧ B} \frac{A_{i} → A}{A ∧ B_{i} → A}}{Γ_{×i} → A} cut

∧E_{2} The case when rΠ is ∧E_{2} is similar to the case when rΠ is ∧E_{1}.

∨I_{1}  {Γ \atop Π′} ; A ; A ∨ B  \frac{{ϕΠ′ \atop Γ → A}}{Γ → A ∨ B}

∨I_{2} The case when rΠ is ∨I_{2} is similar to the case when rΠ is ∨I_{1}.

∨E  \begin{aligned}{Λ \atop Π′} ; A ∨ B & {[A_{α}], Γ \atop Π′′} ; C & {[B_{β}], Δ \atop Π′′′} ; C \\ & C \end{aligned}  \frac{{ϕΠ′ \atop Λ → A ∨ B} \frac{{ϕΠ′′ \atop (A_{α}), Γ → C} {ϕΠ′′′ \atop (B_{β}), Δ → C}}{A ∨ B_{i}, Γ, Δ → C}}{Λ_{×i}, Γ, Δ → C} cut

∀I  {Γ \atop Π′} ; F a ; ∀xF x  \frac{{ϕΠ′ \atop Γ → F a}}{Γ → ∀xF x}

∀E  {Γ \atop Π′} ; ∀xF x ; F t  \frac{{ϕΠ′ \atop Γ → ∀xF x} \frac{F t_{i} → F t}{∀xF x_{i} → F t}}{Γ_{×i} → F t} cut

∃I  {Γ \atop Π′} ; F t ; ∃xF x  \frac{{ϕΠ′ \atop Γ → F t}}{Γ → ∃xF x}

∃E  \begin{aligned}{Δ \atop Π′} ; ∃xF x & & {[F a_{α}], Γ \atop Π′′} ; C \\ & C \end{aligned}  \frac{{ϕΠ′ \atop Δ → ∃xF x} \frac{{ϕΠ′′ \atop (F a_{α}), Γ → C}}{∃xF x_{i}, Γ → C}}{Δ_{×i}, Γ → C} cut

4. Maximum segments and maximum cuts

In the first part of this section we will define the characteristic notions of natural deduction: a thread, a segment and a maximum segment in derivations of the system N. Moreover, we will define normal derivations of the system N, and we will formulate the Normal Form Theorem for the system N.

In the second part of this section we will repeat the definition of maximum cuts in derivations of the system S from [2], and we will show several characteristic examples of derivations from the system S. Next, in the system S we will formulate M-cut-free Form Theorem, which correspond to Normal Form Theorem for the system N.

4.1. Maximum segments. In this section we first define the notion of a thread in a derivation Π from the system N. (It is in fact Prawitz’s notion from [10, p. 25]). A sequence A_{1},A_{2},…,A_{n} of consecutive formula occurrences in a derivation Π is a thread if (1) A_{1} is a top formula; (2) A_{i} stands immediately above A_{i+1} in Π for each i < n; and (3) A_{n} is the end formula in the derivation Π. Next, we repeat Prawitz’s definition of a segment in a derivation Π [10, p. 49]: a segment in a derivation Π is a sequence A_{1}, A_{2}, …, A_{n} of consecutive formula occurrences in a thread of that derivation Π such that (1) A_{1} is not the consequence of a rule ∨E or a rule ∃E; (2) A_{i}, for each i < n, is a minor premiss of a rule ∨E or a rule ∃E;

(3) A_{n} is not the minor premiss of a rule ∨E or a rule ∃E. (Note that all formulae in a segment are of the same form.) Finally, a maximum segment is a segment that begins with a consequence of an introduction rule and ends with a major premiss of an elimination rule.

Example 1. We consider the derivation Π_{1}:

{Λ \atop Π′} ; A ∨ B {[A_{α}], Γ_{1} \atop Π′′} ; C ∧ D {[B_{β}], Γ_{2} \atop Π′′′} ; C ∧ D C ∧ D ∨E C, ∧E_{1}Δ

Π H

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

The notion of maximum formula is a special case of the notion of maximum segment, i.e., a maximum formula is a maximum segment which consists of one 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 2. We consider the derivation Π_{2}:

\begin{matrix}\begin{matrix}{Γ \atop Π′} ; C & {Δ \atop Π′′} ; D \\ C ∧ D \end{matrix} & ∧I \\ C \end{matrix} ; ∧E_{1}

The formula C ∧ D is the consequence of ∧I, and also the major premiss of ∧E_{1}, i.e. it is a maximum formula of the derivation Π_{2}.

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

Remark 3. Our definition of a normal derivation is the same as Prawitz’s definition of a normal derivation from [11]. In [11] Prawitz also defined a full normal derivation as a normal derivation without redundant applications of ∨E and ∃E. However, in [10] his full normal derivations from [11] were called normal derivations.

Now in the system N as a natural deduction system we present Normal Form Theorem:

Theorem (Normal Form Theorem). If Γ Π ; A is a derivation in the system N,

then in the system N there is a normal derivation {Γ \atop Π_{nf}} ; A.

Proof. The proof is similar to the proof of Theorem 1 from [10, pp. 50–51]. □

4.2. Maximum cuts. In this section first we give an example of a maximum cut. In the derivation E_{3} from Example 3 below the cut c3 is a maximum cut. Its left cut formula A∨B “is connected” with the rule ∨R_{1} (i.e., “the introduction of ∨”), and its right cut formula A∨B_{{n,k}} “is connected” with the rule ∨L (i.e., “the elimination of ∨”).

Example 3. The derivation E_{3}:

\frac{A_{q}→A}{A∧C_{q}→A} \frac{\frac{\frac{\frac{A_{i}→A}{A_{i}→A∨B}∨R_{1} A∨B_{l}→A∨B}{A_{il}→A∨B} c1 A∨B_{m}→A∨B}{A_{ilm}→A∨B} c2 \frac{\frac{\frac{\frac{A_{j}→A}{A_{j}→A∨B} \frac{B_{p}→B}{B_{p}→A∨B}}{A∨B_{n}→A∨B} ∨L A∨B_{k}→A∨B}{A∨B_{n}, A∨B_{k}→(A∨B)∧(A∨B)}}{A∨B_{\{n,k\}}→(A∨B)∧(A∨B)}}{A_{\{ilmn,ilmk\}}→(A∨B)∧(A∨B)} c3

A∧C_{{qilmn,qilmk}}→(A∨B)∧(A∨B) c4

To define maximum cuts of a derivation D we need to introduce some notions by which a precise connection between d-formulae in a derivation can be made. More precisely, some of the notions below will be well-known notions from systems of sequents (see Remark 5 below).

First we consider a formula A. One of its subformulae, a subformula C, will be called a d-subformula C of A, when the form of C and the place of its appearance in the formula A will be important. For example, the formula A ≡ (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 A will be called a proper d-subformula when it is not the formula A itself. We also note that in a derivation, two d-formulae of the same form have the same d-subformulae which constitute them. For example, the d-formulae from an i-axiom A_{i} → A, or the left and the right cut formula of a cut have the same d-subformulae. In a d-formula A we can choose the main d-subformula of the d-formula A.

(In the definition of a d-branch below we will use the following denotation: the indices of d-formulae will denote their place in a sequence of d-formulae where these formulae can or cannot be indexed formulae.)

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

(i) either a passive formula in the lower sequent of a rule, or the 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 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 axiom, or the principal formula of a rule which does not have any side formula, then i = n.

b_{A} : A ≡ F_{1} … F_{n} will denote a d-branch of a d-formula A in a derivation D. Moreover, b, b′, b_{1}, … will denote d-branches in a derivation.

Example 4. We consider the derivation E_{4}:

\frac{A_{k} → A}{A ∧ C_{k} → A} ∧L_{1}  \frac{_{A_{i} → A  B_{j} → B}}{A_{ij}, A ⊃ B_{j} → B} ⊃L
A ∧ C_{kij}, A ⊃ B_{j} → B

cut

(i) we have two d-branches of the emphasized d-formula A⊃B_{j} from the sequent A∧C_{kij}, A⊃B_{j} → B, which consist of emphasized d-formulae in the derivation E_{4}: b_{1} : A⊃B_{j}, A⊃B_{j}, A and b_{2} : A⊃B_{j}, A⊃B_{j}, B_{j};

(ii) the d-formula A∧C_{kij} has one d-branch: A∧C_{kij}, A∧C_{k}, A_{k}.

Remark 4. The notion of a d-branch is very similar to the notion of the path in a natural deduction derivation [10, p. 52].

In a d-branch b : A ≡ F_{1} … F_{n} of a d-formula A we consider a d-formula F_{i}, 1⩽i⩽n with its d-subformula C. The d-subformula C of F_{i} has the corresponding d-subformulae C in F_{1}, F_{2}, …, F_{i−1} when 1 < i, and the d-subformula C of F_{i} will be called the successor of its corresponding d-subformulae from F_{1}, F_{2}, …, F_{i−1}.

In the d-branch b_{1} from Example 4 above, the d-subformula A of the d-formula A from A_{i} → A is the successor of its corresponding d-subformulae from the part A ⊃ B_{j}, A ⊃ B_{j} of b_{1} i.e., that d-formula A is the successor of the d-subformula A of the d-formula A ⊃ B_{j} from the sequent A_{ij}, A ⊃ B_{j} → B and the d-subformula A of the d-formula A ⊃ B_{j} from the sequent A ∧ C_{kij}, A ⊃ B_{j} → B. On the other hand, that d-formula is not a successor of the d-subformula B of the d-formula A ⊃ B_{j} from the sequent A ∧ C_{kij}, A ⊃ B_{j} → B. That d-subformula B has the successor only in the second d-formula of b_{1}, the d-formula A ⊃ B_{j} from the sequent A_{ij}, A ⊃ B_{j} → B.

The part A ≡ F_{1} … F_{k} of a d-branch b : A ≡ F_{1} … F_{n}, 1 ⩽ k ⩽ n, whose all d-formulae have the same form (equal to A) and the next d-formula from b (if it exists) is different from A, will be called a branch of the d-formula A in the derivation D.

In Example 3 the d-branch of the d-formula A_{ilm}, the d-branch b : A_{ilm}, A_{il}, A_{i}, A_{i}, is its branch, too. In Example 4 the part A⊃B_{j}, A⊃B_{j} of both d-branches b_{1} and b_{2} is the branch of the d-formula A⊃B_{j} from A∧C_{kij}, A⊃B_{j} → B.

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

If the last d-formula of a branch of a d-formula A is a principal formula of an operational rule, then that branch will be called a proper branch of the d-formula A.

In Example 4 the branch A ⊃ B_{j}, A ⊃ B_{j} of the d-formula A ⊃ B_{j} from the sequent A ∧ C_{kij}, A⊃B_{j} → B is its proper branch.

In a derivation D the d-branch of a d-formula A which is not a part of any other d-branch from the derivation D will be called a long d-branch of that d-formula A.

Remark 6. If in a derivation D the d-branch b : A ≡ F_{1} … F_{n} is a long dbranch of the d-formula A, then the d-formula A is either a cut formula or a formula from the end sequent of the derivation D.

In Example 4 the d-formulae from the end sequent A ∧ C_{kij}, A ⊃ B_{j} → B have the long d-branches: b_{A∧C_{kij}} : A∧C_{kij}, A∧C_{k}, A_{k}; b_{1} : A ⊃ B_{j}, A ⊃ B_{j}, A; b_{2} : A ⊃ B_{j}, A ⊃ B_{j}, B_{j} and b_{B} : B, B, B. Moreover, the left and the right cut formula of the cut have the long d-branches: b_{A}^{l} : A, A and b_{A_{ij}}^{r} : A_{ij}, A_{i}, respectively.

In Example 3 the right cut formula of the cut c3 has the following branches: b_{r1}: A ∨ B_{{n,k}} (the right cut formula of the cut c3 itself), A ∨ B_{n} (from

A ∨ B_{n}, A ∨ B_{k} → (A∨B) ∧ (A∨B)), A∨B_{n} (from A∨B_{n} → A∨B); and

b_{r2}: A ∨ B_{{n,k}} (the right cut formula of the cut c3 itself), A ∨ B_{k} (from A ∨ B_{n}, A ∨ B_{k} → (A∨B) ∧ (A∨B)), A∨B_{k} (from A∨B_{k} → A∨B);

On the other hand, the left cut formula of the cut c3 has the following branch: b_{l}: A∨B (the left cut formula of the cut c3 itself), A∨B (from A∨B_{m} → A∨B). The branch b_{r1} connects the right cut formula of the cut c3 with the rule ∨L,

but the branch b_{l} does not connect the left cut formula of the cut c3 with the rule ∨R_{1}. To make that connection we need to define the notion of the o-tree of a d-formula.

In Example 3 the sequences of the bold emphasized formulae are the o-trees of the left and right cut formula of the cut c3. The o-tree tr_{l} : t_{1}t_{2}t_{3}t_{4}t_{5} of A∨B consists of the following parts: t_{1} is b_{l}; t_{2} is the reversed long d-branch of the right cut formula A∨B_{m} of the cut c2, which is that d-formula itself; t_{3} is the d-branch of the left cut formula A∨B of the cut c2: A∨B (that d-formula itself), A∨B (from A∨B_{l} → A∨B); t_{4} is the reversed long d-branch of the dformula A∨B_{l} from A∨B_{l} → A∨B which consists of that d-formula itself; and t_{5} is the left cut formula A ∨ B of the cut c1. On the other hand, the right cut formula of the cut c3 has two o-trees: tr_{r1} and tr_{r2}. tr_{r1} is the branch b_{r1}, and t_{r2} is t_{1}^{r}t_{2}^{r}, where t_{1}^{r} is the branch b_{r2} and t_{2}^{r} is the reversed long d-branch of the d-formula (A ∨ B) ∧ (A ∨ B) from the end sequent of the derivation D_{3}: A∨B, (A∨B) ∧ (A∨B), (A∨B) ∧ (A∨B), (A∨B) ∧ (A∨B), (A∨B) ∧ (A∨B).

Roughly speaking, one o-tree of a d-formula C in a derivation will consist of long d-branches and reversed long d-branches of some d-formulae, alternately. The first part of an o-tree of a d-formula C will be a branch of C. The other parts of that o-tree (if they exist) will be the long d-branches of cut formulae and the reversed long d-branches of cut formulae, alternately. An o-tree can end with: the principal formula of an operational rule, a cut formula, a d-formula from an axiom, or a d-formula from the end sequent of the derivation. By the form of one o-tree of a d-formula C o-tree, more precisely, by the last d-formula of its o-tree, we will be able to conclude whether the d-formula C is introduced, i.e., whether a d-formula of the same form, which is connected with that d-formula C, is the principal formula of an operational rule.

Now we define the notion of an o-tree of a d-formula. First, for a d-branch b : A ≡ F_{1} … F_{n} of a d-formula A and one of its d-subformulae, the d-subformula C, we need the following notions.

The sequence of d-formulae b^{−1} is the sequence F_{n} … F_{1}.

(1) If the d-formula F_{n} contains the successor of the d-subformula C, then the d-subformula C is a part of the d-branch b.

(2) If in the d-branch b there is a d-formula F_{j} which is the principal formula of an operational rule and the successor of d-subformula C in F_{j} is that d-formula F_{j} itself, then the d-branch b is a part of the d-subformula C.

(3) If in the d-branch b there is a d-formula F_{j} which has the successor of the d-subformula C and either

(i) F_{j} is the principal formula of ∧L_{1}, ∧L_{2}, ∨R_{1} or ∨R_{2}, j < n and the dformula F_{j+1} does not have the successor of the d-subformula C; or

(ii) F_{j} is the principal formula of ∨L, ⊃R or ∃L, and n = j, then the d-subformula C is a t-part of the d-branch b.

(4) If in the d-branch b there is a d-formula F_{j}, j < n, which has the successor of the d-subformula C, the d-formula F_{j} is the principal formula of one of the operational rules ∧R, ∨L, ⊃R, ⊃L and the d-formula F_{j+1} does not have the successor of the d-subformula C, then the d-subformula C and the d-branch b are not connected.

Remark 7. Let b : A ≡ F_{1} … F_{n} be a d-branch of a d-formula A. All possible connections between the d-branch b and a d-subformula C of the d-formula A are presented in (1), (2), (3) and (4) above.

Let A be a d-formula from a derivation D. An o-tree of the d-formula A in the derivation D will be a sequence t_{1}t_{2} … t_{n} (n ⩾ 1), where t_{1} is a branch of the d-formula A in the derivation D, the main d-subformula of the last d-formula of t_{1} is that d-formula itself, and t_{i} ( i > 1) are some long d-branches and reversed long d-branches from D which are connected 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 axiom, 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-axiom and C_{m} is other d-formula of that axiom, then the main d-subformula of C_{m} is the main d-subformula of the last d-formula of t_{2k−1}, the sequence t_{2k} is b^{−1}, where b : C_{1} … C_{m} is a long d-branch which ends in C_{m}, and the main d-subformula of C_{1} is its dsubformula whose successor in C_{m} is the main d-subformula of C_{m}; (ii) a d-formula from a ⊥-axiom, then t_{2k} is the other d-formula from that

⊥-axiom and n is 2k.

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

(i) a d-formula from the end sequent of the derivation 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 the main d-subformula of C is the main d-subformula of C_{1} and t_{2k+1} can be made in the following way:

(a) if there is a d-branch of C which is a part of the main d-subformula of C, then t_{2k+1} is only the d-formula C and n = 2k + 1;

(b) if there is a d-branch of C which ends in an axiom and whose part is the main d-subformula of C, then t_{2k+1} is that d-branch of C and the main d-subformula of the last d-formula of t_{2k+1} is the successor of the main d-subformula of C;

(c) if there is a d-branch of C whose t-part is the main d-subformula of C, then t_{2k} has to be changed, i.e., t_{2k} becomes only its first d-formula and n = 2k (t_{2k+1} does not exist).

Remark 8. If a d-formula A has an o-tree tr : t_{1} … t_{n} in a derivation D, where n is an odd number, it means that in the derivation D there is a rule which ”makes” a d-formula of the same form as A (i.e., a d-formula of the same form as A is the principal formula of that rule) and that principal formula is connected with the d-formula A by several cuts whose cut formulae belong to tr.

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

In Example 3 for the o-trees tr_{r1}, tr_{r2} and tr_{l} we have the following. The o-tree tr_{r1} is a no-solid o-tree of the right cut formula of the cut c3, the d-formula A∨B_{{n,k}}; the o-tree tr_{r2} is a solid o-tree of that d-formula A∨B_{{n,k}}; and the o-tree tr_{l} is a no-solid o-tree of the left cut formula of the cut c3.

By the following notion we want to make complete information about connections of a d-formula A with principal formulae which have the same form as that d-formula A.

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

Now we can define the notion of a maximum cut of a derivation. Let

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

be a subderivation of a derivation D. That cut, the last rule of that subderivation, will be called a maximum cut of the derivation D if neither of its cut formulae have safe origins in the derivation D. Otherwise, that cut will be called a no-maximum cut of the derivation D.

In Example 3 the cuts c1, c2 and c3 are maximum cuts and the cut c4 is a no-maximum cut of the derivation E_{3}.

Finally, we present the following theorem for the system S:

Theorem (M-Cut-Free Form Theorem). If {D \atop Γ → A} is a derivation in the sys-

tem S, then in the system S there is a derivation without maximum cuts {D_{nf} \atop Γ → A}.

5. The proof of M-Cut-Free Form Theorem

In this section we will prove M-Cut-Free Form Theorem as a consequence of Normal Form Theorem for the system N from Section 4.1. In the proof will be used the second part of the property (**) from the Introduction:

Theorem. If a derivation Π is a normal derivation in the system N, then ϕΠ is a derivation without maximum cuts in the system S.

Proof. The theorem is a consequence of the following properties, which hold for the systems S and N: (i) for each derivation Π from the system N the derivation φϕΠ is Π; and (ii) if φD is a normal derivation in the system N, then D is a derivation without maximum cuts in the system S. □

Proof of M-Cut-Free Form Theorem for the system S. Let {D \atop Γ → A}

be a derivation in the system S. By the map φ, the φ-image of the deriva-

tion D, {Γ \atop φD} ; A , is a derivation in the system N. By Normal Form Theorem for the

system N from Section 4.1, in the system N there is a normal derivation {Γ \atop Π_{nf}} ; A.

Finally, by the definition of the map ϕ and Theorem above, the derivation {ϕΠ_{nf} \atop Γ → A}

is a derivation without maximum cuts in the system S. □

References

[1] M. Borisavljević, [2004] Extended natural-deduction images of conversions from the system of sequents, J. Logic Comput. 14:6, 769–799.

[2] M. Borisavljević, [2005] Maximum segments and cuts; in: Proceedings of the 5th Panhellenic Logic Symposium, 40–48, July 25–28, 2005, Athens, Greece.

[3] M. Borisavljević, [2006] A connection between cut elimination and normalization, Arch. Math. Logic 45:2, 113–148.

[4] M. Borisavljević, [2006] Normal derivations and sequent derivations, manuscript

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

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

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

[8] von J. Plato, [2001] Natural deduction with general elimination rules, Arch. Math. Logic 40:1, 541–567.

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

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

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

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

[13] J. Zucker, [1974] The correspondence between cut-elimination and normalization, Ann. Pure Appl. Logic 7, 1–112.

Saobraćajni fakultet Vojvode Stepe 305 11000 Beograd Serbia

mirjanab@afrodita.rcub.bg.ac.yu