PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 101(115) (2017), 75–98 https://doi.org/10.2298/PIM1715075B

THE NORMALIZATION THEOREM FOR EXTENDED NATURAL DEDUCTION

Mirjana Borisavljević

Abstract. The normalization theorem for the system of extended natural deduction will be proved as a consequence of the cut-elimination theorem, by using the connections between the system of extended natural deduction and a standard system of sequents.

1. Introduction

In [6] Gentzen introduced the natural deduction system, the system NJ, and the system of sequents, the system LJ, for intuitionistic predicate logic. There are numerous papers (see, for example, [3, 4, 8, 10, 12–14, 18]) in which natural deduction derivations and sequent derivations were compared, and connections between the normalization procedure from natural deduction systems and the cutelimination procedure from systems of sequents were studied. Because of the wellknown difficulties of the correspondence between reductions which constitute these two procedures (see, for example, [18, part 1.3]) in the papers mentioned above modifications of Gentzen’s systems NJ and LJ were considered. In [3] a standard system of sequents, the system δE, and a new natural deduction system, the system N E, were studied, where the most important characteristic of the system N E is that the elimination rules for all connectives and quantifiers are of the same form as the elimination rules of ∨ and ∃ in Gentzen’s natural deduction system NJ. (With regard to introduction rules of the system N E, they are the introduction rules from NJ.) That system was called the system of extended natural deduction. Namely, natural deduction elimination rules of that kind were introduced in [16], and the natural deduction with these rules was called a natural extension of natural deduction. Moreover, the natural deduction system from [10] (which was also considered in [9]) has the elimination rules of that kind, which were called general elimination rules, and that system was called natural derivation with general elimination rules. In [3] it was showed that these elimination rules make new maximum segments in derivations of the system N E, which do not exist in NJ, and new conversions (i.e. reductions) of normalization procedure in that system. However, normal derivations in N E were defined in Gentzen’s and Prawitz’s way: derivations without maximum segments. The map ψ from the set of derivations of δE with upper indices (i. e. the system SE from [5]), Der(SE), into the set of derivations of N E, Der(N E), was defined and it was proved the following property: each conversion from the set of conversions of a standard cut-elimination procedure in the system SE has the corresponding conversion in the set of conversions of a normalization procedure in the system N E. (That result in the different denotation and with more details was already presented in [1].)

2010 Mathematics Subject Classification: 03F05.

Key words and phrases: cut elimination, normalization.

Communicated by Žarko Mijajlović.

The main goal of this paper is to prove the normalization theorem for a system of extended natural deduction by using the cut-elimination procedure for a standard system of sequents. Namely, the normalization theorem for N E can be proved by an induction on the length of one derivation π with several cases which depend on the last rule of the derivation π (see Prawitz’s proof of Theorem 1 from Section IV in [14]). We note that for natural deduction with general elimination rules from [10] (which is similar to our system N E) and its normal derivations (see [10, Definition 3.3. in Section 3, p. 549]) two proofs of the normalization are presented in [10] and [9]. In [10] the existence of a normal derivation, which corresponds to a nonnormal derivation, was shown in the following way (see [10, Section 5]): ”Given a non-normal derivation, translation to sequent calculus, followed by cut elimination and translation back to natural deduction, will produce a normal derivation”; and in [9] the direct proof was given. Moreover, in [5], normal derivations of the system were defined as in [3] and by using the map ψ and the connections between the conversions of the cut-elimination procedure in SE and the conversions of the normalization procedure in N E from [3] mentioned above, the normalization theorem for N E was presented as one consequence of the cut-elimination procedure for SE. Namely, for each derivation π from N E it was prowed that (1) there is one derivation D from SE such that ψD is π; and if π is not normal, then (2) there is the sequence of the derivations D, D_{1}, …, D_{n}, n ⩾ 1, which are connected by conversions of a cut-elimination procedure, where D_{n} is cut-free and (3) that sequence makes the sequence of the derivations π, ψD_{i_{1}}, ψD_{i_{2}}, …, ψD_{n}, 1 ⩽ i_{1} < i_{2} < … ⩽ n, which are connected by conversions of normalization procedure, where ψD_{n} is one normal derivation. In this paper we want to define the map from derivations of extended natural deduction to derivations of a standard sequent system, which will be used to make the derivation D, whose existence was showed in the proof from [5] mentioned above. To define that map we will consider the system N E^{o}, which is N E with indices i.e. its formulae have indices, and some inference rules and formulae have numbers, and the system SE^{o}, whose some left rules are different than the left rules of SE.

In Subsections 2.1 and 2.2 the systems SE^{o} and N E^{o} will be defined. In Subsection 2.3 the map ψ from the set of derivations of SE^{o}, Der(SE^{o}), to the set of derivations of N E^{o}, Der(N E^{o}), will be presented (ψ from [3]), and the new map ϕ from Der(N E^{o}) to Der(SE^{o}) will be defined. In Section 3, conversions in the systems SE^{o} and N E^{o}, which are in fact the conversions of δE and N E from [3], will be presented. Finally, in Section 4, the proof of the cut-elimination theorem for the system SE^{o} will be given, and the normalization theorem for the system N E^{o} will be proved by using that theorem. Namely, it will be shown that for each derivation π from N E^{o} (1) there is one derivation ϕπ in SE^{o}, and if π is not normal, then (2) there is a sequence of the sequent derivations ϕπ, D_{1}, …, D_{n}, n ⩾ 1, which are connected by conversions of the cut-elimination procedure, where D_{n} is cut-free and (3) that sequence makes the sequence of the derivations π, π_{1}, …, π_{m}, m ⩽ n, which are connected by conversions of the normalization procedure in N E^{o}, where π_{m} is a normal derivation.

2. The systems SE^{o} and N E^{o}

Our language will be the language of the first order predicate logic, i.e. it will have the logical connectives ∧, ∨ and ⊃ (i.e. ⇒), quantifiers ∀ and ∃, and the 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.

The definition of symbols: (1) each natural number i, i > 0, will be a symbol; and (2) if s_{1} and s_{2} are symbols, then (s_{1})(s_{2}) and ( )(s_{2}) will be symbols. The symbols will be denoted by s, t, … and length of a symbol s, s̄, will be the number of natural numbers in s. The symbols of the length 1 will be denoted by i, j, k, . . .. For one symbol s we have the symbol s^{−}: if s is (1) i, then s^{−} does not exist; (2) (i)(j), then s^{−} is i; (3) (s_{1})(s_{2}), where \overline{s_{1}}, \overline{s_{2}} > 1, then s^{−} is (s_{1})(s_{2}^{−}); (4) ( )(s_{2}), then s^{−} is s_{2}^{−}. A finite non-empty set of symbols will be called the index and it will be denoted by a, b, . . .. The index of the form {s}, for a symbol s, will be denoted by s. The index {i} will be called the initial index, and it will be denoted by i. The number of the members of an index a will be denoted by ā. There are two operations on indices: (i) the union a ∪ b of two indices a and b, which is the set-theoretical union; (ii) the product of two indices a and b is a × b =_{df} {(s) ∗ (t) : s ∈ a, t ∈ b}, where ∗ denotes the concatenation of sequences (s) and (t).

A set of indexed formulae will be denoted by Γ^{a}, but the index a usually will be omitted. For a set of indexed formulae Γ we will make the set Γ^{×a} in the following way Γ^{×a} = {C^{c×a} : C^{c} ∈ Γ}. For a sequent A^{a}, A^{b}, Γ → C 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.

2.1. The system SE^{o}. A sequent of the system SE^{o} has the form Γ → A, where Γ is a finite set of formulae with indices and A is one unindexed formula.

Postulates for the system SE^{o}. Initial sequents i-initial sequents: A^{j} → A. ⊥-initial sequents: ⊥^{j}→ P, where P is an 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}

rules for connectives

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

(∀L) \frac{/At^{a}/, Γ → C}{∀xAx^{j}, Γ → C} (∀R) \frac{Γ → Aa}{Γ → ∀xAx}

(∃L) \frac{/Aa^{a}/, Γ → C}{∃xAx^{j}, Γ → C} (∃R) \frac{Γ → At}{Γ → ∃xAx}

The indices j from the initial sequents and the left rules 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 does not appear in Γ ∪ {∀xAx}; -in ∃L: a does not appear in Γ ∪ {∃xAx, C}. The notation /C^{c}/, Θ → D for a sequent is used to indicate the possibility that c is empty (and hance not strictly an index by the definition above, but we may still call an index for convenience). So, /C^{c}/, Θ → D is interpreted as C^{c}, Θ → D, when c ≠ ∅; and as Θ → D, when c = ∅.

D, E, F, D′, D_{1} … will denote derivations in the system SE^{o}. A derivation with the end sequent Γ → A will be denoted by

\begin{matrix}D \\ Γ → A \end{matrix}, while \frac{\begin{matrix}D \\ Γ′ → A′ \end{matrix}}{Γ → A} r or \frac{\begin{matrix}D′ & D′′ \\ Γ′ → A′ & Γ′′ → A′′ \end{matrix}}{Γ → A} r

will denote a derivation F with the last rule r and the end sequent Γ → A. All formulae making up sequents in a derivation D of SE^{o} will be called d-formulae of the derivation D. A derivation D of SE^{o} has the proper variable property (PVP) if every occurrence in D of a proper variable of an inference of (∀R) or (∃L) is above the lower sequent of that inference.

2.2. The system N E^{o}. The system N E^{o} is an extended natural deduction system. π, π̄, π_{1}, π′, … will denote derivations of the system N E^{o}. Γ, Δ, … will denote finite sets of a-classes (see the definition below) in derivations of the system N E^{o}. One derivation of the formula C from the set of a-classes Γ will be denoted by

\begin{matrix}Γ \\ π \\ C \end{matrix}, while \frac{\begin{matrix}Γ \\ π \end{matrix}}{C} r, \frac{\begin{matrix}Γ & Δ \\ π_{1} & π_{2} \end{matrix}}{C} r or \frac{\begin{matrix}Γ & Δ & Λ \\ π_{1} & π_{2} & π_{3} \end{matrix}}{C} r

