Double Negation in Lukasiewicz’s Propositional Logic

Michael Beeson Larry Wos

April 15, 2001

1 Introduction

Although propositional calculus is one of the oldest areas of logic, not all of its mysteries have been unlocked. A number of different axiomatizations and proof systems for propositional logic are known, some of which permit the formulation of a “single axiom”–a formula from which all tautologies can be derived. The existence of truth tables and other decision procedures for propositional logic notwithstanding, it is by no means trivial to prove, for example, that a given 23symbol formula is in fact a single axiom. Truth tables and decision procedures can be used to determine if a given formula is a tautology, or to construct a proof of a given formula from certain axioms and rules, but generally they are not helpful in finding proofs of known axioms from other formulas (which is what one must do to verify that a formula is a single axiom). The search for such proofs has recently become a testbed in automated deduction. We here prove a theorem about propositional logic, that justifies a shortcut in such automated proof-search methods, and besides, has its intrinsic esthetic appeal.

Let L be Lukasiewicz’s formulation of propositional calculus in terms of implication and negation, denoted by i and n, as given on page 221 of [7] p.

221. Specifically, L has three axioms:

L1  i(i(x, y), i(i(y, z), i(x, z)))
L2  i(i(n(x), x), x)
L3  i(x, i(n(x), y))

The inference rules to be used with these axioms are modus ponens and substitution. Specifically, given a major premiss i(p, q) and a minor premiss p, the conclusion of modus ponens is q. The substitution rule permits the deduction of pσ from p, where σ is any substitution. We also consider a more restrictive inference rule called condensed detachment; one section of the paper is devoted to the relationship between this rule and the modus-ponens-substitution system. Our main theorems apply to L1-L3 with condensed detachment as well as to L1-L3 with modus ponens and substitution.

A double negation is a formula n(n(t)), where t is any formula. A formula A contains a double negation if it has a subformula that is a double negation. A derivation contains a double negation if one of its formulas contains a double negation. Suppose that the formula A contains no double negations and is derivable in L. Then does A have a derivation in L that contains no double negation? We answer this question in the affirmative, by translating L into sequent calculus and applying Gentzen’s cut-elimination theorem, and then translating the cut-free proof back into L.

The proof that the translation is sound requires finding double-negation-free proofs of twenty-five specific theorems of L that are used in the translation. We used the theorem-prover Otter to find those proofs. To find these proofs by hand would have been time-consuming, to say the least.

The reason why this theorem is interesting is that it justifies a technique used by Wos in controlling Otter’s search for proofs in this area. Namely, Wos found it useful to cause Otter to discard, rather than retain, any double negations generated during the proof search. The theorem proved here shows that this strategy is a safe one, in that there are no theorems whose proofs actually require the use of double negations that are not contained in the theorem itself. Also, the theorem has a certain appeal because it has the flavor of a Gentzen-style result, but about a decidedly un-Gentzen-like proof system. It shows that something of the flavor of cut-free proofs persists even in quite different formulations of propositional logic, and the proof, which uses Gentzen’s systems and results, shows that this is not accidental.

We would like to thank Kenneth Harris, Branden Fitelson, Ted Ulrich, and Robert Veroff for their attention to early drafts of this paper–Ulrich and Veroff contributed one lemma each (Lemmas 3 and 4), and Harris put Lemma 6 into its present general form.

2 Some theorems proved by Otter

This section presents examples to illustrate the theorem. These special cases are needed in the proof and must therefore be dealt with directly. We submitted an appropriate input file to the theorem-prover Otter, which produced the proofs given in the Appendix (after slight editing for readability). In these proofs, the first column is the statement number, and the second column lists the justification for the line.

Lemma 1 L proves the following formulas without double negation.

i(i(x, n(x)), n(x))  (1)

i(i(x, i(x, y)), i(x, y))  (2)
i(x, (i(y, x))  (3)
i(i(n(x), y), i(n(y), x))  (4)
i(i(x, n(y)), i(y, n(x)))  (5)
i(i(x, y), i(n(y), n(x)))  (6)
i(i(n(x), n(y)), i(y, x))  (7)
i(i(x, i(y, z)), i(y, i(x, z)))  (8)
i(x, x)  (9)
i(i(x, y), i(i(n(x), z), i(n(y), z))  (10)
i(i(x, i(n(y), z)), i(n(i(x, y)), z))  (11)
i(i(n(i(x, y)), z)), i(x, i(n(y), z))  (12)
i(i(x, i(y, z)), i(n(i(x, n(y))), z))  (13)
i(i(n(i(x, n(y))), z), i(x, i(y, z)))  (14)
i(i(x, n(y)), i(i(n(x), z), i(y, z)))  (15)
i(i(n(x), y), i(i(x, z), i(n(y), z)))  (16)
i(i(x, i(n(y), z)), i(x, i(n(z), y)))  (17)
i(i(x, i(y, z)), i(x, i(n(z), n(y))))  (18)
i(i(x, i(n(y), n(z))), i(x, i(z, y)))  (19)
i(i(x, i(y, n(z))), i(x, i(z, n(y))))  (20)
i(i(x, i(y, i(z, w))), i(x, i(z, i(y, w)))  (21)

Proof. See the Appendix.

Lemma 2 L proves i(n(n(x)), x) without using any doubly-negated formula except n(n(x)).

Proof. The following proof was produced using Otter:

29  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
33  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
36  [29,29]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
42  [29,33]  i(i(x, n(y)), i(y, i(x, z)))
47  [33,7]  i(x, x)
60  [36,7]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [33,42]  i(x, i(y, i(n(x), z)))
76  [36,60]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
98  [65,7]  i(x, i(n(i(i(n(y), y), y)), z))

111 [76,98] i(i(x, i(n(y), y)), i(z, i(x, y))) 136 [29,111] i(i(n(x), y), i(z, i(i(y, x), x))) 162 [76,136] i(i(x, i(y, z)), i(i(n(z), y), i(x, z)))

190 [36,162] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 204 [162,8] i(i(n(x), n(y)), i(y, x)) 220 [29,190] i(i(n(x), y), i(i(z, i(u, x)), i(i(y, u), i(z, x)))) 240 [33,204] i(x, i(y, x)) 288 [190,240] i(i(x, i(y, z)), i(y, i(x, z))) 363 [288,L3] i(n(x), i(x, y)) 386 [162,363] i(i(n(x), y), i(n(y), x)) 426 [386,47] i(n(n(x)), x)

That completes the proof of Lemma 2.

The following two lemmas were proved by hand, or by a specially compiled version of Otter, since the publicly available version of Otter proves a more general theorem and then identifies some variables to obtain these results. The Otter proof then does not correspond to a proof by condensed detachment.

Lemma 3 L proves i(i(x, x), i(n(x), n(x))).

Proof . [Ted Ulrich, found without machine assistance]. The first two lines below are formulas shown in Lemma 1 to be provable.

2  (2)  i(i(x, i(x, y)), i(x, y))
6  (6)  i(i(x, y), i(n(y), n(x)))

44 [2,L1] i(i(x, x), i(x, x)) 45 [L1,6] i(i(i(n(y), n(x)), z), i(i(x, y), z)) 43 [45,44] i(i(x, x), i(n(x), n(x)))

Lemma 4 L proves i(i(x, x), i(i(y, y), i(i(x, y), i(x, y)))).

Proof . [Robert Veroff, using a special version of Otter].

45  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
47  [L1,45]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
48  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
49  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
50  [48,L2]  i(x, x)
51  [50,L1]  i(i(x, y), i(x, y))
52  [49,51]  i(i(n(i(x, y)), i(x, y)), i(x, y))
53  [47,48]  i(x, i(n(i(i(n(y), y), y)), z))
54  [53,L1]  i(i(i(n(i(i(n(x), x), x)), y), z), i(u, z))
55  [46,46]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
56  [46,L1]  i(i(x, y), i(i(i(x, z), u), i(i(y, z), u)))
57  [54,52]  i(x, i(i(n(y), y), y))
58  [55,57]  i(i(x, i(n(y), y)), i(z, i(x, y)))

59  [58,46]  i(i(n(x), y), i(z, i(i(y, x), x)))
60  [58,L3]  i(x, i(y, y))
61  [59,58]  i(x, i(i(n(y), z), i(i(z, y), y)))
62  [59,60]  i(x, i(i(i(y, y), z), z))
63  [61,61]  i(i(n(x), y), i(i(y, x), x))
64  [63,55]  i(i(x, i(y, z)), i(i(n(z), y), i(x, z)))
65  [63,48]  i(x, i(i(y, x), x))
66  [65,55]  i(i(x, i(y, z)), i(z, i(x, z)))
67  [66,65]  i(x, i(x, x))
68  [66,62]  i(x, i(y, x))
69  [67,60]  i(i(x, i(y, y)), i(x, i(y, y)))
70  [68,67]  i(i(x, i(y, x)), i(x, i(y, x)))
71  [64,55]  i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y))))
72  [56,55]  i(i(x, i(i(y, z), u)), i(i(y, v), i(x, i(i(v, z), u))))
73  [71,68]  i(i(x, i(y, z)), i(y, i(x, z)))
74  [73,L1]  i(i(i(x, i(y, z)), u), i(i(y, i(x, z)), u))
75  [74,69]  i(i(x, i(y, x)), i(y, i(x, x)))
76  [75,L1]  i(i(x, x), i(i(y, x), i(y, x)))
77  [72,70]  i(i(x, i(i(y, z), u)), i(i(y, y), i(x, i(i(y, z), u))))
78  [77,76]  i(i(x, x), i(i(y, y), i(i(x, y), i(x, y))))