will denote one derivation of C whose last inference rule is r. Some inference rules in a derivation π will have numbers and the largest of them will be the number of the derivation π, Nπ. All formulae making up a derivation π of the system N E^{o} will be called the d-formulae of the derivation π. In \begin{matrix}Γ \\ π \\ C \end{matrix} the d-formulae from the a-classes of Γ are the top-formulae of that derivation and their full-forms, can be:

(T1) A^{i},  (T2) A^{t}, t̄> 1,  (T3) (… (A^{t})^{n^{1}} …)^{n^{n}}, t̄⩾ 1, n ⩾ 1,
(T4) [[… [[(… (A^{t})^{n^{1}} …)^{n^{n}}]^{l^{1}}] …]^{l^{l}}]^{l}, t̄⩾ 1, n ⩾ 0, l ⩾ 0,

where i and t are indices of these formulae and n_{1}, …, n_{n}, l_{1}, …, l_{l} and l are numbers of these formulae and some inference rules.

Example 2.1. Trivial derivations (see the definition below), for example, A^{1}, A ∧ B^{4}, have the top-formulae of the form (T1). The top-formulae of π_{1}: \frac{A^{1} B^{2}}{A∧B} ∧IE are of the form (T1), where ∧IE is one inference rule (see below). The operations on derivations, substitutions and contractions (see below) make top-formulae of the forms (T2)–(T4). The result of the substitution of the derivation π_{1} for the dformula A∧B^{4} (which is one a-class, see below) of the trivial derivation A∧B^{4} is π_{2}: \frac{A^{(1)(4)} B^{(2)(4)}}{(A∧B^{()(4)})^{5}} ∧IE; 5 whose top-formulae are of the form (T2). π_{3}: \frac{(A^{(3)(1)})^{4} B^{2}}{A∧B} ∧IE; 4 is the result of the substitution of the derivation A^{3} for the a-class A^{1} of π_{1} and its top-formula (A^{(3)(1)})^{4} is of the form (T3). In π_{4}:

\frac{\frac{[A^{1}]^{4} B^{2}}{A ∧ B} ∧ IE [A^{3}]^{4}}{(A ∧ B) ∧ A} ∧ IE; 4

we have the contraction of the formulae (the a-classes) A^{1} and A^{3} after the second ∧IE and the top-formulae [A^{1}]^{4} and [A^{3}]^{4} are of the form (T4), where n = l = 0 and L is 4. The result of the substitution of the derivation A^{5} for the a-class [A^{1,3}]^{4} of π_{4} (the d-formulae [A^{1}]^{4} and [A^{3}]^{4}) is π_{5}:

\frac{\frac{[(A^{(5)(1)})^{6}]^{4} B^{2}}{A ∧ B} ∧ IE [(A^{(5)(3)})^{6}]^{4}}{(A ∧ B) ∧ A} ∧ IE; 4, 6

where n = 1, l = 0, N_{1} is 6 and L is 4.

The part A^{t} of a top-formula will be called the core of that top-formula. If from a top-formula its core and the first [and the last] with its number (when they exist) are deleted, then the bark of that top-formula will be obtained, and it will be denoted by ⟨ ⟩. For a top-formula of the form (T4), its core is A^{t} and its bark is [… [[(… ( )^{n^{1}} …)^{n^{n}}]^{l^{1}}] …]^{l^{l}} (it is empty, when n = l = 0), and that top-formula will be written [⟨A^{t}⟩]^{l}, but ⟨ ⟩ and [ ]^{L} will usually be omitted. The top-formulae of the forms (T1) and (T2) are equal to their cores and their barks are empty.

The d-formula C is the end-formula of \begin{matrix}Γ \\ π \\ C \end{matrix} and its full-form can be:

(E1) C^{i},  (E2) C,  (E3) (… (C^{s})^{n^{1}} …)^{n^{n}}, n ⩾ 1,

where i and s are indices of these formulae and n_{1}, …, n_{n} are numbers of these formulae and some inference rules. The part C^{s} of each end-formula (where the index s does not exist, when its form is (E2)) will be called the core of that end-formula. If from one end-formula its core is deleted, then the bark of that end-formula will be obtained and it will be denoted by ∥ ∥ (but, ∥ ∥ will usually be omitted). For an end-formula of the form (E3), its core is C^{s} and (… ( )^{n^{1}} …)^{n^{n}} is its bark. The end-formulae of the forms (E1) and (E2) are equal to their cores and their barks are empty.

Example 2.2. Trivial derivations have the end-formulae of the form (E1). In Example 2.1 the end-formulae of π_{1}, π_{3}, π_{4}, and π_{5} are of the form (E2) and the end-formula of π_{2} is of the form (E3), where s is ( )(4), n = 1 and N_{1} is 5.

If a derivation π has one top-formula of the full-form (T4), then it has k topformulae (k > 1) of the full-form (T4) with the same form (i.e. one predicate formula A) and the same number l. The union of the indices (they have one symbol) of all these top-formulae is the index a and all top-formulae whose indices belong to a will make the a-class (i.e. the assumption class) in that derivation π and it will be denoted by [A^{a}]^{l} or A^{a}. Specially, each top-formula of the form (T1)–(T3) is one a-class A^{t} (in (T1) t is i) in that derivation π. If we write

{[A^{s_{1}}]^{l} … [A^{s_{m}}]^{l}Γ \atop π} ; C,

where a = {s_{1}, …, s_{m}}, then it means that the d-formulae [A^{s_{1}}]^{l} … [A^{s_{m}}]^{l} make the a-class [A^{a}]^{l} and in Γ there is not any d-formula from that a-class.

Postulates in the system N E^{o}.

A derivation π in the system N E^{o} is either one trivial derivation A^{i} or one derivation which is made by the following operations on derivations and the inference rules.

(1)Operations on derivations If the derivation π_{1} is

\begin{matrix}[A^{s_{1}}]^{k} … [A^{s_{m}}]^{k}[A^{t_{1}}]^{m} … [A^{t_{n}}]^{m}Γ \\ π′ \\ B \end{matrix},

where a = {s_{1}, …, s_{m}}, b = {t_{1}, …, t_{n}}, m, n ⩾ 1 (k (m) does not exist when m (n) is 1), then the derivation π

[[A^{s_{1}}]^{k}]^{n} … [[A^{s_{m}}]^{k}]^{n}[[A^{t_{1}}]^{m}]^{n} … [[A^{t_{n}}]^{m}]^{n}Γ π′ B (denoted by {[[A^{a}]^{k}]^{n}[[A^{b}]^{m}]^{n}Γ \atop π′} ; B )

is the result of the contraction of the a-classes [A^{a}]^{k} and [A^{b}]^{m} and it has the a-class [A^{a∪b}]^{n}, where n is one number larger than Nπ_{1}, when Nπ_{1} exists and an arbitrary number, otherwise; and n is the number of all formulae of that a-class. The number n is also one number of the last inference rule (see below) of π (that rule can have several numbers) and Nπ = n.

Example 2.3. In π_{4} from Example 2.1 the contraction of the a-classes [A^{1}] and [A^{3}] make the a-class [A^{1,3}]^{4}, 4 is the number of the last inference rule of π_{4} and Nπ_{4} = 4. The result of the contraction of the a-classes [A^{1,3}]^{4} and [A^{5,6}]^{7} in

\frac{{π_{4} \atop (A ∧ B) ∧ A} \frac{[A^{5}]^{7} [A^{6}]^{7}}{A ∧ A}∧IE; 7}{((A ∧ B) ∧ A) ∧ (A ∧ A)}∧IE is \frac{\frac{\frac{[[A^{1}]^{4}]^{8}B^{2}}{A ∧ B}∧IE [[A^{3}]^{4}]^{8}}{(A ∧ B) ∧ A} ∧IE; 4 \frac{[[A^{5}]^{7}]^{8}[[A^{6}]^{7}]^{8}}{A ∧ A}∧IE; 7}{((A ∧ B) ∧ A) ∧ (A ∧ A)}∧IE; 8.

If the derivation π_{1} is \begin{matrix}Γ \\ π′ \\ ∥A^{s}∥ \end{matrix} and the derivation π_{2} is

\begin{matrix}[⟨A^{t_{1}}⟩]^{l} … [⟨A^{t_{n}}⟩]^{l}Δ \\ π′′ \\ B \end{matrix},

where d-formulae (inference rules) of π_{1} and π_{2} have different indices (numbers), b is {t_{1}, …, t_{n}}, n ⩾ 1 (l does not exist when n is 1), then the result of the substitution of the derivation π_{1} for the a-class [A^{b}]^{l} in the derivation π_{2} is the derivation π

\begin{aligned}{[Γ^{×t_{1}}]^{l} \atop π′} ; ⟨(∥A^{(s)(t_{1})}∥)^{n}⟩ & … & {[Γ^{×t_{n}}]^{l} \atop π′} ; ⟨(∥A^{(s)(t_{n})}∥)^{n}⟩ & Δ \\ & & π′′ \end{aligned} ; B (denoted by \begin{matrix}{[Γ^{×b}]^{l} \atop π′} ; (A^{(s)(b)})^{n} & Δ \\ π′′ \end{matrix} ; B )

where n is one number larger than Nπ_{1} and Nπ_{2}, when Nπ_{1} or Nπ_{2} exists and an arbitrary number, otherwise; in each d-formula ⟨(∥A^{(s)(t_{i})}∥)^{n}⟩, 1 ⩽ i ⩽ n, which is one sb-formula of π, ⟨ ⟩ is the bark of the top-formula [⟨A^{t_{i}}⟩]^{l} of π_{2} and ∥ ∥ is the bark of the end-formula of π_{1}, and n is its number and l is its c-number. If π_{1} is one d-formula and l exists, then the sb-formulae are [⟨(∥A^{(s)(t_{i})}∥)^{n}⟩]^{l}, 1 ⩽ i ⩽ n. Each a-class [C^{c}]^{m} from the set of a-classes Γ of π_{1}, c = {r_{1}, …, r_{m}}, m ⩾ 1, has its corresponding a-class [C^{c×b}]^{l} in π, i.e. each d-formula [⟨C^{r_{j}}⟩]^{m} from [C^{c}]^{m} has n corresponding d-formulae [[⟨C^{r_{j}×t_{i}}⟩]^{m}]^{l}, 1 ⩽ i ⩽ n. If one of π_{1} and π_{2} is not one d-formula, then the number n is the number of the last inference rule of π which can have several numbers. If π_{1} and π_{2} are d-formulae, (… (A^{s})^{n^{1}} …)^{n^{n}} and (… (A^{t})^{l^{1}} …)^{l^{l}}, respectively, where n, l ⩾ 0, then π is the d-formula (… (((… (A^{(s)(t)})^{n^{1}} …)^{n^{n}})^{n})^{l^{1}} …)^{l^{l}}. In all cases Nπ = n.

Example 2.4. In π_{2} from Example 2.1 (A ∧ B^{( )(4)})^{5} is the sb-formula of one substitution where 5 is its number and the number of the last inference rule of π_{2}, ∧IE. The substitution of the derivation A ∧ B^{9} for the a-class [A ∧ B^{6,7}]^{8} in

\frac{[A ∧ B^{6}]^{8}[A ∧ B^{7}]^{8}}{(A ∧ B) ∧ (A ∧ B)} ∧IE; 8

is the derivation π_{6}:

\frac{[(A ∧ B^{(9)(6)})^{10}]^{8}[(A ∧ B^{(9)(7)})^{10}]^{8}}{(A ∧ B) ∧ A ∧ B)} ∧IE; 8, 10

and the substitution of π_{2} for the a-class [A ∧ B^{(9)(6),(9)(7)}]^{8} in π_{6} is

\frac{\frac{[A^{s_{1}}]^{8} [B^{t_{1}}]^{8}}{(((A∧B^{(( )(4))((9)(6))})^{5})^{11})^{10}} ∧ IE \frac{[A^{s_{2}}]^{8} [B^{t_{2}}]^{8}}{(((A∧B^{(( )(4))((9)(7))})^{5})^{11})^{10}} ∧ IE}{(A∧B)∧(A∧B)}∧ IE; 8, 10, 11,

where s_{1} = {((1)(4))((9)(6))}, t_{1} = {((2)(4))((9)(6))}, s_{2} = {((1)(4))((9)(7))}, t_{2} = {((2)(4))((9)(7))}.

(2)Logical 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 π_{1}} ; 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 ∀xAx} & & {/At^{a}/ \atop π_{2}} ; C \\ & C \end{aligned} ; (∀EE)  {Aa \atop ∀xAx} (∀IE)

\begin{aligned}{π_{1} \atop ∃xAx} & & {/Aa^{c}/ \atop π_{2}} ; C \\ & C \end{aligned} ; (∃EE)  {At \atop ∃xAx} (∃IE)

⊥-rule: \frac{⊥^{j}}{P} ⊥E, where P is any atomic formula different from ⊥.

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^{o} (see also [18, 2.3.8.(b)]). In N E^{o} (by using the notions above) we can define the proper variable property (PVP) of a derivation π (see [18, 2.5.1.(c)] or [14, p. 28]) which is very similar to PVP in SE^{o}. In the rule (⊃IE) and all elimination rules in the brackets / / there is the a-class which is discharged by that rule if its index is not ∅, and if it is ∅, then nothing is discharged by that rule. Moreover, the other a-classes of the same formula (like the one discharged) may exist, and they are not discharged by that rule. We note that in one rule and the discharged a-class by that rule one number can be written, for example ⊃IE1 and /A^{a}/^{1}, where 1 is not the number of that rule.

Example 2.5. In the system N E^{o} we consider the following derivation π

\frac{\frac{[B^{(8)(7)}]^{3} C^{(9)(7)}}{(B ∧ C^{( )(7)})^{2}}∧IE \frac{\frac{[B^{(5)(4)}]^{3} C^{(6)(4)}}{(B ∧ C^{( )(4)})^{1}}∧IE \frac{\frac{A^{1} /B^{2}/^{2}}{A ∧ B}∧IE /C^{3}/^{1}}{(A∧B)∧C} ∧IE}{(A∧B) ∧C}∧EE_{2}1; 1}{(A∧B)∧C}∧EE_{1}2; 2, 3

where in ∧EE_{2}1; 1: 1 denotes that the discharged a-class by that rule ∧EE_{1} is C^{3}, which is denoted by /C^{3}/^{1}; and 1 denotes that the operation on derivations whose d-formulae have the number 1 is made after that rule, i.e. the substitution with the sb-formula (B ∧ C^{( )(4)})^{1} and 1 is the number of that inference rule ∧EE_{2}1; 1. In ∧EE_{1}2; 2, 3: 2 denotes that the discharged a-class by that rule is /B^{2}/^{2}; 2 denotes that the substitution with the sb-formula (B ∧ C^{( )(7)})^{2} is made after that rule; 3 denotes that the contraction of the a-classes B^{(5)(4)} and B^{(8)(7)} is made after the substitution with number 2; and 2 and 3 are the numbers of that inference rule.

Remark 2.1. If in the system N E^{o} we have the derivations which are of the same form, their indexed d-formulae have different indices, but there is a bijection between the indices of the corresponding d-formulae, then we do not make distinction between these derivations.

In the system N E^{o} 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 [14]. For example, A ∨ B is the major premiss and the d-formulae C are minor premisses of the rule (∨EE).

2.3. The maps which connect derivations of SE^{o} and N E^{o}. We will present two maps which connect the set of derivations of the systems SE^{o} and N E^{o}, the sets Der(SE^{o}) and Der(N E^{o}), respectively. Both maps will be defined by induction on the length of the derivation, where the lengths of derivations D and π will be defined in the usual way, as the number of all rules in these derivations.

The map ψ: Der(SE^{o}) ⟶ Der(N E^{o}) is in fact the map ψ from [3] and it has the property that the image of a derivation D with the end sequent Γ → C is the derivation ψD of the formula C from the set of a-classes Γ:

ψ (\begin{matrix}D \\ Γ → C \end{matrix}) = \begin{matrix}Γ \\ ψD \\ C \end{matrix}

where Γ from Γ → C is the set of indexed formulae and Γ from ψD is the set of a-classes and each d-formula D^{d} from Γ of Γ → C has the corresponding a-class D^{d} of d-formulae from Γ of the derivation ψD. There are several cases which depend on the last rule of the derivation D, rD.

D ψD C^{i} → C C^{i}

⊥^{i} → P {⊥^{i} \atop P} ⊥E

\frac{{D′ \atop Γ → A} {D′′ \atop A^{a}, Δ → C}}{Γ^{×a}, Δ → C} cut  {Δ {Γ^{×a} \atop ψD′} ; (A^{a})^{n} \atop ψD′′} ; C
where n>max(NψD′,NψD′′).

\frac{{D′ \atop A^{a}, A^{b}, Γ → C}}{A^{a∪b}, Γ → C} contraction  {[A^{a}]^{n}[A^{b}]^{n}Γ \atop ψD′} ; C
where n>NψD′.

\frac{{D′ \atop /A^{a}/, Γ → B}}{Γ → A ⊃ B} ⊃R  {/A^{a}/Γ \atop ψD′} ; B ; A ⊃ B ⊃IE

\frac{{D′ \atop Γ → A} {D′′ \atop /B^{b}/, Δ → C}}{Γ, A ⊃ B^{i}, Δ → C} ⊃L  \begin{aligned}A ⊃ B^{i} & {Γ \atop ψD′} ; A & {/B^{b}/Δ \atop ψD′′} ; C \\ & C \end{aligned} ; ⊃EE

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

\frac{{D′ \atop /A^{a}/, Γ → C}}{A ∧ B^{i}, Γ → C} ∧L_{1}  \begin{aligned}A ∧ B^{i} & & {/A^{a}/Γ \atop ψD′} ; C \\ & C \end{aligned} ; ∧EE_{1}

The cases when rD is ∧L_{2}, ∀L and ∃L are similar to the case when rD is ∧L_{1}.

\frac{{D′ \atop Γ → A}}{Γ → A ∨ B} ∨R_{1}  {Γ \atop ψD′} ; A ; A ∨ B ∨IE_{1}

The cases when rD is ∨R_{2}, ∀R and ∃R are similar to the case when rD is ∨R_{1}.

\frac{{D′ \atop /A^{a}/, Γ → C} {D′′ \atop /B^{b}/, Δ → C}}{A ∨ B^{i}, Γ, Δ → C} ∨L  \begin{aligned}A ∨ B^{i} & {/A^{a}/Γ \atop ψD′} ; C & {/B^{b}/Δ \atop ψD′′} ; C \\ & C \end{aligned} ; ∨EE

Now we define the map ϕ: Der(N E^{o}) ⟶ Der(SE^{o}), which has the property that the image of a derivation of C from the set of a-classes Γ is the derivation with the end sequent Γ → C:

ϕ (\begin{matrix}Γ \\ π \\ C \end{matrix}) = \begin{matrix}ϕπ \\ Γ → C \end{matrix}

where for each a-class D^{d} from Γ of the derivation Γ π ; C from N E^{o} there is the corre-

sponding d-formula D^{d′} in Γ from its ϕ-image, \begin{matrix}ϕπ \\ Γ→C \end{matrix}, and there is a bijection from d to d′, i.e. each symbol s from d has the corresponding symbol s′ in d′, where s′ is (… ((s)(t_{1})) …)(t_{m}), m ⩾ 0 (see the definition below when π ends with an elimination rule). There are several cases which depend on the last rule of π, rπ, where the last rule of π is its last inference rule when it does not have any number; or the contraction or the substitution whose d-formulae have the largest the number of the last inference rule of π, i.e. Nπ.

If the last inference rule of π does not have any number, then π and ϕπ are

π ϕπ C^{i} C^{i} → C

{⊥^{i} \atop P} ⊥E ⊥^{i} → P

{/A^{a}/Γ \atop π′} ; B ; A ⊃ B ⊃IE \frac{{ϕπ′ \atop /A^{a′}/, Γ → B}}{Γ → A ⊃ B} ⊃R