3 Condensed detachment

A more restricted system with axioms L1-L3 has been considered in the literature [2, 3], and the original question answered in this paper was about that system. The substitution rule is not used, and modus ponens is replaced by by condensed detachment, in which the major premiss is i(p, q), the minor premiss is r where r unifies with p, and the conclusion is qσ, where σ is the most general unifier of p and r. For example, if α is a complicated formula, and we wish to deduce i(α, α), it would not be acceptable to first deduce i(x, x) and then substitute x = α. We would be forced to give a (longer) direct derivation of i(α, α).^{1} We shall show in this section that our theorem about the eliminability of double negation holds for L1-L3 with condensed detachment, if and only if it holds for L1-L3 with modus ponens and substitution. Similar but not identical results are in [2, 5].

Lemma 5 Every formula of the form i(α, α) is provable from L1-L3 by condensed detachment, without using double negations except those occurring as subformulas of α.

1In the absence of the substitution rule, any alphabetic variant of an axiom is also accepted as an axiom. An “alphabetic” variant of A is a formula Aσ where the substitution σ is oneto-one and merely renames the variables.

Proof . By Lemma 1, formulas (9), Lemma 3, and Lemma 4, the following are provable by condensed detachment (without using double negation) from L1-L3:

i(x, x)  (22)
i(i(x, x), i(i(y, y), i(i(x, y), i(x, y))))  (23)
i(i(x, x), i(n(x), n(x)))  (24)

It follows by induction on the complexity of the propositional formula α that for each α, the formula i(α, α) is provable in L1-L3 by condensed detachment. The base case, when α is a proposition letter, follows by replacing x by α in the proof of i(x, x). The line (the proof in Lemma 1 is only two lines long) that is an axiom becomes an alphabetic variant of an axiom, which is still considered an axiom. If we have a proof of i(β, β) then we can apply condensed detachment and i(i(x, x), i(n(x), n(x))) to get a proof of i(n(β), n(β)). This could introduce a double negation if β is already a negation, but in that case it is a double negation that already occurs in α = n(β), and so is allowed. Similarly, if we have proofs of i(α, α) and i(β, β), we can apply condensed detachment to the second formula just given and get a proof of i(i(α, β), i(α, β)). That completes the proof of the lemma.

Lemma 6 Let σ be a substitution and A be any formula. Suppose that α = Aσ has no variables in common with A and the domain of σ is contained in the set of variables of A. Then σ is the most general unifier of A and Aσ.

Remark. We need this only when A is an instance of L1, L2,or L3, in which case it can be seen more directly by considering the unification algorithm. But Kenneth Harris stated (and proved) the matter in the proper generality, and we give his formulation here. Proof . Define a substitution σ to be idempotent if σσ = σ. Let Dσ be the domain of σ and Iσ the set of variables contained in the range of σ, i.e. the variables introduced by σ when applied to the variables in its domain. Then Dσ ∩ Iσ is empty if and only if σ is idempotent.

Now let A and σ be as in the hypothesis of the lemma. Then Dσ ∩ Iσ is empty, so σ is idempotent. Therefore σ unifies A and Aσ. We will show it is a most general unifier. Let β be a substitution such that Aβ = Aσβ, and assume the domain of β is contained in the set of variables of A. Then also Cβ = Cσβ for all subformulas C of A. We must show that for some substitution α, we have β = σα. But it suffices to take α = β: let x be in the domain of β; then x is a subformula of A and hence we can take C = x in Cβ = Cσβ, so xβ = xσβ. Since x was any element of the domain of β, we have β = σβ. This completes the proof of the lemma.

Lemma 7 Every substitution instance of axioms L1, L2, and L3 is provable by condensed detachment.

Proof . Let α be a substitution instance of an axiom A (so A is one of L1, L2, or L3). Renaming the variables in the axiom A if necessary, we may assume that the variables occurring in A do not occur in α. By Lemma 5, i(α, α) is provable by condensed detachment. Let σ be the substitution such that Aσ = α. By the preceding lemma, σ is the most general unifier of α and A, so we can apply condensed detachment to i(α, α) and A to conclude α. That completes the proof of the lemma.

Lemma 8 If A is provable in L1-L3 with condensed detachment, and σ is any substitution, then Aσ is provable in L1-L3 with condensed detachment.