\begin{aligned}{Γ \atop π′} ; A ⊃ B & {Δ \atop π′′} ; A & {/B^{b}/Λ \atop π′′′} ; C \\ & C \end{aligned} ; ⊃EE  \frac{{ϕπ′ \atop Γ → A ⊃ B} \frac{{ϕπ′′ \atop Δ → A} {ϕπ′′′ \atop /B^{b′}/, Λ → C}}{Δ, A ⊃ B^{i}, Λ → C} ⊃L}{Γ^{×i}, Δ, Λ → C} cut

\begin{matrix}{Γ \atop π′} ; A & {Δ \atop π′′} ; B \\ A ∧ B \end{matrix} ∧IE  \frac{{ϕπ′ \atop Γ → A}  {ϕπ′′ \atop Δ → B}}{Γ, Δ → A ∧ B} ∧R

\begin{aligned}{Γ \atop π′} ; A ∧ B & & {/A^{a}/Δ \atop π′′} ; C \\ & C \end{aligned} ; ∧EE_{1}  \frac{{ϕπ′ \atop Γ → A ∧ B} \frac{{ϕπ′′ \atop /A^{a′}/, Δ → C}}{A ∧ B^{i}, Δ → C} ∧L_{1}}{Γ^{×i}, Δ → C} cut

The case when rπ is ∧EE_{2} is similar to the case when rπ is ∧EE_{1}.

{Γ \atop π′} ; A ; A ∨ B ∨IE_{1} \frac{{ϕπ′ \atop Γ → A}}{Γ → A ∨ B} ∨R_{1}

The case when rπ is ∨IE_{2} is similar to the case when rπ is ∨IE_{1}.

\begin{aligned}{Γ \atop π′} ; A ∨ B & {/A^{a}/Δ \atop π′′} ; C & {/B^{b}/Λ \atop π′′′} ; C \\ & C \end{aligned} ; ∨EE  \frac{{ϕπ′ \atop Γ → A ∨ B} \frac{{ϕπ′′ \atop /A^{a′}/, Δ → C} {ϕπ′′′ \atop /B^{b′}/, Λ → C}}{A ∨ B^{i}, Δ, Λ → C} ∨L}{Γ^{×i}, Δ, Λ → C} cut

The case when rπ is ∀IE is similar to the case when rπ is ∨IE_{1}.

\begin{aligned}{Γ \atop π′} ; ∀xAx & & {/At^{a}/Δ \atop π′′} ; C \\ & C \end{aligned} ; ∀EE  \frac{{ϕπ′ \atop Γ → ∀xAx} \frac{{ϕπ′′ \atop /At^{a′}/, Δ → C}}{∀xAx^{i}, Δ → C} ∀L}{Γ^{×i}, Δ → C} cut

The case when rπ is ∃IE is similar to the case when rπ is ∨IE_{1}.

\begin{aligned}{Γ \atop π′} ; ∃xAx & & {/Ab^{a}/Δ \atop π′′} ; C \\ & C \end{aligned} ; ∃EE  \frac{{ϕπ′ \atop Γ → ∃xF x} \frac{{ϕπ′′ \atop /Ab^{a′}/, Δ → C}}{∃xAx^{i}, Δ → C} ∃L}{Γ^{×i}, Δ → C} cut

If the last inference rule of π has numbers, n is the largest of its numbers, and − n is the number of the d-formulae of one contraction, i.e. π is the result of a contraction in a derivation π′, then π and ϕπ are

{Γ[A^{a}]^{n}[A^{b}]^{n} \atop π′} ; C  and  ^{\frac{{ϕπ′ \atop A^{a′}, A^{b′}, Γ → C}}{A^{a′∪b′}, Γ → C}} contraction;

− n is the number of the d-formulae of one substitution, i.e. π is the result of a

substitution of {Δ \atop π′} ; A in {Γ, A^{a} \atop π′′} ; C, then π and ϕπ are

{Γ {Δ^{×a} \atop π′} ; (A^{a})^{n} \atop π′′} ; C  and  ^{\frac{{ϕπ′ \atop Δ → A} {ϕπ′′ \atop A^{a′}, Γ → C}}{Δ^{×a′}, Γ → C}} cut.

Remark 2.2. We consider a derivation D of the system SE^{o} and its ψ-image, the derivation ψD = π, in the system N E^{o}. By the definition of the map ψ, if the major premiss of one elimination rule of π is the sb-formula ⟨(∥A^{(s)(t)}∥)^{n}⟩, then its full-form is [… [[(… (((… (A^{(s)(t)})^{k^{1}} …)^{k^{k}})^{n})^{n^{1}} …)^{n^{n}}]^{l^{1}}] …]^{l^{l}} (∗) where n, k, l ⩾ 0, s may not exist and n>max(k_{1}, …, k_{k}, n_{1}, …, n_{n}, l_{1}, …, l_{l}), when one of n, k and l is not 0.

Now, for a derivation π of the system N E^{o} we define the derivation π^{−}. If π is a trivial derivation C^{i}, then π^{−} is π. If π is

(∗_{1}) \begin{matrix}Γ \\ π_{1} \\ \frac{A}{C} & r \end{matrix},  (∗_{2}) \frac{\begin{matrix}Γ & Δ \\ π_{1} & π_{2} \\ A & C \end{matrix}}{C} r  or  (∗_{3}) \frac{\begin{matrix}Γ & Δ & Λ \\ π_{1} & π_{2} & π_{3} \\ A & B & C \end{matrix}}{C} r

and the last rule of the derivation π is (1.1) one substitution with only one sbformula, the sb-formula ⟨(∥A^{(s)(t)}∥)^{n}⟩, which is the major premiss of r and r is an elimination rule, i.e. π is (∗_{2}) or (∗_{3}), A is the sb-formula whose full-form is (∗) from Remark 2.2, and its number n is the largest number of r, then π^{−} is

\frac{\begin{matrix}Γ & Δ \\ π_{1}^{−} & π_{2}^{−} \\ A^{−} & C \end{matrix}}{C} r  or  \frac{\begin{matrix}Γ & Δ & Λ \\ π_{1}^{−} & π_{2}^{−} & π_{3}^{−} \\ A^{−} & B & C \end{matrix}}{C} r,

where A^{−} is either ⟨(∥A^{(s)(t^{−})}∥)^{n}⟩ without ( )^{n^{1}}, when n > 0 (or ⟨∥A^{(s)(t^{−})}∥⟩, when n = 0), and in the rule whose number is n_{1} (or n) that number is deleted, t is replaced by t^{−} in all d-formulae of the subderivations of π^{−}; (1.2) one contraction, one substitution which not the substitution from (1.1) or the rule r, then π^{−} is

\begin{matrix}Γ \\ π_{1}^{−} \\ \frac{A}{C} & r \end{matrix},  \frac{\begin{matrix}Γ & Δ \\ π_{1}^{−} & π_{2}^{−} \\ A & C \end{matrix}}{C} r  or  \frac{\begin{matrix}Γ & Δ & Λ \\ π_{1}^{−} & π_{2}^{−} & π_{3}^{−} \\ A & B & C \end{matrix}}{C} r,

respectively.

Theorem 2.1. In N E^{o} for each derivation π and its ψ ∘ ϕ-image π_{1}: π_{1}^{−} is π.

Proof. By an induction on the length of a derivation π from the system N E^{o}. There are several cases according to the last rule of π. We only consider the case when the last rule of π is ⊃EE without numbers, and the other cases are similar. In that case π is

\begin{aligned}{Γ \atop π′} ; A ⊃ B & {Δ \atop π′′} ; A & {/B^{b}/^{1}Λ \atop π′′′} ; C \\ & C \end{aligned} ; ⊃EE1, its ϕ-image is ^{\frac{{ϕπ′ \atop Γ→ A⊃B} \frac{{ϕπ′′ \atop Δ→ A} {ϕπ′′′ \atop /B^{b′}/, Λ→ C}}{Δ, A ⊃ B^{i}, Λ→ C} ⊃L}{Γ^{×i}, Δ, Λ→ C}} cut,

where for each a-class D^{d} from Γ, Δ, Λ in the derivation π and the corresponding d-formula D^{d′} from Γ^{×i}, Δ, Λ in the last sequent of ϕπ the following holds: there is a bijection between symbols from d and d′, i.e. each symbol s from d has the corresponding symbol s′ in d′, where s′ is (… ((s)(t_{1})) …)(t_{m}), m ⩾ 0.

Next, the ψ-image of the derivation ϕπ is

\frac{\begin{matrix}Γ^{×i} & Δ & /B^{b′}/^{1}Λ \\ ψϕπ′ & ψϕπ′′ & ψϕπ′′′ \\ (A ⊃ B^{i})^{n} & A & C \end{matrix}}{C} ⊃EE1; n,

where n > max(Nψϕπ′, Nψϕπ′′, Nψϕπ′′′). By the induction hypothesis, (ψϕπ′)^{−} is π′, (ψϕπ′′)^{−} is π′′ and (ψϕπ′′′)^{−} is π′′′. The derivation (ψϕπ)^{−} is obtained from ψϕπ when, ψϕπ′, ψϕπ′′, ψϕπ′′′ are replaced by (ψϕπ′)^{−}, (ψϕπ′′)^{−}, (ψϕπ′′′)^{−}, respectively, (A⊃B^{i})^{n} is replaced by A⊃B, i is deleted in the d-formulae from Γ^{×i} and n is deleted in EE1; n. Finally, by the Remark 2.1, (ψϕπ)^{−} is π. □

3. Conversions in the systems SE^{o} and N E^{o}

3.1. Conversions in the system SE^{o}. The conversions of derivations in the system SE^{o}, the pm^{E}-conversions, are in fact conversions of derivations of the system δE from [3]. Almost all of them are the transformations from Gentzen’s proof of Hauptsatz in [6]. The characteristic of the pm^{E}-conversions is that they can be applied on a derivation D of the following form

\frac{\begin{matrix}D′ \\ Γ → A \end{matrix}  \begin{matrix}D′′ \\ A^{a}, Δ → B \end{matrix}}{Γ^{×a}, Δ → B} cut

where subderivations D′ and D′′ do not contain any cut rule. The degree d, the left rank lr, the right rank rr and the rank r of the derivation D above are the well-known Gentzen’s notions (see, for example, [3]).

There are three kinds of pm^{E}-conversions: p^{E}-conversions, mf^{E}-conversions and ms^{E}-conversions. In each conversion below its redex will be the derivation D and its contractum will be the derivation C. If we have, for example, that the conversion (1 < lr ↗ rr−c_{r} > 1)^{E} is applied on the derivation D above, then 1 < lr means that the left rank of D is greater than 1, thus the last rule of D′ is either a contraction or a left rule; rr − c_{r} > 1 means that D′′ ends with several contractions of the cut formula A and the principal formula of the first rule above these contractions, i.e. the rule r, is not any of the contracted formulae (rr − c = 1, otherwise); ↗ means that by that conversion the cut and the contractions are permuted with that rule r. If a contractum C has two (or three) subderivations of the same form we will suppose that the indices of their formulae are different. More precisely, the end sequents of two of these subderivations of C will be denoted, for example, by Γ^{e} → C and Γ^{e′} → C which will mean that there is a bijection between Γ^{e} and Γ^{e′} (i.e. Γ^{e} ≃ Γ^{e′}). (See [3, Section 5.1] for details.) A^{a_{1}^{m}} will denote the sequence A^{a_{1}}, …, A^{a_{m}}, m⩾1. The rule c … with A^{a_{1}^{m}} in its upper sequent and A^{a} in its lower sequent will mean m − 1 contractions of formulae from A^{a_{1}^{m}}, where a is a_{1} ∪ ... ∪ a_{m} (m ⩾ 1); otherwise it will mean several contractions of formulae which are not emphasized. Finally, Γ^{×a} and Γ^{e×a} will denote the same set of indexed formulae.

p^{E}-conversions. The p^{E}-conversions consist of the following four kinds of conversions:

(Is)^{E}, (1 ⩽ lr↗ rr_{r} >1)^{E}, (1 ⩽ lr ↗ rr−c_{r} > 1)^{E} and (1 ⩽ lr ↗ rr−c_{r} = 1)^{E}, where the rule r cannot be a cut rule.

▷I◁ (Is)^{E} Conversions (Is)^{E} will be conversions (Is) from [3], when at list one of the subderivation D′ or D′′ of D is an initial sequent (i.e. Zucker’s trivial cut, see [18, p. 40]).

▷II◁ (1 ⩽ lr ↗ rr > 1)^{E} In the redex the last rule of the subderivation D′′ is either a right rule; or a left rule or a contraction whose principal formula is not the cut formula A^{a}. We present, as one example, the case when rD′′ is ∨L.

(1 ⩽ lr ↗ rr_{∨L} > 1)^{E} The derivations D and C are

\frac{\begin{matrix}D′ \\ Γ → A \end{matrix} \frac{\begin{matrix}D′′_{1} & D′′_{2} \\ A^{a}, /C^{c}/, Δ′ → B & /D^{d}/, Δ′′ → B \end{matrix}}{C ∨ D^{i}, A^{a}, Δ′, Δ′′ → B} ∨ L}{C ∨ D^{i}, Γ^{×a}, Δ′, Δ′′ → B} cut

\frac{\frac{\begin{matrix}D′ & D′′_{1} \\ Γ → A & A^{a}, /C^{c}/, Δ′ → B \end{matrix}}{Γ^{×a}, /C^{c}/, Δ′ → B} cut \begin{matrix}D′′_{2} \\ /D^{d}/, Δ′′ → B \end{matrix}}{C ∨ D^{i}, Γ^{×a}, Δ′, Δ′′ → B} ∨ L

▷III◁ (1 ⩽ lr ↗ rr −c > 1)^{E} In the redex the subderivation D′′ ends with n−1 contractions of the formulae A (n ⩾ 2) and the principal formula of the first rule above these contractions is not any of the contracted formulae. We only present the case when the rule above the contractions is ⊃L.

(1 ⩽ lr ↗ rr − c_{⊃L} > 1)^{E} The derivation D is

\frac{{D′ \atop Γ → A} \frac{\frac{{D′′_{1} \atop A^{a_{1}^{k}} , Δ′ → C} {D′′_{2} \atop /D^{d}/, A^{a_{k+1}^{n}}, Δ′′ → B}}{C ⊃ D^{i}, A^{a_{1}^{n}}, Δ′, Δ′′ → B} ⊃ L}{C ⊃ D^{i}, A^{a}, Δ′, Δ′′ → B} c …}{C ⊃ D^{i}, Γ^{×a}, Δ′, Δ′′ → B} cut

where a is a_{1} ∪ ... ∪ a_{n} and the end sequents of D′′_{1} and D′′_{2} contain the formulae from A^{a}, i.e. 1 ⩽ k ⩽ n − 1 in D. The derivation C is

\frac{\frac{\frac{{D′ \atop Γ^{c} → A} \frac{{D′′_{1} \atop A^{a_{1}^{k}} , Δ′ → C}}{A^{a′}, Δ′ → C} c …}{Γ^{c×a′}, Δ′ → C} cut  \frac{{D′ \atop Γ^{c′} → A} \frac{{D′′_{2} \atop /D^{d}/, A^{a_{k+1}^{n}}, Δ′′ → B}}{/D^{d}/, A^{a′′}, Δ′′ → B} c …}{/D^{d}/, Γ^{c′×a′′}, Δ′′ → B} cut}{C ⊃ D^{i}, Γ^{c′×a′′}, Γ^{c×a′}, Δ′, Δ′′ → B} ⊃L}{C ⊃ D^{i}, Γ^{b}, Δ′, Δ′′ → B} c …

where a′ is a_{1}∪...∪a_{k}, a′′ is a_{k+1}∪...∪a_{n} and Γ^{b} is Γ^{c×a′∪c′×a′′} ≃ Γ^{c×(a′∪a′′)} ≃ Γ^{c×a} (see [18, Note on p. 40]). If the end sequent of D′′_{1} or D′′_{2} does not contain any formula from A^{a}, then the contractum is the derivation C above, where its subderivation which ends with the sequent Γ^{c×a′}, Δ′→C is replaced by D′′_{1} or its subderivation which ends with /D^{d}/, Γ^{c′×a′′}, Δ′′ → B is replaced by D′′_{2}, respectively.

In the conversions below the indexed formulae of the end sequent of the contractum C will not be explained in details as in the case above. We will assume that these formulae are obtained by using (oi): operations on indices.

▷IV◁ (1 ⩽ lr ↗ rr − c = 1)^{E} In the redex D′′ ends with n − 1 contractions of A (n ⩾ 2) and the principal formula of the first rule above these contractions is one of the contracted formulae. We present the case when that rule is ∧L_{1}.

(1 ⩽ lr ↗ rr − c_{∧L_{1}} = 1)^{E} The derivation D is

\frac{{D′ \atop Γ → C ∧ D}  \frac{\frac{{D′′_{1} \atop /C^{b}/, C ∧ D^{a_{2}^{n}}, Δ → B}}{C ∧ D^{i}, C ∧ D^{a_{2}^{n}}, Δ → B} ∧ L_{1}}{C ∧ D^{a}, Δ → B} c …}{Γ^{×a}, Δ → B} cut

where the principal formula of ∧L_{1} has, for example, the index a_{1}, i.e. i is a_{1} (but, we note that each a_{l}, 1 ⩽ l ⩽ n, can be the index i), and a is a_{1} ∪ ... ∪ a_{n}. The derivation C (when b ≠ ∅) is

\frac{\frac{{D′ \atop Γ^{e′} → C ∧ D} \frac{\frac{{D′ \atop Γ^{e} → C ∧ D} \frac{{D′′_{1} \atop /C^{b}/, C ∧ D^{a_{2}^{n}}, Δ → B}}{/C^{b}/, C ∧ D^{a′}, Δ → B} c …}{Γ^{e×a′}, /C^{b}/, Δ → B} cut}{Γ^{e×a′}, C ∧ D^{i}, Δ → B} ∧ L_{1}}{Γ^{e×a′}, Γ^{e′×i}, Δ → B} cut}{Γ, Δ → B} c …

where a′ is a_{2} ∪ ... ∪ a_{n} and Γ, Δ → B is obtained by using (oi). If b is ∅, then the contractum is only the subderivation of C above, which ends with the upper cut.

m^{E}-conversions consists of mf^{E}-conversions and ms^{E}-conversions.

mf^{E}-conversions. The mf^{E}-conversions consist of two kinds of conversions: (1 = lr ↔ rr = 1)^{E} and (1 = lr ↔ rr − c = 1)^{E}. In all mf^{E}-conversions of the first kind the left and the right rank of the redex are 1.

▷V◁ (1 = lr ↔ rr = 1)^{E} In the redex the subderivations D′ and D′′ end with rules whose principal formulae are the cut formulae. We present the case when the cut formula is C ⊃ D.

(1 = lr_{⊃} ↔ rr_{⊃} = 1)^{E} The derivations D and C (when c and d are not ∅) are

\frac{\frac{{D′_{1} \atop /C^{c}/, Γ → D}}{Γ → C ⊃ D} ⊃ R \frac{{D′′_{1} \atop Δ′ → C} {D′′_{2} \atop /D^{d}/, Δ′′ → B}}{C ⊃ D^{i}, Δ′, Δ′′ → B} ⊃ L}{Γ^{×i}, Δ′, Δ′′ → B} cut

\frac{\frac{{D′′_{1} \atop Δ′^{f} → C} {D′_{1} \atop /C^{c}/, Γ → D}}{Δ′^{f×c}, Γ → D} cut  {D′′_{2} \atop /D^{d}/, Δ′′ → B}}{Δ′^{f×c×d}, Γ^{×d}, Δ′′ → B} cut

If c = ∅ and d ≠ ∅, then C is ^{\frac{\begin{matrix}D′_{1} & D′′_{2} \\ Γ→D & /D^{d}/,Δ′′→B \end{matrix}}{Γ^{×d},Δ′′→B}} cut, and similarly when c ≠ ∅ and d = ∅. If c = d = ∅, then C is D′′_{2}.