Proof . The base case has been done in Lemma 3. For the induction step, suppose the last inference has the premisses i(p, q) and r, where τ is the most general unifier of p and r, and the conclusion is qτ = A. By the induction hypothesis, we have condensed-detachment derivations of i(pτσ, qτσ) and of rτσ. Since pτ = rτ, also pτσ = rτσ, the inference from i(pτσ, qτσ) and rτσ to qτσ is legal by condensed detachment. Hence we have a condensed detachment proof of qτσ = Aσ. That completes the proof of the lemma.

Theorem 1 If L1-L3 proves A using modus ponens and substitution, then L1-L3 proves A using condensed detachment, by a proof involving no new double negations; that is, every doubly-negated formula in the condensed-detachment proof occurs already in the modus-ponens-and-substitution proof.

Proof . We proceed by induction on the length of the derivation using modus ponens and substitution. For the base case, A is an axiom, and there is nothing to prove. Suppose the last inference is by substitution, with premiss B and conclusion A = Bσ. By the induction hypothesis there exists a condenseddetachment proof of B. By Lemma 8, there exists a condensed-detachment proof of A. Now suppose the last inference is by modus ponens, inferring A from i(B, A) and B. By the induction hypotheses there are condensed detachment proofs of B and i(B, A). The inference from these premisses to A can be made by condensed detachment (the most general unifier required is the identity). Therefore there is a condensed-detachment proof of A. That completes the proof of the theorem.

4 L and sequent calculus

Let G1 be the intuitionistic Gentzen calculus as given in Kleene [4]. Let G be G1 (minus cut), restricted to implication and negation, i.e., formulas containing other connectives are not allowed. Thus the rules of inference of G are the four rules involving implication and negation, plus the structural rules. The rules of G1 are listed on pp. 442-443 of [4]. They will also be given in the course of the proof.

We remind the reader that L is propositional logic with Lukasiewicz’s axioms L1-L3, using modus ponens and substitution as inference rules. We also remind the reader that by the results of the preceding section, L1-L3 with condensed detachment as the only inference rule proves every theorem of L, and without introducing double negations that were not present in the proof using modus ponens and substitution. We give a translation of L into G. Namely, if A is a formula of L, then A^{0} is a formula of G, obtained by these rules:

i(a, b)^{0} = a^{0} → b^{0}
n(a)^{0} = ¬a^{0}

Of course, when a is a proposition letter (variable) then a^{0} is just a. If Γ = A_{0}, …, A_{n} is a list of formulas of L, then Γ^{0} is the list A_{0}^{0}, …, A_{n}^{0}.

We translate G into L in the following manner. First we assign to each formula A of G a corresponding formula A′ of L, given by

(A → B)′ = i(A′, B′)
(¬A)′ = n(A′)

where again A′ = A for proposition letters A. We need to define Γ′ also, where Γ is a list of formulas; but the definition is different for lists occurring on the left of ⇒ than for lists occurring on the right. Officially then, the (·)′ function takes an additional argument when its main argument is a list. What we write as Γ′ for human readability is really ′( em left, Γ) or ′(right, Γ). We agree to suppress the left and right arguments, which should be clear from the context. If Γ = A_{1}, …, A_{n} is a list of formulas occurring on the left of ⇒, then Γ′ is A′_{1}, …, A′_{n}. If Γ = A_{1}, …, A_{n} occurs on the right of ⇒, then Γ′ is a single formula of L, defined thus: For lists of length 1, say [A], we define [A]′ = A′. We do not define []′, where [] is the empty list. For lists of length at least 2, we define:

(A_{1}, …, A_{n}, ¬A_{n+1})′ = i(A_{n+1}, (A_{1}, …, A_{n})′)

(A_{1}, …, A_{n+1})′ = i(n(A_{n+1}), (A_{1}, …, A_{n})′) if A_{n+1} is not a negation

We use recursion from the right rather than the left, since Kleene defined his contraction rule “from the right”. Note that this translation does not introduce double negations in (A′_{1}, …, A′_{n}) where none occur in (A_{1}, …, A_{n}). We can express the translation of lists in a single equation if we introduce the notation ñ by ñ(a) = n(a) if a is not a negation, and ñ(n(a)) = a. Then we have

(A_{1}, …, A_{n+1})′ = i(ñ(A_{n+1}), i((A_{1}, …, A_{n})′)

In general a “formula” of L involving ñ is an abbreviation of two or more formulas of L.^{2}

These two translations are inverses:

2We note that essentially this same translation has been given in [6] in connection with

Lemma 9 Let A be a formula of L. Then A^{0}′ = A.

Proof. By induction on the complexity of A. If A is a variable, then A^{0} = A and A^{0}′ = A. We have

i(x, y)^{0}′ = (x^{0} → y^{0})′
= i(x^{0}′, y^{0}′)
= i(x, y)

and we have

n(x)^{0}′ = (¬(x^{0}))′
= n(x^{0}′)
= n(x)

Henceforth we simplify our notation by using lower-case letters for formulas of L, and upper-case letters for formulas of G. Then we can write a instead of A′, and A instead of a^{0}. By the preceding lemma, there is no ambiguity in this convenient notation. Thus, for example, (A → B)′ is i(a, b). Greek letters are used for lists of formulas, and upper-case and lower-case again refer to G and L. But bear in mind, if Θ is a list of length 2 or more, for example A, B, then θ = Θ′ is i(n(a), b) when Θ occurs on the right of ⇒.

The following lemma is needed in carrying out an inductive proof later in the paper. It can be skipped on the first reading. By (Γ, Δ) we mean the result of appending the lists Γ and Δ. By (Γ, C) we mean the result of adding one more element C to the list Γ. Were we to be formal about these matters, we would regard the lists as “written backwards”, so that our recursions from the right end of lists would be normal list recursions, and (Γ, C) would be [C|Γ]. Instead of introducing formal list notation, we stick with (Γ, C) and (Γ, Δ).

Lemma 10 When the list Δ is not empty, and (Γ, Δ) occurs on the right of ⇒, then (Γ, Δ)′ is equivalent in L to i(ñ(Δ′), Γ′).

Remark. We spell out what is abbreviated by the use of ñ in the statement of the lemma. If Δ′ is a negated formula n(α), then (Γ, Δ)′ is equivalent to i(α, Γ′). Otherwise, (Γ, Δ)′ is equivalent to i(n(Δ′), Γ′). Proof. By induction on the length of the list Δ. When the length of Δ is one, the conclusion of the lemma is just the definition of (Γ, Δ)′. For the induction step, we replace Δ in the statement of the lemma by (Δ, C). We have

(Γ, (Δ, C))′ = ((Γ, Δ), C)′  by the associativity of append

Lukasiewicz’s multi-valued logics. It is the obvious translation of Gentzen calculus into the implication-and-negation fragment of propositional calculus. Since we need to check that the translation is sound without using double negation, we cannot appeal to any of the results of [6].

= i(ñ(C), (Γ, Δ)′)
= i(ñ(C), i(ñ(Δ′), Γ′))  by the induction hypothesis
= i(ñ(C), i(ñ(δ), γ))

On the other hand,

i(ñ((Δ, C)′), Γ′) = i(ñ(i(ñ(C), δ)), γ)
= i(n(i(ñ(C), δ)), γ)

What we need then is the equivalence in L of i(x, i(ñ(y), z)) and i(n(i(x, y)), z), which could be applied with x = ñ(C), y = δ, and z = γ. Because of the use of ñ, there are really two equivalences, one obtained by replacing ñ by n, and the other obtained by replacing ñ(y) by y and y by n(y). Then each of the two equivalances has to be formulated as two implications in L, left-to-right and right-to-left. These four theorems have already been proved in L as formulas

(11) through (14) of Lemma 1. That completes the proof of the lemma.

Lemma 11 (Deduction theorem for L) If L proves a from assumptions δ, B, then i(b, a) is a theorem proved in L from assumptions δ. Moreover, if the given proof has no double negations, then this proof in L from δ has no double negations.

Proof. By induction on the length of proofs in L. Base case: a either is b or a member of δ, or an axiom of L. If a is b, then we use the fact that i(b, b) is a theorem of L, provable without double negations (except those occurring in b) by Lemma 5. If a is a member of δ or an axiom of L, then we use the fact that i(x, i(y, x)) is a theorem of L, provable without double negations, by formula

(3) of Lemma 1. Applying the substitution x := a, y := b, we have a proof of i(a, i(b, a)) from δ without double negations except those occurring in a and b. Applying detachment, we have a proof of i(b, a) from δ as desired.

Turning to the induction step, suppose the last step in the given proof infers q from i(p, q) and p. By the induction hypothesis, we have proofs of i(b, p) and i(b, i(p, q)) from δ. By axiom L1 and substitution we have i(i(b, p), i(i(b, i(p, q), i(b, q)))). Applying detachment once, we have i(i(p, q), i(b, q))). Applying detachment again, we have i(b, q) as desired. Note that no double negations are introduced. That completes the proof of the lemma.