▷VI◁ (1 = lr ↔ rr − c = 1)^{E} In the redex the subderivation D′ ends with a right rule i.e. its principal formula is the cut formula and the derivation D′′ ends with n − 1 contractions of the formulae A (n ⩾ 2) where the principal formula of the first rule above these contractions is one of the contracted formulae. We present the case when the cut formula is C ⊃ D.

(1 = lr_{⊃} ↔ rr − c_{⊃} = 1)^{E} The derivation D is

\frac{\frac{{D′_{1} \atop /C^{c}/, Γ → D}}{Γ → C ⊃ D} ⊃ R  \frac{\frac{{D′′_{1} \atop C ⊃ D^{a_{1}^{k−1}}, Δ′ → C} {D′′_{2} \atop /D^{d}/, C ⊃ D^{a_{k+1}^{n}}, Δ′′ → B}}{C ⊃ D^{i}, C ⊃ D^{a_{1}^{k−1}}, C ⊃ D^{a_{k+1}^{n}}, Δ′, Δ′′ → B} ⊃ L}{C ⊃ D^{a}, Δ′, Δ′′ → B} c…}{Γ^{×a}, Δ′, Δ′′ → B} cut

where the principal formula of the rule ⊃L has, for example, the index a_{k}, i.e. i is a_{k}, (but, we note that each a_{l}, 1 ⩽ l ⩽ n, can be the index i) and the end sequents of D′′_{1} and D′′_{2} contain formulae from A^{a}, i.e. 2 ⩽ k ⩽ n − 1, and a is a_{1} ∪ ... ∪ a_{n}. The derivation C (when c ≠ ∅ and d ≠ ∅) is

\frac{\frac{\frac{\frac{\frac{{D′_{1} \atop /C^{c}/, Γ^{f}→D}}{Γ^{f}→C⊃D} \frac{{D′′_{1} \atop C⊃D^{a{k−1 \atop 1}} , Δ′ →C}}{C⊃D^{a′}, Δ′ →C} c…}{Γ^{f×a′}, Δ′ →C} cut {D′_{1} \atop /C^{c′}/, Γ^{f′}→D}}{Γ^{f×a′×c′} , Δ^{′×c′}, Γ^{f′}→D} cut \frac{\frac{{D′_{1} \atop /C^{c′′}/, Γ^{f′′}→D}}{Γ^{f′′}→C⊃D} \frac{{D′′_{2} \atop /D^{d}/, C⊃D^{a{n \atop k+1}}, Δ′′ →B}}{/D^{d}/, C⊃D^{a′′}, Δ′′ →B} c…}{/D^{d}/, Γ^{f′′×a′′} , Δ′′ →B} cut}{Γ^{f×a′×c′×d}, Γ^{f′′×a′′} , Γ^{f′×d} , Δ^{′×c′×d} , Δ′′ →B} cut}{Γ^{b}, Δ′, Δ′′ →B} c...

where a′ is a_{1}∪...∪a_{k−1}, a′′ is a_{k+1}∪...∪a_{n} and Γ^{b}, Δ′, Δ′′ → B is obtained by using (oi). If the end sequent of D′′_{1} or D′′_{2} does not contain any formula from C⊃D^{a}, then the contractum is C above, where its subderivation which ends with Γ^{f×a′}, Δ′→C is replaced by D′′_{1}, or its subderivation which ends with /D^{d}/, Γ^{f′′×a′′}, Δ′′ → B is replaced by D′′_{2}, respectively. If c is ∅, then the contractum is the derivation C above, where its subderivation which ends with Γ^{f×a′×c′}, Δ^{′×c′}, Γ^{f′} → D is replaced by D′_{1}. If d is ∅, then the contractum is the subderivation of the derivation C above, which ends with /D^{d}/, Γ^{f′′×a′′}, Δ′′ → B without /D^{d}/.

ms^{E}-conversions. The ms^{E}-conversions are (1 < lr ↖ rr = 1)^{E} conversions. In all ms^{E}-conversions the right rank of the redex is 1 and its left rank is greater than 1.

▷VII◁ (1 < lr ↖ rr = 1)^{E} In the redex the last rule of derivation D′ is a left rule or a contraction, and the last rule of D′′ is a left rule whose principal formula is the cut formula. We only present the case when the rule rD′ is ∃L and the cut formula A is C ∧ D.

(1 < lr_{∃} ↖ rr_{∧} = 1)^{E} The derivation D is

\frac{\frac{{D′_{1} \atop /F a^{c}/, Γ′ → C ∧ D}}{∃xF x^{j}, Γ′ → C ∧ D} ∃L  \frac{{D′′_{1} \atop /C^{b}/, Δ → B}}{C ∧ D^{i}, Δ → B} ∧ L_{1}}{∃xF x^{j×i}, Γ′^{×i}, Δ → B} cut

and the derivation C is

\frac{\frac{{D′_{1} \atop /F a^{c}/, Γ′ → C ∧ D} \frac{{D′′_{1} \atop /C^{b}/, Δ → B}}{C ∧ D^{i}, Δ → B} ∧ L_{1}}{/F a^{c×i}/, Γ′^{×i}, Δ → B} cut}{∃xF x^{j}, Γ′^{×i}, Δ → B} ∃L

An arbitrary derivation F, whose one subderivation is the redex of one conversion above, will be converted into a derivation F′ by replacing D (in F) with the contractum of that conversion, the derivation C, by using the operation pruning^{E} defined in [3], which is completely analogous to the definition of the operation pruning in [18, 3.1.5 and 7.8.3 ]. Then we define

F p^{E}-conv F′, F mf^{E}-conv F′ or F ms^{E}-conv F′ iff F′ is obtained from F by replacing one its subderivation D, which is the redex of a p^{E}-conversion, mf^{E}- conversion or ms^{E}-conversion respectively, with the contractum of that conversion, and the corresponding pruning^{E} is applied on the part of F below D. Moreover, the right cut formula of the last cut in D will be the d-formula of that conversion.

F m^{E}-conv F′ iff either F mf^{E}-conv F′ or F ms^{E}-conv F′.

A derivation F pm^{E}-converts into a derivation F′ iff there is a sequence of derivations, F_{0}, …, F_{n}, n ⩾ 0, such that F_{0} is F, F_{n} is F′, and for all i < n (when n > 0) either F_{i} p^{E}-conv F_{i+1} or F_{i} m^{E}-conv F_{i+1}.

If a derivation F does not have any cut rule, then F will be called a cut-free derivation in the system SE^{o}.

3.2. Conversions in the system N E^{o}. We will define the conversions in the system N E^{o}, which are the conversions in the system N E presented in [3] with indices of formulae, and numbers of some formulae and inference rules. In the system N E^{o} all elimination rules make maximum segments of several formulae i.e. there are special conversions of derivations from N E^{o} which do not exist for derivations from Gentzen’s system NJ. Each conversion will have the redex, the derivation π, and the contractum, the derivation \overline{π}. In fact, we will consider the derivations with subderavations π and \overline{π}, respectively (see (cn) below).

▽ (Emaxf-conversions) These conversions are used to eliminate a maximum formula in a derivation of the system N E^{o}.

(E∨_{1}-convn) The redex, the derivation π, is

\begin{aligned}{Γ \atop π_{1}} ; C ; (C ∨ D)^{k} ^{∨IE^{1}} & {/C^{c}/Δ′ \atop π_{2}} ; (B)^{l} & {/D^{d}/Δ′′ \atop π_{3}} ; (B)^{m} \\ & B \end{aligned} ; ∨EE

and C ∨ D is a maximum formula of π, where k, l and m may not exist. We present (E∨_{1}-convn) in the full form. The derivation π is the subderivation of π′

{[E^{a_{1}}]_{...}^{l}/F^{b_{1}}/_{...}^{∗}Γ_{1} \atop π_{1}} ; C ; (C ∨ D)^{k} ; ∨IE_{1}  {/C^{c}/[E^{a_{2}}]_{...}^{l}/F^{b_{2}}/_{...}^{∗}Δ′_{1} \atop π_{2}} ; (B)^{l}  {/D^{d}/[E^{a_{3}}]_{...}^{l}/F^{b_{3}}/_{...}^{∗}Δ′′_{1} \atop π_{3}} ; (B)^{m} (B)^{i} ∨EE[E^{a_{4}}]_{...}^{l}/F^{b_{4}}/_{...}^{∗}Φ
π_{4}
H

Γ is [E^{a_{1}}]_{...}^{l}/F^{b_{1}}/_{...}^{∗}Γ_{1}; Δ′ is [E^{a_{2}}]_{...}^{l}/F^{b_{2}}/_{...}^{∗}Δ′_{1}; Δ′′ is [E^{a_{3}}]_{...}^{l}/F^{b_{3}}/_{...}^{∗}Δ′′_{1}, where in π_{i}, 1 ⩽ i ⩽ 4: [E^{a_{i}}]^{l} denotes the part of one a-class which is made by the contraction whose number is l and … denotes the parts of a-classes which are made by all contractions of that kind; /F^{b_{i}}/^{∗} denotes the part of one a-class which is the discharged a-class by one rule from π_{4} and … denotes the parts of all a-classes of that kind. The rule ∨IE_{1} can have several numbers, which appear: 1-1 only in π_{1}; the rule ∨EE can have several numbers which appear: 2-1 only in π_{1}, 2-2 only in π_{2}, 2-3 only in π_{3}, 2-12 in π_{1} and π_{2}, 2-13 in π_{1} and π_{3}, 2-23 in π_{2} and π_{3}, 3-123 in π_{1}, π_{2} and π_{3}; the numbers k, l and m, when they exist, can be the numbers either of ∨EE or of one rule from π_{4}; and i can be the number of one rule from π_{4}.

The contractum π̄ has different forms in the cases when c ≠ ∅ and c = ∅. If the number k (l) exists and the number of the sb-formulae with that number is greater than 1, then π′_{1} (π′_{2}) below is π_{1} (π_{2}) without the contraction whose number is the c-number of the sb-formula whose number is k (l) and without each contraction whose number is greater than that number.

If c ≠ ∅, then π̄ is the subderivation

{{Γ^{×c} \atop π′_{1}} ; (C^{c})^{n^{2}}[E^{a_{2}}]^{l′′} … /F^{b_{2}}/^{∗} … Δ′_{1} \atop π′_{2}} ; B

in π′′:

{{[E^{a_{1}×c}]^{l′′} … /F^{b_{1}×c}/^{∗} … Γ_{1}^{×c} \atop π′_{1}} ; (C^{c})^{n^{2}}[E^{a_{2}}]^{l′′} … /F^{b_{2}}/^{∗} … Δ′_{1} \atop π′_{2}} ; (B)^{n^{1}} [E^{a_{4}}]^{l′′} … /F^{b_{4}}/^{∗} … Φ

π_{4}

H

where: (1) [E^{a_{1}×c}]^{l′′}, [E^{a_{2}}]^{l′′} and [E^{a_{4}}]^{l′′} denote the parts of one a-class which is made by the contraction whose number is the number of one rule in π_{4} and … denotes the a-classes which are made by all contractions of that kind; (2) /F^{b_{1}×c}/^{∗} /F^{b_{2}}/^{∗} and /F^{b_{4}}/^{∗} denote the parts of one a-class which is the discharged a-class by one rule from the derivation π_{4}, and … denotes all a-classes of that kind; (3) n_{1} is j̄+ 1 and n_{2} is j̄+ 2, where j̄ is the number of a rule r from π_{4} in π′ which is the smallest of all numbers of the rules from π_{4} in π′, and n_{1} and now n_{2} are the numbers of r fom π_{4} in π′′, (3.1) in π′′ there are j, j ⩾ 0, contractions of top-formulae from π′_{1}, π′_{2} and π_{4} whose corresponding top-formulae from the subderivations π_{1}, π_{2} and π_{4} of π′ have the c-number of the sub-formulae whose numbers are k and l, and their numbers are the numbers of r, so if j′′ is the corresponding number of a number j′ from π_{4} in π′ and (3.1.1) j′ ⩾ j̄, then j′′ = j′ + j + 2; (3.1.2) j′ < j̄, then j′′ = j′.

If c = ∅, then \overline{π} is the subderivation \begin{matrix}[E^{a_{2}} ]^{l}.../F^{b_{2}} /^{∗}...Δ′_{1} \\ π′_{2} \\ B \end{matrix} in the derivation π′′:

{{[E^{a_{2}}]^{l′′} … /F^{b_{2}}/^{∗} … Δ′_{1} \atop π′_{2}} ; (B)^{n^{1}} [E^{a_{4}}]^{l′′} … /F^{b_{4}}/^{∗} … Φ \atop π_{4}} ; H

where n_{1} and numbers in π_{4} from π′′ are obtained as in the case when c ≠ ∅. (cn): If in the derivation π there are some a-classes which are contracted (they may be discharged a-classes of some rules), and they appear in π̄, then these a-classes are contracted in the derivation π̄, too.

(E∨_{2}-convn) Similarly to (E∨_{1}-convn).

The other Emaxf-conversions and all Emaxs-conversions below will not be presented in the full form, but we will assume that in each of them (cn) holds and the derivation which contains its contractum will be obtained similarly as in the case (E∨_{1}-convn).

(E∧_{1}-convn) The redex, the derivation π, is

\begin{matrix}\begin{matrix}{Γ \atop π_{1}} ; C & {Δ \atop π_{2}} ; D \\ C ∧ D \end{matrix} ∧IE & {/C^{c}/Λ \atop π_{3}} ; B \\ B \end{matrix} ; ∧EE_{1}

where C∧D is a maximum formula of π. The contractum \overline{π} has two forms in the cases when c ≠ ∅ and c = ∅:

{{Γ^{×c} \atop π′_{1}} ; (C^{c})^{^{n}^{1}} Λ \atop π′_{3}} ; B  and  {Λ \atop π′_{3}} ; B,  respectively.

(E∧_{2}-convn) Similarly to (E∧_{1}-convn). (E⊃-convn) The redex, the derivation π, is

\begin{aligned}{/C^{c}/Γ \atop π_{1}} ; D ; C ⊃ D ⊃IE & {Δ′ \atop π_{2}} ; C & {/D^{d}/Δ′′ \atop π_{3}} ; B \\ & B \end{aligned} ; ⊃EE

where C⊃D is a maximum formula of π. The contractum π̄ has three forms in the cases when c ≠ ∅, d ≠ ∅; c = ∅, d ≠ ∅; and d = c = ∅:

{{{Δ^{′×c×d} \atop π′_{2}} ; (C^{c})^{^{n}^{2}} Γ^{×d} \atop π′_{1}} ; (D^{d})^{^{n}^{1}}Δ′′ \atop π′_{3}} ; B  {{Γ^{×d} \atop π′_{1}} ; (D^{d})^{^{n}^{1}}, Δ′′ \atop π′_{3}} ; B  and  {Δ′′ \atop π′_{3}} ; B,  respectively.

(E∀-convn) Similarly to (E∧_{1}-convn). (E∃-convn) Similarly to (E∧_{1}-convn). ▽ (Emaxs-conversions). The Emaxs-conversions are used to eliminate maxi-

mum segments (for details see [3, Section 5.3]).

(Emaxs_{∧_{1}}^{∧_{1}}). The redex π and the contractum π̄ are

\begin{matrix}\begin{matrix}{Γ \atop π_{1}} ; (A ∧ B)^{n} & {/A^{a}/Δ \atop π_{2}} ; (C ∧ D)^{l} \\ (C ∧ D)^{m} \end{matrix} ∧EE_{1} & {/C^{c}/Λ \atop π_{3}} ; (G)^{k} \\ G \end{matrix} ∧EE_{1} and \frac{{Γ \atop π_{1}} ; (A ∧ B)^{n′′} \begin{matrix}{/A^{a}/Δ \atop π_{2}} ; (C ∧ D)^{l′′} & {/C^{c}/Λ \atop π_{3}} ; (G)^{k′′} \\ G \end{matrix} ∧EE_{1}}{G} ∧ EE_{1}

where (C ∧ D)^{m} is the last d-formula of one maximum segment, which is defined in the usual way: it is one a sequence of d-formulae F_{1}, …, F_{n} which are of the same form, F_{i+1} is immediately below F_{i}, 1 ⩽ i ⩽ n − 1, F_{1} is the consequence of one introduction rule and F_{n} is the major premiss of one elimination rule. In π: n, k, l and m may not exist; the upper rule ∧EE_{1} can have several numbers, which appear: 1-1 only in π_{1}, 1-2 only in π_{2} or 1-12 in π_{1} and π_{2}, and the numbers n and l when they exist; the lower rule ∧EE_{1} can have several numbers which appear: 2-1 only in π_{1}, 2-2 only in π_{2}, 2-3 only in π_{3}, 2-12 in π_{1} and π_{2}, 2-13 in π_{1} and π_{3}, 2-23 in π_{2} and π_{3}, 3-123 in π_{1}, π_{2} and π_{3}, and the numbers n and l when they exist and they are not numbers of the upper rule ∧EE_{1}, and k and m when they exist. In π̄: the upper rule ∧EE_{1} can have several numbers from 1-2, 2-2, 2-3 and 2-23 above, the number k′′ and l′′; the lower rule ∧EE_{1} have all numbers of two last rules ∧EE_{1} from π which are not numbers of the upper rule ∧EE_{1} and n′′, and it can have the numbers k′′ and l′′ when they are not number of the upper rule ∧EE_{1}.

In all conversions below the connections between numbers of π and π̄ are as in this conversion.

(Emaxs_{∧_{2}}^{∧_{1}}) Similarly to (Emaxs_{∧_{1}}^{∧_{1}}).

(Emaxs_{⊃}^{∧_{1}}) The redex π and the contractum π̄ are

\begin{matrix}\begin{aligned}{Γ \atop π_{1}} ; A ∧ B & {/A^{a}/Δ \atop π_{2}} ; C ⊃ D \\ & C ⊃ D \end{aligned}  ∧EE_{1} & {Λ \atop π_{3}} ; C & {/D^{d}/Θ \atop π_{4}} ; G \\ G \end{matrix} ; ⊃EE and \frac{{Γ \atop π_{1}} ; A ∧ B  \begin{aligned}{/A^{a}/Δ \atop π_{2}} ; C ⊃ D & {Λ \atop π_{3}} ; C & {/D^{d}/Θ \atop π_{4}} ; G \\ & G \end{aligned} ; ⊃EE}{G} ∧ EE_{1}
(Emaxs_{∨}^{∧_{1}}) Similarly to (Emaxs_{⊃}^{∧_{1}}).
(Emaxs_{∀}^{∧_{1}}) and (Emaxs_{∃}^{∧_{1}}) are defined similarly to (Emaxs_{∧_{1}}^{∧_{1}}).

The conversions (Emaxs_{r}^{∧_{2}}) are completely analogous to the conversions (Emaxs_{r}^{∧_{1}}), where r is an arbitrary elimination rule.

(Emaxs_{∧_{1}}^{⊃}) The redex π and the contractum π̄ are

\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} and \frac{{Γ \atop π_{1}} ; A ⊃ B  {Δ \atop π_{2}} ; A \begin{matrix}{/B^{b}/Λ \atop π_{3}} ; C ∧ D & {/C^{c}/Θ \atop π_{4}} ; G \\ G \end{matrix} ; ∧EE_{1}}{G} ⊃EE

(Emaxs_{∧_{2}}^{⊃}) Similarly to (Emaxs_{∧_{1}}^{⊃}).

(Emaxs_{⊃}^{⊃}) The redex π and the contractum π̄ are

\begin{matrix}\begin{matrix}{Γ \atop π_{1}} ; A ⊃ B & {Δ \atop π_{2}} ; A & {/B^{b}/Λ \atop π_{3}} ; C ⊃ D \\ C ⊃ D \end{matrix} ⊃EE & {Θ_{1} \atop π_{4}} ; C & {/D^{d}/Θ_{2} \atop π_{5}} ; G \\ G \end{matrix} ; ⊃EEand \frac{{Γ \atop π_{1}} ; A ⊃ B {Δ \atop π_{2}} ; A \begin{aligned}{/B^{b}/Λ \atop π_{3}} ; C ⊃ D & {Θ_{1} \atop π_{4}} ; C & {/D^{d}/Θ_{2} \atop π_{5}} ; G \\ & G \end{aligned} ; ⊃EE}{G} ⊃EE