We shall call a sequent Γ ⇒ Δ “double-negation-free” if it contains no double negation. Since the L-translation does not introduce new double negations, this is the same as requiring that the L-translation contain no double negation.

Lemma 12 If the final sequent Γ ⇒ Θ of a G-proof is double-negation-free, then the entire G-proof is double-negation free.

Proof. By the subformula property of cut-free proofs: every formula in the proof is a subformula of the final sequent.

Lemma 13 (i) Suppose G proves the sequent Γ ⇒ Δ, where Δ is nonempty. Then L proves δ from assumptions γ. If G proves Γ ⇒ [], where [] is the empty list, then L proves p from assumptions γ, where p is any variable of L not occurring in γ.

(ii) If any double negations occur in subformulas of the given sequent Γ ⇒ Δ (where here Δ can be empty or not), then a proof in L as in (i) can be found that contains no double negations except those arising from the L-translations of double-negated subformulas of Γ ⇒ Δ.

(iii) If in part (i) the L-translation of the given sequent Γ ⇒ Δ does not contain any double negations, then the proof in L that is asserted to exist can also be found without double negations.

Proof.

We proceed by induction on the length of proof of Γ ⇒ A in G. base case: the sequent has the form Γ, A ⇒ A. We must show that a is derivable in L from premisses γ, a, which is clear. Now for the induction step. We consider one case for each rule of G.

Case 1, the last inference in the G-proof is by rule →⇒:

Δ ⇒ Λ, A B, Γ ⇒ Θ

A → B, Δ, Γ ⇒ Λ, Θ

By the induction hypothesis, we have an L-proof of (Λ, A)′ from δ, and an L-proof of θ from b and γ. We must give an L-proof of (Λ, Θ)′ from i(a, b), δ, and γ. We consider several cases, according as A is or is not a negation, Λ is or is not empty, and Θ is empty, or of length 1, or of length 2 or more.

First consider the case (1a) that Λ is empty, so (Λ, A)′ is just a. Applying detachment to i(a, b) (which is (A → B)′) and the given proof of a from δ, we derive b. Copying the steps of the proof of θ from assumptions b, γ (but changing the justification of the step(s) b from “assumption” to the line number where b has been derived) we have derived θ from assumptions (A → B)′,δ, γ, completing the proof of case 1 when Λ is empty.