(Emaxs_{∨}^{⊃}) Similarly to (Emaxs_{⊃}^{⊃}).

(Emaxs_{∀}^{⊃}) and (Emaxs_{∃}^{⊃}) are defined similarly to (Emaxs_{∧_{1}}^{⊃}). The conversions (Emaxs_{r}^{∨}) are completely analogous to the conversions (Emaxs_{r}^{⊃}), where r is an arbitrary elimination rule. The conversions (Emaxs_{r}^{∀}) and (Emaxs_{r}^{∃}) are completely analogous to the conversions (Emaxs_{r}^{∧_{1}}), where r is an arbitrary elimination rule.

Emaxf-conversions and Emaxs-conversions make the set of Emax-conversions. In a derivation π its maximum formulae (i.e. maximum segments of one d-formula) and formulae from its maximum segments will be called the max-formulae of π.

π′ Emaxf π′′ (π′ Emaxs π′′) iff the derivation π′′ is obtained from the derivation π′ by replacing one its subderivation π, which has the form of the redex of an Emaxf-conversion (Emaxs-conversion), with the contractum of that Emaxfconversion (Emaxs-conversion).

π′ Emax π′′ iff either π′ Emaxf π′′ or π′ Emaxs π′′.

If for π′ Emax π′′ we want to note the last formula A^{s} of the maximum segment of the redex π, then we will write π′ Emax π′′ by the formula A^{s}.

π′ Emax> π′′ iff there is a sequence π_{0}, …, π_{n}, n > 0, such that π_{0} is π′, π_{n} is π′′, and for each i, i < n, π_{i} Emax π_{i+1}.

π′ Emax-converts into π′′ iff either π′ Emax> π′′ or π′ is π′′.

If a derivation π does not have any subderivation which is the redex of a Emax-conversion with a max-formula, then the derivation π will be called a normal derivation in N E^{o}.

3.3. Connections between conversions from SE^{o} and N E^{o}. We will present the connections between the conversions of derivations from the systems SE^{o} and N E^{o} by using the connections between the conversions of derivations from the systems δE and N E from [3, Section 6].

Theorem 3.1. Let D and C be derivations in the system SE^{o}.

If D p^{E}-conv C, then

(1) ψD = ψC in the system N E^{o};

(2) (ψD)^{−} = (ψC)^{−} in the system N E^{o}.

Proof. (1) See [3, Theorem 6.1].

(2) By the definition of π^{−} for a derivation π and the part (1). □

If a symbol is of the form: − either i or ( )(i), then the symbol i is its part; − (i)(j), then i and j are its parts; − (s)(t), then the symbols s and t and all their parts are its parts. The set which contains each symbol from an index a whose part is the index of the principal formula of one rule for connectives will be called the m-subset of the index a.

Theorem 3.2. If D m^{E}-conv C, then ψD Emax>ψC in the system N E^{o}. Moreover, if D m^{E}-conv C, A^{a} is its formula and b is the m-subset of a, then there is a sequence of derivations ψD ≡ π_{1}, …, π_{l+1} ≡ ψC, such that l = b̄ and for each i, 1 ⩽ i ⩽ l, π_{i} Emax π_{i+1} by some A^{s}, s ∈ b.

Proof. See [3, Theorem 6.2, Theorem 6.3] and [4, Theorem 2]. □

Theorem 3.3. In the system N E^{o}, if π Emax π′, then π^{−} Emax π^{′−}.

Proof. By the definition of π^{−} for a derivation π. □

Theorem 3.4. If D is a cut-free derivation in the system SE^{o}, then ψD and (ψD)^{−} are normal derivations in the system N E^{o}.

Proof. See [3, Corollary 6.5] and Theorem 3.3. □

4. Cut elimination and normalization

4.1. The cut-elimination theorem for the system SE^{o}. We will prove the cut-elimination theorem for the system SE^{o}.

Theorem 4.1. In the system SE^{o} each derivation F pm^{E}-converts into a cutfree derivation F_{cf}.

It is well known that to prove this theorem it is sufficient to prove the following lemma.

Lemma 4.1. Each derivation D of the form ^{\frac{\begin{matrix}D′ & D′′ \\ Γ→A & A^{a},Δ→B \end{matrix}}{Γ^{×a},Δ→B}} cut, where D′ and D′′ are cut-free derivations, pm^{E}-converts into a cut-free derivation F.

Proof. In the usual way, by an induction in the pair ⟨d, r⟩ where d is the degree of D and r is its rank. See the proof of Cut-lemma in [4]. We note that p^{E}-conversions and m^{E}-conversions are p-conversions and m-conversions without conversions (1 < lr ↖ rr − c = 1) from [4]. But, it is easy to see that in the proof of Cut-lemma from [4] the conversions (1 ⩽ lr ↗ rr − c = 1) can be used instead of conversions (1 < lr ↖ rr − c = 1). □

4.2. The normalization theorem for the system N E^{o}. We will prove the normalization theorem for the system N E^{o} by using the cut-elimination theorem for the system SE^{o}.

Theorem 4.2. In the system N E^{o} each derivation π Emax-converts into a normal derivation π_{N}.

Proof. In the system N E^{o} we consider a derivation π. If π is a normal derivation, then the derivation π_{N} is π. If π is not a normal derivation, then in the system SE^{o} we consider the ϕ-image of the derivation π, the derivation F = ϕπ. In the system N E^{o} there is the derivation ψF, i.e. ψϕπ, and by Theorem 2.1, ψF^{−} is π. By Theorem 4.1 the derivation F pm^{E}-converts into a cut-free derivation F_{cf}, i.e. there is a sequence of derivations F_{1}, …, F_{n}, such that n > 1 (by ψF^{−} = π and Theorem 3.4), F_{1} is F, F_{n} is F_{cf}, and for all i < n: either F_{i} p^{E}-conv F_{i+1} or F_{i} m^{E}-conv F_{i+1}.

So, in N E^{o} there is the sequence ψF_{1}, …, ψF_{n}, n > 1, such that:

(1) ψF_{1} is ψϕπ;

(2) for each i, 1 ⩽ i ⩽ n − 1, (2.1) if F_{i} p^{E}-conv F_{i+1}, then ψF_{i} = ψF_{i+1} (by Theorem 3.1(1)); (2.2) if F_{i} m^{E}-conv F_{i+1}, then ψF_{i} Emax> ψF_{i+1} (by Theorem 3.2);

(3) ψF_{n} = ψF_{cf} is a normal derivation (by Theorem 3.4).

Thus, in the system N E^{o} we have a sequence of different derivations from the sequence ψF_{1}, …, ψF_{n}, the sequence ψF_{i_{1}}, ψF_{i_{2}}, …, ψF_{i_{k}}, 1 = i_{1} <⋯ < i_{k}⩽ n, k ⩽ n. ψF_{i_{k}} is the normal derivation ψF_{cf} and for all i_{j} and i_{j+1}, 1 ⩽ j ⩽ k − 1: ψF_{i_{j}} Emax> ψF_{i_{j+1}}. Thus, there is a sequence of derivations π_{1}^{j}, π_{2}^{j}, …, π_{m_{j}}^{j}, m_{j} > 1, such that ψF_{i_{j}} ≡ π_{1}^{j} Emax π_{2}^{j} E max … Emax π_{m_{j}}^{j} ≡ ψF_{i_{j+1}}.

By (1) and Theorem 2.1, ψF_{1}^{−} ≡ ψF_{i_{1}}^{−} is π and by Theorem 3.4, ψF_{i_{k}}^{−} is a normal derivation. Next, in N E^{o} for each derivation π′, there is the derivation π^{′−}, so for each j, 1 ⩽ j ⩽ k − 1, we have the sequence of derivations π_{1}^{j−}, π_{2}^{j−}, …, π_{m_{j}}^{j−}, m_{j} > 1, and by Theorem 3.3: ψF_{i_{j}}^{−} ≡ π_{1}^{j−} Emax π_{2}^{j−} E max … Emax π_{m_{j}}^{j−} ≡ ψF_{i_{j+1}}^{−}.

Thus, there is the following sequence of conversions:

π ≡ π_{1}^{1−}E max … E max π_{m_{1}}^{1−} ≡ ψF_{i_{2}}^{−} ≡ π_{1}^{2−}E max … E max π_{m_{k−1}}^{k−1−} ≡ ψF_{i_{k}}^{−}, i.e. the derivation π Emax-converts into a normal derivation, the derivation ψF_{i_{k}}^{−}. □

Acknowledgments. I am grateful to the anonymous referee for some useful comments concerning the previous version of this paper. This work was supported by project ON 174026 of the Ministry of Education, Science and Technological Development of the Republic of Serbia.

References

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

2. , A cut-elimination proof in intuitionistic predicate logic, Ann. Pure Appl. Logic 99 (1999), 105–136.

3. , Extended natural-deduction images of conversions from the system of sequents, J. Log. Comput. 14(6) (2004), 769–799.

4. , A connection between cut elimination and normalization, Arch. Math. Logic 45(2) (2006), 113–148.

5. , Normalization as a consequence of cut elimination, Publ. Inst. Math., Nouv. Sér. 86(100) (2009), 27–34.

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

7. , 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. S. Negri, J. von Plato, Structural Proof Theory, Cambridge University Press, 2001.

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

11. , Translations from natural deduction to sequent calculus, Math. Log. Q. 49 (2003), 435–443.

12. , A sequent calculus isomorphic to Gentzen’s natural deduction, Rev. Symb. Log. 4(1) (2011), 43–53.

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

14. D. Prawitz, Natural Deduction, Almquist and Wiksell, Stockholm, 1965.

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

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

17. A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 1996.

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

Faculty of Transport and Traffic Engineering (Received 07 09 2016) University of Belgrade (Revised 23 12 2016) Belgrade Serbia

    mirjanab@afrodita.rcub.bg.ac.rs