Henceforth we may assume that Λ is not empty. We now claim that L proves (i(n(b), λ) from assumptions i(a, b) and δ. We call this “Claim Q”. We argue for Claim Q by cases, according as A is a negation or not. First, we assume A is not a negation. Then we are given by the induction hypothesis an L-proof of i(n(a), λ) from assumptions δ. By (10) of Lemma 1,

i(i(a, b), i(i(n(a), λ), i(n(b), λ)))

is a theorem of L. Applying detachment twice, we see that L proves i(n(b), λ) from assumptions i(a, b) and δ. This is claim Q.

Now we argue for Claim Q in case A is a negation, say A = ¬E, and Λ is not empty. As usual we denote E′ by e, so (Λ, A)′ is i(e, λ). Then we are given by the induction hypothesis an L-proof of i(e, λ) from assumptions δ. By (16) of Lemma 1 (taking x = e, y = b, and z = λ),

i(i(n(e), b), i(i(e, λ), i(n(b), λ)))

is a theorem of L. Applying detachment twice, we see that L proves i(n(b), λ) from assumptions i(a, b) and δ. This establishes Claim Q for the case A is a negation. Since that was the second case, Claim Q is now established.

In addition to the proof of i(n(b), λ) from assumptions i(a, b) and δ, we also have (by the induction hypothesis) an L-proof of θ from assumptions b, γ. At this point the argument divides into case (1b), when Θ is the empty list, and case (1c), when Θ is not empty.

Case (1b): Θ is the empty list. Then θ is a new variable not occurring elsewhere in the proof, and we require a proof of λ from assumptions i(a, b), δ, γ. Substituting n(b) for the variable θ we have an L-proof of n(b) from assumptions b, γ. Applying detachment to this and i(n(b), λ), we have a proof of λ from assumptions i(a, b), δ, γ as required. This completes the proof of case (1b).

Case (1c): Θ is not empty. We require a proof of (Λ, Θ)′ from assumptions i(a, b), γ, δ. Applying the deduction theorem to the L-proof of θ from b, γ, we have an L-proof of i(b, θ) from γ. So from the desired assumptions we can prove i(b, θ) and i(n(b), λ), and we require a proof of (Λ, Θ)′. By Lemma 10, (Λ, Θ)′ is equivalent in L to i(ñ(θ), λ), just as it would be if Θ were a list of length one. Our situation is this: we have i(b, θ) and i(n(b), λ), and we require i(ñ(θ), λ). If θ is not a negation, we can replace ñ(θ) by n(θ). Applying (10) from Lemma 1, with x = b, y = θ, and z = λ, we have

i(i(b, θ), i(i(n(b), λ), i(n(θ), λ))).

Applying detachment twice we have i(n(θ), λ) as desired. If, on the other hand, θ = n(α), then our situation is this: we have i(b, n(α)) and i(n(b), λ), and we require i(α, λ). Taking x = b, y = α, and z = λ in formula (15) of Lemma 1, we have

i(i(b, n(α)), i(i(n(b), λ), i(α, λ))).

Applying detachment twice we have i(α, λ) as required. This completes the proof of case (1c), and hence of case 1.

Case 2, the last inference in the G-proof is by rule ⇒→:

{A, Γ ⇒ Θ, B \atop Γ ⇒ Θ, A → B}

Case 2a, Θ is the empty list. By the induction hypothesis, we have an Lproof of b from γ and a. Applying the deduction theorem for L, we have a proof in L of i(a, b) from γ. But (A → B)′ = i(a, b), completing this case. Note that double negations are not introduced by the deduction theorem if they are not already present.

Case 2b, Θ is not empty. By the induction hypothesis, we have an L-proof of i(ñ(b), θ) from assumptions γ and a. By the deduction theorem for L, we have a proof of i(a, i(ñ(b), θ)) from γ. We require a proof of i(n(i(a, b)), θ) from γ. There are two cases, according as B is a negation or not. First, if B is not a negation, then we have a proof of i(a, i(n(b), θ)) and require a proof of i(n(i(a, b)), θ). Taking x = a, y = b, and z = θ in formula (11) of Lemma 1, we have

i(i(a, i(n(b), θ)), i(n(i(a, b)), θ)).

Applying detachment, we obtain the desired proof of i(n(i(a, b)), θ) in L.

Second, if B is a negation, say B = ¬C, then b is n(c) and ñ(b) is c, so we have an L-proof of i(a, i(c, θ)) from γ, and we require a proof of i(n(i(a, n(c))), θ). By formula (13) of Lemma 1, we have i(i(x, i(y, z)), i(n(i(x, n(y)), z)). Apply the substitution x := a, y := c, z := θ, and then apply detachment. This yields the required proof of i(n(i(a, n(c))), θ. That completes the proof of Case 2b and the proof of Case 2.

Case 3, the last inference in the G-proof introduces negation on the right:

{A, Γ ⇒ Θ \atop Γ ⇒ Θ, ¬A}

Case 3a, Θ is the empty list. Then by the induction hypothesis, there is an L-proof of p from a and γ, where P is a new variable (not occurring in Γ or A). By the deduction theorem for L, there is a proof of i(a, p) from γ. So it suffices to show that n(a) is derivable in L from i(a, p). This follows from i(i(x, n(x)), n(x)) by detachment. We have shown in Lemma (1), formula (1), that this formula is provable in L without using double negation.

Case 3b, Θ is not empty. Then (Θ, ¬A)′ is i(a, θ). By induction hypothesis there is an L-proof of θ from a and γ. By the deduction theorem for L, there is a proof of i(a, θ) from γ. This completes the proof of Case 3b, and hence of Case 3.

Case 4, the last inference in the G-proof introduces negation on the left:

{Γ ⇒ Θ, A \atop ¬A, Γ ⇒ Θ}

Case 4a, Θ is the empty list. By the induction hypothesis, we have an Lproof of a from γ. We must show that from n(a) and γ, we can deduce b in L, where b is a new variable. We have i(a, i(n(a), b) by axiom L3. Applying detachment twice, we have the desired proof of b, completing case 4a.

Case 4b, Θ is not empty. In proving part (iii) of the lemma, we are assuming that ¬A contains no double negation; therefore, A is not a negation, so (Θ, A)′ is i(n(a), θ). By the induction hypothesis, we have an L-proof of i(n(a), θ) from γ. We must show that from n(a) and γ we can derive θ. But this follows immediately by detachment. This completes the proof as far as part (iii) of the lemma goes.

In proving parts (i) and (ii) of the lemma, we can no longer be certain that A is not a negation, so we must treat the case when A is ¬E. Then (Θ, A)′ is i(e, θ), and by the induction hypothesis, we have an L-proof of i(e, θ) from γ. We must show that from n(a) (that is, n(n(e))) and γ we can derive θ. It is permissible to use the double negation n(n(e)) since this double negation arises from the double negated formula ¬¬E, that is ¬A, which occurs in the conclusion of this inference, which is the final sequent of the proof. We have i(n(n(e)), e) provable in L without using any double negation other than n(n(e)), as shown in Lemma 2. By detachment we have a proof of e from n(n(e)). Applying detachment, using the given proof of i(e, θ) from γ, we obtain the required proof of θ from n(n(e)) and γ. This completes case 4b, and hence also case 4.

Case 5, the last inference is by contraction in the antecedent:

{C, C, Γ ⇒ Θ \atop C, Γ ⇒ Θ}

By the induction hypothesis we have a proof of θ from assumptions c, c, which also qualifies as a proof from assumptions c, so there is nothing more to prove.

Case 6, the last inference is by contraction in the succedent (the succedent is the part of a sequent to the right of the ⇒ sign):

{Γ ⇒ Θ, C, C \atop Γ ⇒ Θ, C}

Case 6a, Θ is the empty list. By the induction hypothesis we have a proof in L from assumptions γ of i(ñ(c), c). We need a proof of c from γ. If C is not a negation, we have a proof from γ of i(n(c), c). By axiom L2 we have i(i(n(c), c), c). Applying detachment we get a proof of c as desired. If C is a negation, say ¬E, then c is n(e), and we have a proof from γ of i(e, c), that is to say i(e, n(e)), and we need a proof of n(e) from γ. But i(i(e, n(e)), n(e)) is formula (1) of Lemma 1, so applying detachment we obtain the required proof. This completes case 6a.

Case 6b, Θ is not empty. We have by the induction hypothesis a proof in L from γ of i(ñ(c), i(ñ(c), θ)). We need a proof of i(ñ(c), θ). By formula (2) of Lemma 1, we have

i(i(x, i(x, y)), i(x, y)).

Taking x = ñ(c) and y = θ, and applying detachment, we get the desired result. This completes case 6b, and hence case 6.

Case 7, the last inference is by thinning in the succedent:

{Γ ⇒ Θ \atop Γ ⇒ Θ, C}

Case 7a, Θ is the empty list. Then by the induction hypothesis, we have a proof of p from γ, where p is a new variable. Substituting c for p in this proof we obtain the desired proof of c from γ. This completes case 7a.

Case 7b, Θ is not empty. Then by the induction hypothesis we have a proof in L of θ from assumptions γ, and we need a proof of i(ñ(c), θ) from γ. But i(x, (i(y, x)) is a theorem of L, provable without double negations by Lemma 1, formula (3). Applying detachment, with x = θ and y = ñ(c), we obtain the desired proof. This completes case 7b, and hence case 7.

Case 8, the last inference is by thinning in the antecedent:

{Γ ⇒ Θ \atop C, Γ ⇒ Θ}

By the induction hypothesis, we have a proof in L of θ from assumptions Γ′. That counts as a proof from assumptions C, Γ′ as well. That completes case 8.

Case 9, the last inference is by interchange in the succudent:

{Γ ⇒ Λ, C, D, Θ \atop Γ ⇒ Λ, D, C, Θ}

Case 9a, Θ and Λ are both empty. Then by the induction hypothesis we have a proof of i(ñ(c), d) and we need a proof of i(ñ(d), c). There are four subcases according as c and d are negations or not. If neither is a negation, we use the theorem i(i(n(y), x), i(n(x), y)), which is formula (4) of Lemma 1, with y = d and x = c, followed by an application of detachment. If c = n(e) and d = n(u), then we have a proof of i(e, n(u)), and we need a proof of i(u, n(e)). By formula (5) of Lemma 1, we have i(i(x, n(y)), i(y, n(x))). Applying this with x = e and y = u, and using detachment, we have the required proof. Now suppose c = n(e) but d is not a negation. Then we have a proof of i(e, d), and we need a proof of i(n(d), n(e)). Formula (6) of Lemma 1 is i(i(x, y), i(n(y), n(x))). Applying this with x = e and y = d, and using detachment, we have the required proof of i(n(d), n(e)). Finally, if d = n(u) but c is not a negation, we have a proof of i(n(c), n(u)) and need a proof of i(u, c). Formula (7) of Lemma 1 is i(i(n(x), n(y)), i(y, x)). Applying this with x = c and y = u, and using detachment, we have the required proof. This completes Case 9a.

Case 9b, Θ is empty and Λ is not empty. By the induction hypothesis, we have a proof of i(ñ(c), i(ñ(d), λ)), and we need a proof of i(ñ(d), i(ñ(c), λ)). For this we use the following theorem of L, shown in Lemma 1 to be provable without double negation:

i(i(x, i(y, z)), i(y, i(x, z))).

Take x = ñ(c), y = ñ(d), and z = λ. Applying detachment and the given proof, we obtain the desired proof.

Case 9c, Θ is not empty but Λ is empty. By Lemma 10, (C, D, Θ)′ is equivalent in L to i(ñ(θ), (C, D)′, which is i(ñ(θ), i(ñ(c), d)). By the induction hypothesis, we have a proof of this in L from γ. Similarly, (D, C, Θ)′ is i(ñ(θ), i(ñ(d), c)). What we need then is

i(i(x, i(ñ(y), z)), i(x, i(ñ(z), y))).  (25)

Because of the use of ñ, this is really four theorems, according as y and z are both negations, neither one is a negation, or one is a negation and the other is not. Those four theorems are formulas (17) through (20) of Lemma 1, so we do have (25) in L (and without the use of double negations). Applying (25) with x = γ, y = c, and z = d, and then using detachment, we obtain the required proof of i(ñ(θ, i(ñ(d), c)). This completes case 9c.

Case 9d, both Θ and Λ are nonempty. By Lemma 10, (Λ, C, D, Θ)′ is equivalent in L to i(ñ(θ), (Λ, C, D)′, which is i(ñ(θ), i(ñ(c), i(ñ(d), λ))). Similarly, (Λ, D, C, Θ is i(ñ(θ), i(ñ(d), i(ñ(c), λ))). By the induction hypothesis, we have a proof from γ of the former, and we need a proof from γ of the latter. By formula (21) of Lemma 1, we have

i(i(x, i(y, i(z, w))), i(x, i(z, i(y, w))).

Applying this with x = ñ(θ), y = ñ(c), z = ñ(d), and w = λ, and then applying detachment, we obtain the required proof. This completes case 9d, and hence Case 9.

Case 10, the last inference is by interchange in the antecedent. This just means the order of formulas in the assumption list has changed, so there is nothing to prove.

This completes the proof of part(i) of the lemma. Regarding parts (ii) and (iii): by the preceding lemma, any double negations occurring anywhere in the G-proof must occur in the final sequent. No new double negations are introduced in the translation to L, and all the theorems of L that we used (from Lemma 1) have been given double-negation-free proofs in L, found by Otter. Only in case 4b was there any use of the extra hypothesis of part (i), that the conclusion contains no double negations, and an extra argument was given in case 4b for parts (ii) and (iii). Although we may not have pointed it out in each other case and sub-case, the argument given earlier produces an L-proof in which any double negations arise from the translations into L of doubly-negated subformulas of the final sequent. In particular, if the final sequent contains no double negations, then the L-proof produced also contains no double negations.

Theorem 2 Suppose L proves A from assumptions Δ and neither Δ nor A contains double negation. Then there is a proof in L of A from Δ that does not contain double negation.

More generally, if Δ and A are allowed to contain double negation, then there is a proof in L of A from Δ that contains no new double negations. That is, all doubly-negated formulas occurring in the proof are subformulas of Δ or of A.

Remark. The theorem is also true with “triple negation” or “quadruple negation”, etc., in place of double negation. For instance, if A contains a triple negation, then it has a proof containing no double negations not already contained in A. In particular it then contains no triple negations not already contained in A, since every triple negation is a double negation.

Proof. Let A^{0} be the translation of A into G defined earlier. Double negations in A^{0} arise only from double negations in A. Since L is sound, A^{0} is a logical consequence of Δ^{0}. Hence, by completeness and Gentzen’s cut-elimination theorem, there is a proof in G of Δ^{0} ⇒ A^{0}. By the previous lemma, there is a proof in L of A^{0}′ from assumptions Δ^{0}′ that contains no new double negations. But by Lemma 9, A^{0}′ = A and Δ^{0}′ = Δ. This completes the proof.

Theorem 3 Suppose A is provable from L1-L3 using condensed detachment as the only rule of inference. Then A has a proof from L1-L3 using condensed detachment in which no doubly negated formulas occur except those that already occur as subformulas of A.

Proof . Suppose A is provable from L1-L3 using condensed detachment. Each condensed detachment step can be converted to three steps using substitution and modus ponens, so A is provable in L. By the preceding theorem, A has a proof in L in which no doubly negated formulas occur except those that already occur in A. By Theorem 1, A then has a condensed detachment proof in which no additional double negations occur. This completes the proof.

Corollary 1 Let T be any set of axioms for (two-valued) propositional logic. Suppose that there exist condensed-detachment proofs of L1-L3 from T in which no double negations occur (except those that occur in T, if any). Then the preceding theorem is true with T in place of L1-L3.

Proof . Let A be provable from T. Then A is a tautology, and hence provable from L1-L3. By the theorem, there is a proof of A from L1-L3 that contains no double negations (except those occurring in A, if any). Supplying the given proofs of L1-L3 from T, we construct a proof of A from T which contains no double negations except those occurring in T or in A (if any). That completes the proof.

Example. We can take T to contain exactly one formula, the single axiom M of Meredith. M is double-negation free, and double-negation-free proofs of L1-L3 from M have been found using Otter, one of which can be found in [8]. Therefore, the theorem is true for single axiom M.

Appendix

Here are the proofs of the formulas in Lemma 1 found with the aid of Otter. In the first column are arbitrary line numbers; in the second column are the line numbers of the major and minor premises used to derive the line by condensed detachment (or L1, L2, or L3 instead of a line number). These proofs are presented exactly as found by Otter–that is, no effort is made here to use the results of earlier proofs in the later proofs; each proof begins again from the axioms alone.

28  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
29  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
31  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
32  [L3,L2]  i(n(i(i(n(x), x), x)), y)
34  [28,28]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
40  [28,29]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
54  [31,L2]  i(x, x)
58  [L1,32]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
71  [34,40]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
94  [31,58]  i(x, i(n(i(i(n(y), y), y)), z))

107 [71,94] i(i(x, i(n(y), y)), i(z, i(x, y))) 118 [28,107] i(i(n(x), y), i(z, i(i(y, x), x))) 128 [71,118] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 141 [34,128] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 155 [128,L3] i(i(n(x), n(y)), i(y, x)) 201 [31,155] i(x, i(y, x)) 262 [141,201] i(i(x, i(y, z)), i(y, i(x, z))) 330 [262,L3] i(n(x), i(x, y)) 421 [128,330] i(i(n(x), y), i(n(y), x)) 558 [141,421] i(i(x, i(y, z)), i(i(n(y), z), i(x, z))) 731 [558,54] i(i(n(x), y), i(i(x, y), y) 1032 [731,54] i(i(x, n(x)), n(x))

That proves (1).

28  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
29  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
31  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
32  [L3,L2]  i(n(i(i(n(x), x), x)), y)
34  [28,28]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
40  [28,29]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
54  [31,L2]  i(x, x)
58  [L1,32]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
71  [34,40]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
94  [31,58]  i(x, i(n(i(i(n(y), y), y)), z))

107 [71,94] i(i(x, i(n(y), y)), i(z, i(x, y))) 118 [28,107] i(i(n(x), y), i(z, i(i(y, x), x))) 128 [71,118] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 141 [34,128] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 155 [128,L3] i(i(n(x), n(y)), i(y, x)) 201 [31,155] i(x, i(y, x)) 262 [141,201] i(i(x, i(y, z)), i(y, i(x, z))) 330 [262,L3] i(n(x), i(x, y))

332 [262,L1] i(i(x, y), i(i(z, x), i(z, y))) 421 [128,330] i(i(n(x), y), i(n(y), x)) 558 [141,421] i(i(x, i(y, z)), i(i(n(y), z), i(x, z))) 731 [558,54] i(i(n(x), y), i(i(x, y), y)) 1020 [262,731] i(i(x, y), i(i(n(x), y), y)) 1029 [731,330] i(i(x, i(x, y)), i(x, y))

That proves (2).

28  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
29  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
31  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
32  [L3,L2]  i(n(i(i(n(x), x), x)), y)
34  [28,28]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
40  [28,29]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
58  [L1,32]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
71  [34,40]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
94  [31,58]  i(x, i(n(i(i(n(y), y), y)), z))

107 [71,94] i(i(x, i(n(y), y)), i(z, i(x, y))) 118 [28,107] i(i(n(x), y), i(z, i(i(y, x), x))) 128 [71,118] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 155 [128,L3] i(i(n(x), n(y)), i(y, x)) 201 [31,155] i(x, i(y, x))

That proves (3).

28  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
29  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
31  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
32  [L3,L2]  i(n(i(i(n(x), x), x)), y)
34  [28,28]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
40  [28,29]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
58  [L1,32]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
71  [34,40]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
94  [31,58]  i(x, i(n(i(i(n(y), y), y)), z))

107 [71,94] i(i(x, i(n(y), y)), i(z, i(x, y))) 118 [28,107] i(i(n(x), y), i(z, i(i(y, x), x))) 128 [71,118] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 141 [34,128] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 155 [128,L3] i(i(n(x), n(y)), i(y, x)) 201 [31,155] i(x, i(y, x)) 262 [141,201] i(i(x, i(y, z)), i(y, i(x, z))) 330 [262,L3] i(n(x), i(x, y))

421 [128,330] i(i(n(x), y), i(n(y), x))

That proves (4).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
61  [43,L2]  i(x, x)
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 400 [254,137] i(i(x, i(n(y), n(z))), i(x, i(z, y))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 579 [40,400] i(i(n(x), y), i(i(y, n(z)), i(z, x))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1096 [633,579] i(i(n(x), y), i(i(x, n(z)), i(z, y))) 1497 [1096,61] i(i(x, n(y)), i(y, n(x)))

That proves (5).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z)))
48  [40,2]  i(i(x, y), i(i(i(x, z), u), i(i(y, z), u)))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
72  [46,48]  i(i(x, i(i(y, z), u)), i(i(y, v), i(x, i(i(v, z), u))))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))

84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 124 [L1,109] i(i(i(x, i(i(y, z), z)), u), i(i(n(z), y), u)) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 144 [124,L2] i(i(n(x), y), i(i(y, x), x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 232 [188,144] i(i(x, y), i(i(n(y), x), y)) 262 [201,137] i(n(x), i(x, y)) 309 [72,232] i(i(n(x), y), i(i(z, x), i(i(y, z), x))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 636 [422,158] i(n(i(x, n(y))), y) 1158 [309,636] i(i(x, i(y, n(z))), i(i(z, x), i(y, n(z)))) 1627 [1158,L3] i(i(x, y), i(n(y), n(x)))

That proves (6).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 137 [121,L3] i(i(n(x), n(y)), i(y, x))

That proves (7).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))

65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,4] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z)))

That proves (8).

31  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
54  [31,L2]  i(x, x)

That proves (9).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 397 [254,188] i(i(x, i(y, i(z, u))), i(x, i(z, i(y, u)))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 619 [254,422] i(i(x, i(n(y), z)), i(x, i(n(z), y))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1017 [40,619] i(i(n(x), y), i(i(y, z), i(n(z), x))) 1087 [397,633] i(i(i(n(x), y), i(z, u)), i(z, i(i(n(y), x), u)))

1447 [1087,1017] i(i(x, y), i(i(n(x), z), i(n(y), z)))

That proves (10).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 230 [L1,188] i(i(i(x, i(y, z)), u), i(i(y, i(x, z)), u)) 254 [188,2] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 300 [230,46] i(i(x, i(y, z)), i(i(u, x), i(y, i(u, z)))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 617 [300,422] i(i(x, i(n(y), z)), i(n(z), i(x, y))) 619 [254,422] i(i(x, i(n(y), z)), i(x, i(n(z), y))) 1019 [619,617] i(i(x, i(n(y), z)), i(n(i(x, y)), z))

That proves (11).

40  [2,2]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [2,3]  i(i(x, y), i(i(n(x), x), y))
43  [2,4]  i(i(i(n(x), y), z), i(x, z))
44  [4,3]  i(n(i(i(n(x), x), x)), y)

46 [40,40] i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z)))) 50 [40,41] i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z))) 61 [43,3] i(x, x) 65 [2,44] i(i(x, y), i(n(i(i(n(z), z), z)), y)) 75 [46,50] i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z)))) 84 [43,65] i(x, i(n(i(i(n(y), y), y)), z)) 97 [75,84] i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,4] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [2,158] i(i(i(x, y), z), i(y, z)) 241 [188,61] i(x, i(i(x, y), y)) 254 [188,2] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 391 [46,254] i(i(x, i(y, z)), i(i(z, u), i(x, i(y, u)))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 619 [254,422] i(i(x, i(n(y), z)), i(x, i(n(z), y))) 633 [2,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1017 [40,619] i(i(n(x), y), i(i(y, z), i(n(z), x))) 1289 [633,1017]i(i(n(x), y), i(i(x, z), i(n(z), y))) 1669 [1289,61] i(i(x, y), i(n(y), n(x))) 2034 [254,1669]i(i(x, i(y, z)), i(x, i(n(z), n(y)))) 2595 [2034,241]i(x, i(n(y), n(i(x, y)))) 3289 [391,2595]i(i(n(i(x, y)), z), i(x, i(n(y), z)))

That proves (12).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
61  [43,L2]  i(x, x)
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 230 [L1,188] i(i(i(x, i(y, z)), u), i(i(y, i(x, z)), u)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y)))

262 [201,137] i(n(x), i(x, y)) 300 [230,46] i(i(x, i(y, z)), i(i(u, x), i(y, i(u, z)))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 619 [254,422] i(i(x, i(n(y), z)), i(x, i(n(z), y))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1017 [40,619] i(i(n(x), y), i(i(y, z), i(n(z), x))) 1289 [633,1017] i(i(n(x), y), i(i(x, z), i(n(z), y))) 1669 [1289,61] i(i(x, y), i(n(y), n(x))) 2033 [300,1669] i(i(x, i(y, z)), i(n(z), i(x, n(y)))) 2461 [619,2033] i(i(x, i(y, z)), i(n(i(x, n(y))), z))

That proves (13).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
61  [43,L2]  i(x, x)
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 230 [L1,188] i(i(i(x, i(y, z)), u), i(i(y, i(x, z)), u)) 241 [188,61] i(x, i(i(x, y), y)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 300 [230,46] i(i(x, i(y, z)), i(i(u, x), i(y, i(u, z)))) 391 [46,254] i(i(x, i(y, z)), i(i(z, u), i(x, i(y, u)))) 400 [254,137] i(i(x, i(n(y), n(z))), i(x, i(z, y))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 516 [230,391] i(i(x, i(y, z)), i(i(z, u), i(y, i(x, u)))) 579 [40,400] i(i(n(x), y), i(i(y, n(z)), i(z, x))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1096 [633,579] i(i(n(x), y), i(i(x, n(z)), i(z, y)))

1497 [1096,61] i(i(x, n(y)), i(y, n(x))) 1847 [300,1497] i(i(x, i(y, n(z))), i(z, i(x, n(y)))) 2238 [1847,241] i(x, i(y, n(i(y, n(x))))) 2699 [516,2238] i(i(n(i(x, n(y))), z), i(x, i(y, z)))

That proves (14).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 397 [254,188] i(i(x, i(y, i(z, u))), i(x, i(z, i(y, u)))) 400 [254,137] i(i(x, i(n(y), n(z))), i(x, i(z, y))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 579 [40,400] i(i(n(x), y), i(i(y, n(z)), i(z, x))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1087 [397,633] i(i(i(n(x), y), i(z, u)), i(z, i(i(n(y), x), u))) 1457 [1087,579] i(i(x, n(y)), i(i(n(x), z), i(y, z)))

That proves (15).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))

75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 391 [46,254] i(i(x, i(y, z)), i(i(z, u), i(x, i(y, u)))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 615 [391,422] i(i(x, y), i(i(n(x), z), i(n(z), y))) 960 [188,615] i(i(n(x), y), i(i(x, z), i(n(y), z)))

That proves (16).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 422 [121,262] i(i(n(x), y), i(n(y), x)) 619 [254,422] i(i(x, i(n(y), z)), i(x, i(n(z), y)))

That proves (17).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
61  [43,L2]  i(x, x)
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 422 [121,262] i(i(n(x), y), i(n(y), x)) 619 [254,422] i(i(x, i(n(y), z)), i(x, i(n(z), y))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1017 [40,619] i(i(n(x), y), i(i(y, z), i(n(z), x))) 1289 [633,1017] i(i(n(x), y), i(i(x, z), i(n(z), y))) 1669 [1289,61] i(i(x, y), i(n(y), n(x))) 2034 [254,1669] i(i(x, i(y, z)), i(x, i(n(z), n(y))))

That proves (18).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y))))

137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 400 [254,137] i(i(x, i(n(y), n(z))), i(x, i(z, y)))

That proves (19).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
61  [43,L2]  i(x, x)
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 201 [L1,158] i(i(i(x, y), z), i(y, z)) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 262 [201,137] i(n(x), i(x, y)) 400 [254,137] i(i(x, i(n(y), n(z))), i(x, i(z, y))) 422 [121,262] i(i(n(x), y), i(n(y), x)) 579 [40,400] i(i(n(x), y), i(i(y, n(z)), i(z, x))) 633 [L1,422] i(i(i(n(x), y), z), i(i(n(y), x), z)) 1096 [633,579] i(i(n(x), y), i(i(x, n(z)), i(z, y))) 1497 [1096,61] i(i(x, n(y)), i(y, n(x))) 1848 [254,1497] i(i(x, i(y, n(z))), i(x, i(z, n(y))))

That proves (20).

40  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
41  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
43  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
44  [L3,L2]  i(n(i(i(n(x), x), x)), y)
46  [40,40]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))

50  [40,41]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
65  [L1,44]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
75  [46,50]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
84  [43,65]  i(x, i(n(i(i(n(y), y), y)), z))
97  [75,84]  i(i(x, i(n(y), y)), i(z, i(x, y)))

109 [40,97] i(i(n(x), y), i(z, i(i(y, x), x))) 121 [75,109] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 130 [46,121] i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y)))) 137 [121,L3] i(i(n(x), n(y)), i(y, x)) 158 [43,137] i(x, i(y, x)) 188 [130,158] i(i(x, i(y, z)), i(y, i(x, z))) 254 [188,L1] i(i(x, y), i(i(z, x), i(z, y))) 397 [254,188] i(i(x, i(y, i(z, u))), i(x, i(z, i(y, u))))

That proves (21).

References

[1] Beeson, M., and Wos, L., Appendix to Double negation in Lukasiewicz’s propositional logic, available in several electronic formats

    from http://mathcs.sjsu.edu/faculty/beeson/Papers/pubs.html.

[2] Hindley, J. R., and Meredith, D., Principal type-schemes and condensed Detachment Journal of Symbolic Logic 55, No. 1, pp. 90–105, 1990.

[3] Kalman, J. A., Condensed detachment as a rule of inference, Studia Logica LXII, No. 4, 444–451, 1983.

[4] Kleene, S. C., Introduction to Metamathematics, van Nostrand, Princeton, N. J. (1952).

[5] Mints, G., and Tammet, T., Condensed detachment is complete for relevance logic: a computer-aided proof, Journal of Automated Reasoning 7, 587–596, 1991.

[6] Prijatelj, Andreja, Bounded contraction and Gentzen-style formulation of Lukasiewicz logics, Studia Logica 57 (1996), no. 2-3, 437–456.

[7] Wos, L., and Pieper, G., A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific, Singapore (1999).

[8] Wos, L., Conquering the Meredith Single Axiom, J. Automated Reasoning, to appear in 2001.