Double Negation Elimination in Some Propositional Logics

Michael Beeson Robert Veroff Larry Wos

March 3, 2002

Abstract

We consider various propositional logics in the implication-and-negation fragment, based on the rule of inference condensed detachment, which combines modus ponens and substitution into a single inference rule. We say that such a logic L admits double negation elimination if whenever it proves a theorem B, there is a proof of B which contains no double negations not occurring in B itself. In particular, if B contains no double negations, there is a doublenegation-free proof of B. We give general conditions on a logic L under which it admits double negation elimination. We verify (with computer assistance) that these conditions are satisfied by Lukasiewicz’s propositional logic L1-L3, and by “infinite-valued” logic axiomatized by A1-A4. Moreover, these systems also admit strong double negation elimination. This means that if B^{∗} is obtained from B by erasing some double negations in B, and B is a theorem of L, then B^{∗} is also a theorem of L, and can be proved without using double negations not occurring in B^{∗}. We then take up the case of intuitionistic logic H, which does not satisfy strong double negation elimination, and show that it nevertheless does satisfy double negation elimination. The proof for H involves a translation to Genzten sequent calculus and back.

1 Introduction

In logic, merited emphasis is placed on the nature of various axiom systems, the number of members, the length (individually and collectively), the number of distinct letters (variables), the total number of occurrences of various function symbols, and other measures of the “simplicity” of a proof. To mention but one of many examples, in the mid-1930s J. Lukaksiewicz discovered a 23-letter single axiom for two-valued sentential (or propositional) calculus. In the early 1950s, C. A. Meredith found a 21-letter single axiom. Whether a still shorter single axiom for this area of logic exists is currently unknown. Concerns for the properties of axiom systems are mirrored in concerns for properties of proofs: length, complexity, size, lemma dependence, and (of particular relevance to this article) term structure.

Although it was unknown until recently, Hilbert considered a twenty-fourth problem for inclusion in the famous list of twenty-three important problems that he presented at the beginning of the twentieth century. This twenty-fourth problem focused on the importance of finding simpler proofs. Apparently Hilbert did not include the problem in his final list because of the difficulty of defining “simpler” precisely.

Ceteris paribus, the avoidance of a class of terms makes a proof simpler, as when a proof is free of doubly negated subformula. This paper, in the spirit of Hilbert’s twenty-fourth problem, takes up this specific form of simplicity, and asks for general sufficient conditions on a system of propositional logic L, that would guarantee that doubly negated formulas which do not occur in the theorem, are not needed in the proof.

Although propositional calculus is one of the oldest areas of logic, not all of its mysteries have been unlocked. 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 23-symbol 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. The theorems we prove here about double negation elimination not only have an intrinsic, aesthetic appeal in that they show the possibility of simplifying proofs, but they also are of interest because they justify a shortcut in automated proof-search methods, namely: discard double negations that do not occur in the goal.

We shall work with logics formulated using only the two connectives, implication and negation. There are several notations in use for propositional logic which we want to mention before continuing. First, one can use infix → for implication and prefix ¬ for negation. For example we could write x → (¬x → y). Many papers on propositional logic use Polish notation, in which C is used for implication (conditional) and N for negation. The same formula would then be rendered as CxCNxy. Finally, the notation which is easiest when using Otter is prefix, with parentheses. We use i(x, y) for implication and n(x) for negation, so the example formula becomes i(x, i(n(x), y)). In this paper we use the latter notation exclusively, because it permits us to cut-and-paste machine-produced proofs, eliminating errors of transcription. We make use of the theorem-proving program Otter [5] to produce proofs in various propositional logics, which we use to verify that those logics satisfy the hypotheses of our general theorems on double negation elimination.

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 [11]. 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 rule to be used with these axioms is known as condensed detachment. This is a rule that combines substitution and modus ponens. 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. Condensed detachment has premisses i(p, q) and r, where p and r unify–that is, there is a substitution σ which makes pσ = rσ. In that case, and provided σ is the most general such substitution, the conclusion of condensed detachment is qσ. This inference rule requires renaming of variables in the premises before the unification, to avoid unintended clashes of variables.^{1}

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, not only for Lukasiewicz’s system L1-L3, but for other axiomatizations of ordinary propositional logic, and other systems of logic entirely, such as “infinite-valued logic”.

We would like to thank Kenneth Harris, Branden Fitelson, and Ted Ulrich, for their attention to early drafts of this paper. In addition, Ulrich contributed part of the proof of D1-D3 from L1-L3.

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. A technicality arises as to whether it is permitted, required, or forbidden to rename the variables of the premisses before applying condensed detachment. The definition on p. 212 of [11] does not mention renaming, and read literally would not allow it, but the implementation in Otter requires it, and [9] explicitly permits it. If it is not permitted, then by renaming variables in the entire proof of the premiss, we obtain a proof of the renamed premiss, using alphabetic variants of the axioms, so the same formulas will be provable in either case. Similarly, renaming of variables in conclusions is allowed. Technically, we could wait until the conclusions are used before renaming them, but in practice, Otter renames variables in each conclusion as it is derived.

2 Condensed detachment

We remind the reader that the systems of primary interest in this paper use condensed detachment as their sole rule of inference. 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(α, α). 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, 6]. The following three formulas will play an important role:

D1  i(x, x)
D2  i(i(x, x), i(n(x), n(x)))
D3  i(i(x, x), i(i(y, y), i(i(x, y), i(x, y))))

Lemma 1 Suppose L is any system of propositional logic with condensed detachment as the sole inference rule, and suppose that there are double-negation-free proofs of D1-D3 in L. Then every formula of the form i(α, α) is provable from L by condensed detachment, without using double negations except those occurring as subformulas of α.

Proof . We prove by induction on the complexity of the propositional formula α that for each α, the formula i(α, α) is provable in L by condensed detachment. The base case, when α is a proposition letter, follows by replacing x by α in the proof of i(x, x). Any line of the proof that is an axiom becomes an alphabetic variant of that axiom, which is still considered an axiom. Actually, in view of the convention that renaming variables in the conclusion is allowed, it would be enough just to replace x by α in the last line of the proof. If we have a proof of i(β, β) then we can apply condensed detachment and D2 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 D3 and get a proof of i(i(α, β), i(α, β)). That completes the proof of the lemma.

Lemma 2 If A is an instance of C, then the result of applying CD to i(A, B) and C is B (or an alphabetic variant of B).

Proof : Rename variables in C if necessary so that C and A have no variables in common. Let σ be a most general unifier of A and C. Then the result of applying condensed detachment to i(A, B) and C is Bσ.

Let τ be a most general substitution such that Cτ = A; since A is assumed to be an instance of C such a τ exists. Since the variables of C do not occur in A or B, Bτ = B and Aτ = A. Then Cτ = A = Aτ, so τ = σρ for some substitution ρ. Then B = Bτ = Bσρ. Thus σρ is the identity on B. Hence σρ is the identity on each variable occurring in B. Hence σ and ρ do nothing but (possibly) rename variables. Hence Bσ, which is the result of this application of condensed detachment, is B or an alphabetic variant of B. That completes the proof of the lemma.

Lemma 3 Suppose L is a logic proving D1-D3 by condensed detachment without double negation. Then each substitution instance α of an axiom of L is provable by condensed detachment without using double negations, except those double negations occurring as subformulas of α, if any.

Proof . Let α be a substitution instance of an axiom A. Renaming the variables in the axiom A if necessary, we may assume that the variables occurring in A do not occur in α. By Lemma 1, i(α, α) is provable by condensed detachment, without using any double negations except possibly those already occurring in α. By Lemma 2, the result of applying condensed detachment to i(α, α) and A is α or an alphabetic variant ασ of α. If it is not literally α, we can rename variables in the conclusion (or if one prefers to avoid renaming conclusions, throughout the entire proof) to create a proof of α. This completes the proof of the lemma.

A proof of B in L from assumptions Γ is defined as usual: lines of the proof are either inferred from previous lines, or are axioms, or belong to Γ. However, when condensed detachment is used as a rule of inference, we have to distinguish between (propositional) variables, which occur in the axioms, and specific (constant) proposition letters, which occur in assumptions. For example, if we have i(n(n(x)), x) as an axiom, then we can derive any substitution instance of that formula, but if we have i(n(n(a)), a) as an assumption, we cannot use it to derive an instance with some other formula substituted for a.

The following theorem is the easy half of the relation between condenseddetachment proofs and modus ponens proofs. The sense of the theorem is that substitutions can be pushed back to the axioms.

Theorem 1 (Pushback Theorem) Let L be a system of propositional logic, and suppose L proves B using condensed detachment, or using modus ponens and substitution. Then there exists a proof of B using modus ponens from substitution instances of axioms of L. Similarly if L proves B from assumptions Δ there exists a proof of B using modus ponens from Δ and substitution instances of axioms of L.

Remark. It would not make sense to speak of substitution instances of Δ since assumptions cannot contain variables, as explained above. Proof. First we prove the theorem in case the given proof uses modus ponens and substitution. We proceed by induction on the length of the given proof of B. If the length is zero then B is an axiom or assumption, and there is nothing to prove. If the last inference is by modus ponens, say B is inferred from i(A, B) and A, then by the induction hypothesis there are proofs of these premises from substitution instances of axioms, and adding the last inference, we obtain the desired proof of B.

If the last inference is by substitution, say B = Aσ is inferred from A, then by the induction hypothesis there is a proof π of A using modus ponens only from substitution instances of axioms. Apply the substitution σ to every line of π; the result is the desired proof of B. If there are assumptions, they are unaffected by σ since they do not contain variables.

Now suppose the original proof uses condensed detachment. Each condensed detachment inference can be broken into two substitutions and a modus ponens, so a condensed detachment proof gives rise to a modus ponens and substitution proof, and we can apply the previous part of the proof. That completes the proof.

Lemma 4 Suppose L is a logic proving formulas D1-D3 by condensed detachment without double negation,and suppose that the axioms of L contain no double negations. If A is provable in L with condensed detachment and σ is any substitution, then Aσ is provable in L by condensed detachment.

Proof . By induction on the length of the proof π of A in L, we prove that the statement of the lemma is true for all substitutions σ. The base case occurs when A is an axiom, so Aσ is a substitution instance of an axiom. By Lemma 3, Aσ is provable in L by condensed detachment, and any double negations occurring in the proof occur already in Aσ.

For the induction step, suppose the last inference of the given proof π has 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σ. This completes the proof of the lemma.

Theorem 2 (D-completeness) Suppose L is a logic which proves formulas D1-D3. If L proves A using modus ponens and substitution, then L proves A using condensed detachment.

Remark. Note that we cannot track what happens to double negations in this proof. The proof does not guarantee that passing from substitution to condensed detachment will not introduce new double negations. Somewhat to our surprise, we do not need any such result to prove double negation elimination, and quite the reverse, we shall derive such a result from double negation elimination. Proof . By Theorem 1, there is a proof π of A from substitution instances of axioms, using modus ponens as the only rule of inference. By Lemma 3, there are condensed-detachment proofs of these substitution instances of axioms. Since modus ponens is a special case of condensed detachment, if we string together the condensed detachment proofs of the instances of axioms required, followed by the proof π, we obtain a condensed detachment proof of A. That completes the proof of the theorem.

3 The main theorem

Let L be a system of propositional logic, given by some axioms and the sole inference rule of condensed detachment. Let L* be the system of logic whose axioms are the closure of (the axioms of) L under applications of the following syntactic rule: If x is a proposition letter, and subterm n(x) appears in a formula A, then construct a new formula by replacing each occurrence of x in A by n(x) and cancelling any double negations that result. In other words, we pick a set S of proposition letters occurring negated in A, and replace each occurrence of a variable x in S throughout A by n(x), cancelling any doubly negated propositions. The first description of L* calls for replacing all occurrences of only one variable, but if we repeat that operation we can in effect replace a subset.

An example will make the definition of L* clear. If this procedure is applied to the axiom

i((i(n(x), n(y)), i(y, x))

we obtain the following three new axioms (by replacing first both x and y, then only y, then only x):

A6  i(i(x, y), i(n(y), n(x)))
A7  i(i(n(x), y), i(n(y), x))
A8  i(i(x, n(y)), i(y, n(x)))

We say that L admits double negation elimination if whenever L proves a theorem B, there exists a proof of B in L such that any double negations occurring as subformulae of the proof, already occur as subformulae of B. In particular, double-negation-free theorems have double-negation-free proofs.

We say that L admits strong double negation elimination if whenever L proves a theorem B, and B^{∗} is obtained from B by erasing some of the double negations in B, then there is a proof of B^{∗} in L, and moreover, there is a proof of B^{∗} in L which contains only doubly-negated formulae occurring in B^{∗}. To be more precise about B^{∗}, if some doubly negated subformulas occur more than once in B, one must erase all or none of those double negations. That is, B^{∗} is obtained from B by replacing all occurrences of some doubly-negated subformulas n(n(q)) in B by q.

Theorem 3 Suppose that in L there are double-negation-free proofs of D1-D3, and double-negation-free proofs of all the axioms of L*. Then L admits strong double negation elimination.

Remark. The theorem is also true with “triple negation” or “quadruple negation”, etc., in place of double negation. For instance, if B contains a triple negation, then it has a proof containing no double negations not already contained in B. In particular it then contains no triple negations not already contained in B, since every triple negation is a double negation. Proof. Suppose B is provable in L. If B contains any double negations, select arbitrarily a subset of the doubly negated subformula of B, and form B^{∗} by replacing each of these formulas n(n(q)) by q. Of course, B^{∗} may still contain double negations; if we are only proving double negation elimination and not strong double negation elimination, we take B^{∗} to be B. By Theorem 1, there is a modus ponens proof of B from substitution instances of axioms. If this proof contains any double negations which do not occur in B^{∗}, we simply erase them. This erasure takes a modus ponens step into another legal modus ponens step. Note that one cannot “simple erase” double negations in a condenseddetachment proof; but now we have a modus ponens proof, and double negations can be erased in modus ponens proofs. At axioms, it transforms a substitution instance of an axiom of L into a substitution instance of an axiom of L*. Thus, we have a proof of B^{∗} from substitution instances of axioms of L* which does not contain any double negations except those which occur in B^{∗}. By Lemma 3, there are condensed detachment proofs of these substitution instances of L* (from axioms of L*). By hypothesis, the axioms of L* have double-negation-free proofs in L. We now construct the desired proof as follows: first write down the double-negation free proofs of the axioms of L*. Then write down proofs of the substitution instances of axioms of L* which are required. This much provides proofs of all the substitution instances of axioms of L*, from L rather than from L*. Now write down the proof of B^{∗} from those substitution instances. That is the desired proof. The only double negations it contains are those contained in B^{∗}. That completes the proof of the theorem.

Theorem 4 (Strong d-completeness) Suppose L is a logic which admits strong double negation elimination. If L proves A using modus ponens and substitution, without using double negations except those that occur as subformulae of A, then L proves A using condensed detachment, without using double negations except those that occur as subformulae of A.

Proof : Suppose L proves A using modus ponens and substitution. Then by Theorem 2, there is a condensed detachment proof of A (possibly using new double negations). By strong double negation elimination, there is a condensed detachment proof of A in L, using only double negations that occur as subformulae of A.

4 Lukasiewicz’s system L1-L3

As mentioned in the introduction, this system has the 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))

Lemma 5 L1-L3 prove formulas D1-D3. Proof . Formula D1 is i(x, x). Here is a two-line proof produced by Otter:

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

Formula D2 is proved by first proving some auxiliary formulas D4 and D5:

D4  i(i(x, i(x, y)), i(x, y))
D5  i(i(x, y), i(n(y), n(x)))

Here is an Otter proof of D4 from L1-L3:

30  [L3,L2]  i(n(i(i(n(x), x), x)), y)
31  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
32  [L1,30]  i(i(x, y), i(n(i(i(n(z), z), z)), y))
33  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
34  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
35  [33,L2]  i(x, x)
36  [32,33]  i(x, i(n(i(i(n(y), y), y)), z))
37  [31,31]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
38  [31,34]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
39  [38,37]  i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z))))
40  [39,36]  i(i(x, i(n(y), y)), i(z, i(x, y)))
41  [40,31]  i(i(n(x), y), i(z, i(i(y, x), x)))
42  [41,39]  i(i(x, i(y, z)), i(i(n(z), y), i(x, z)))
43  [42,37]  i(i(x, i(n(y), z)), i(i(u, i(z, y)), i(x, i(u, y))))
44  [42,L3]  i(i(n(x), n(y)), i(y, x)))
45  [44,33]  i(x, i(y, x))
46  [43,45]  i(i(x, i(y, z)), i(y, i(x, z)))
47  [46,L3]  i(n(x), i(x, y))
49  [47,42]  i(i(n(x), y), i(n(y), x))
50  [49,43]  i(i(x, i(y, z)), i(i(n(y), z), i(x, z)))
51  [50,35]  i(i(n(x), y), i(i(x, y), y))
53  [51,47]  i(i(x, i(x, y)), i(x, y))

Here is an Otter proof of D5 from L1-L3:

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)))

Now we are ready to prove D2. This proof was found by Ted Ulrich, without machine assistance.

44 [D4,L1] i(i(x, x), i(x, x)) 45 [L1,D5] 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)))

Finally, we are ready to prove D3. The following proof was found using a specially compiled version of Otter. (The difficulty is that normal Otter derives a more general conclusion, which subsumes the desired conclusion.)

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))))

That completes the proof of the lemma. Theorem 5 Lukasiewicz’s system L1-L3 admits strong double negation elimination. Proof. We begin by calculating the formulas L* for this system. We obtain the following:

L4  i(i(x, n(x)), n(x))
L5  i(n(x), i(x, y))

By Theorem 3 it suffices to verify that there are double-negation-free proofs of L4,L5, and D1-D3. We have already verified D1-D3 above, so it only remains to exhibit double-negation-free proofs of L4 and L5. Here is an Otter proof of L4:

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))

Here is an Otter proof of L5:

19  [L1,L1]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
20  [L1,L2]  i(i(x, y), i(i(n(x), x), y))
22  [L1,L3]  i(i(i(n(x), y), z), i(x, z))
23  [L3,L2]  i(n(i(i(n(x), x), x)), y)
25  [19,19]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
31  [19,20]  i(i(x, y), i(i(n(i(y, z)), i(y, z)), i(x, z)))
77  [L1,23]  i(i(x, y), i(n(i(i(n(z), z), z)), y))

207 [25,31] i(i(x, i(n(i(y, z)), i(y, z))), i(i(u, y), i(x, i(u, z)))) 234 [22,77] i(x, i(n(i(i(n(y), y), y)), z)) 265 [207,234] i(i(x, i(n(y), y)), i(z, i(x, y))) 287 [19,265] i(i(n(x), y), i(z, i(i(y, x), x))) 297 [207,287] i(i(x, i(y, z)), i(i(n(z), y), i(x, z))) 389 [297,L3] i(i(n(x), n(y)), i(y, x)) 439 [22,389] i(x, i(y, x))

522 [L1,439] i(i(i(x, y), z), i(y, z)) 590 [522,389] i(n(x), i(x, y))

That completes the proof of the theorem.

Corollary 1 Let T be any set of axioms for (two-valued) propositional logic. Suppose that there exist double-negation-free condensed-detachment proofs of L1-L3 from T. Then the preceding theorem is true with T in place of L1-L3.

Proof . We must show T admits strong double-negation elimination. Let A be provable from T, and let A∗ be obtained from A by erasing some of the double negations in A (but all occurrences of any given formula, if there are multiple occurrences of the same doubly-negated subformula). We must show that T proves A∗ by a proof whose doubly-negated subformula occur in A∗. Since T is an axiomatization of two-valued logic, 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 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 [13]. Therefore, the theorem is true for the single axiom M.

5 Infinite-valued logic

Lukasiewicz’s infinite-valued logic is a subsystem of classical propositional logic which was studied in the 1930s. It is of interest partly because there is a natural semantics for it, according to which propositions are assigned truth values which are real (or rational) numbers between 0 and 1, with 1 being true and 0 being false. Lukasiewicz’s axioms A1-A4 are complete for this semantics, as was proved (but apparently not published) by Wasjberg, and proved again by Chang [1]. Axioms A1-A4 are formulated using implication i(p, q) and negation n(p) only. Truth values are given by

∥n(p)∥ = 1 − ∥p∥
∥i(p, q)∥ = min(1 − ∥p∥ + ∥q∥, 1).

Axioms A1-A4 are as follows^{2}

i(x, i(y, x))  (A1)
i(i(x, y), i(i(y, z), i(x, z)))  (A2)

2A comparison with Lukasiewicz’s axioms L1-L3: Note that axiom A2 is the same as L1, and A4 is the same as L3, but L2 is not provable from A1-A4.

i(i(i(x, y), y), i(i(y, x), x))  (A3)
i(i(n(x), n(y)), i(y, x))  (A4)

The standard reference for infinite-valued logic is [8].

Lemma 6 A1-A4 prove formulas D1-D3 without double negation.

Proof . Here is an Otter proof of D1 from A1-A4:

24  [A2,A1]  i(i(i(x, y), z), i(y, z))
32  [24,A3]  i(x, i(i(x, y), y))
59  [A2,32]  i(i(i(i(x, y), y), z), i(x, z))

113 [59,24] i(x, i(y, y)) 118 [113,113] i(x, x)

Here is an Otter proof of D2 from A1-A4, found using a specially compiled version of Otter.

118  [A1,A1]  i(x, i(y, i(z, y)))
119  [A2,A2]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
121  [A2,A1]  i(i(i(x, y), z), i(y, z))
122  [A2,A3]  i(i(i(i(x, y), y), z), i(i(i(y, x), x), z))
126  [A3,118]  i(i(i(x, i(y, x)), z), z)
139  [121,A4]  i(n(x), i(x, y))
140  [121,A3]  i(x, i(i(x, y), y))
143  [A2,139]  i(i(i(x, y), z), i(n(x), z))
148  [A2,140]  i(i(i(i(x, y), y), z), i(x, z))

179 [121,126] i(x, x) 185 [140,179] i(i(i(x, x), y), y) 214 [A3,185] i(i(x, i(y, y)), i(y, y)) 235 [122,119] i(i(i(i(x, y), i(z, y)), i(z, y)), i(i(x, z), i(x, y))) 385 [119,148] i(i(x, i(y, z)), i(y, i(x, z))) 395 [148,A3] i(x, i(i(y, x), x)) 591 [385,395] i(i(x, y), i(y, y)) 598 [591,591] i(i(x, x), i(x, x)) 628 [591,118] i(i(x, i(y, x)), i(x, i(y, x))) 645 [143,598] i(n(x), i(x, x)) 646 [121,628] i(i(x, y), i(y, i(x, y))) 647 [646,645] i(i(x, x), i(n(x), i(x, x))) 648 [119,214] i(i(x, y), i(x, x)) 648 [A1,648] i(x, i(i(y, z), i(y, y))) 650 [235,649] i(i(x, i(y, z)), i(x, i(y, y))) 651 [650,647] i(i(x, x), i(n(x), n(x)))

Here is a proof of D3, found using a specially compiled version of Otter.

30  [A1,A1]  i(x, i(y, i(z, y)))
31  [A2,A2]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
32  [A2,A1]  i(i(i(x, y), z), i(y, z))
33  [31,31]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
34  [31,L2]  i(i(x, y), i(i(i(x, z), u), i(i(y, z), u)))
35  [32,31]  i(i(x, y), i(z, i(x, z)))
36  [32,A4]  i(n(x), i(x, y))
37  [32,A1]  i(x, i(y, i(z, x)))
38  [34,33]  i(i(x, i(i(y, z), u)), i(i(y, v), i(x, i(i(v, z), u))))
39  [36,35]  i(x, i(n(y), x))
40  [39,30]  i(n(x), i(y, i(z, i(u, z))))
41  [A3,32]  i(x, i(i(x, y), y))
42  [41,33]  i(i(x, i(y, z)), i(y, i(x, z)))
43  [42,A2]  i(i(i(x, i(y, z)), u), i(i(y, i(x, z)), u))
44  [42,A1]  i(x, i(y, y))
45  [44,37]  i(x, i(y, i(z, i(u, u))))
46  [44,A3]  i(i(i(x, x), y), y)
47  [46,A3]  i(i(x, i(y, y)), i(y, y))
48  [47,45]  i(i(x, i(y, y)), i(x, i(y, y)))
49  [47,40]  i(i(x, i(y, x)), i(x, i(y, x)))
50  [48,43]  i(i(x, i(y, x)), i(y, i(x, x)))
51  [49,38]  i(i(x, i(i(y, z), u)), i(i(y, y), i(x, i(i(y, z), u))))
52  [50,A2]  i(i(x, x), i(i(y, x), i(y, x)))
53  [52,51]  i(i(x, x), i(i(y, y), i(i(x, y), i(x, y))))

Theorem 6 The system of “infinite-valued logic” A1-A4 admits strong double negation elimination.

Proof. We begin by calculating the formulas L* for this system. The only axiom containing negations is A3, but there are three possible replacements, so we get three new axioms A6-A8 as follows.^{3}

A6  i(i(x, y), i(n(y), n(x)))
A7  i(i(n(x), y), i(n(y), x))
A8  i(i(x, n(y)), i(y, n(x)))

By Theorem 3 it suffices to verify that there are double-negation-free proofs of A6, A7, A8, and D1-D3. We have already verified D1-D3 above, so it only remains to exhibit double-negation-free proofs of A6-A8.

Here is an Otter proof of A6:

3The name A5 is already in use for another formula, originally used as an axiom along with A1-A4, but later shown to be provable from A1-A4.

81  [A1,A1]  i(x, i(y, i(z, y)))
82  [A2,A2]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
84  [A2,A1]  i(i(i(x, y), z), i(y, z))
87  [A2,A4]  i(i(i(x, y), z), i(i(n(y), n(x)), z))
89  [A3,81]  i(i(i(x, i(y, x)), z), z)
92  [82,82]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
95  [82,A2]  i(i(x, y), i(i(i(x, z), u), i(i(y, z), u)))
99  [84,A4]  i(n(x), i(x, y))

100 [84,A3] i(x, i(i(x, y), y)) 112 [87,89] i(i(n(x), n(i(y, i(z, y)))), x) 148 [95,99] i(i(i(n(x), y), z), i(i(i(x, u), y), z))) 149 [92,99] i(i(x, y), i(n(y), i(x, z))) 154 [92,100] i(i(x, i(y, z)), i(y, i(x, z))) 291 [154,95] i(i(i(x, y), z), i(i(x, u), i(i(u, y), z))) 296 [154,A2] i(i(x, y), i(i(z, x), i(z, y))) 450 [92,296] i(i(x, i(y, z)), i(i(z, u), i(x, i(y, u)))) 566 [450,149] i(i(i(x, y), z), i(i(x, u), i(n(u), z))) 791 [566,112] i(i(n(x), y), i(n(y), x)) 998 [148,791] i(i(i(x, y), z), i(n(z), x)) 1109 [291,998] i(i(i(x, y), z), i(i(z, u), i(n(u), x))) 1186 [1109,112] i(i(x, y), i(n(y), n(x)))

Here is an Otter proof of A7:

81  [A1,A1]  i(x, i(y, i(z, y)))
82  [A2,A2]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
84  [A2,A1]  i(i(i(x, y), z), i(y, z))
87  [A2,A4]  i(i(i(x, y), z), i(i(n(y), n(x)), z))
89  [A3,81]  i(i(i(x, i(y, x)), z), z)
92  [82,82]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
99  [84,A4]  i(n(x), i(x, y))

100 [84,A3] i(x, i(i(x, y), y)) 112 [87,89] i(i(n(x), n(i(y, i(z, y)))), x) 149 [92,99] i(i(x, y), i(n(y), i(x, z))) 154 [92,100] i(i(x, i(y, z)), i(y, i(x, z))) 296 [154,A2] i(i(x, y), i(i(z, x), i(z, y))) 450 [92,296] i(i(x, i(y, z)), i(i(z, u), i(x, i(y, u))))) 566 [450,149] i(i(i(x, y), z), i(i(x, u), i(n(u), z))) 791 [566,112] i(i(n(x), y), i(n(y), x))

Here is an Otter proof of A8:

81  [A1,A1]  i(x, i(y, i(z, y)))
82  [A2,A2]  i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u))
84  [A2,A1]  i(i(i(x, y), z), i(y, z))

87  [A2,A4]  i(i(i(x, y), z), i(i(n(y), n(x)), z))
89  [A3,81]  i(i(i(x, i(y, x)), z), z)
92  [82,82]  i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z))))
95  [82,A2]  i(i(x, y), i(i(i(x, z), u), i(i(y, z), u)))
99  [84,A4]  i(n(x), i(x, y))

100 [84,A3] i(x, i(i(x, y), y)) 112 [87,89] i(i(n(x), n(i(y, i(z, y)))), x) 148 [95,99] i(i(i(n(x), y), z), i(i(i(x, u), y), z)) 149 [92,99] i(i(x, y), i(n(y), i(x, z))) 154 [92,100] i(i(x, i(y, z)), i(y, i(x, z))) 291 [154,95] i(i(i(x, y), z), i(i(x, u), i(i(u, y), z))) 296 [154,A2] i(i(x, y), i(i(z, x), i(z, y))) 450 [92,296] i(i(x, i(y, z)), i(i(z, u), i(x, i(y, u)))) 554 [82,450] i(i(x, y), i(i(z, u), i(i(y, z), i(x, u)))) 566 [450,149] i(i(i(x, y), z), i(i(x, u), i(n(u), z))) 791 [566,112] i(i(n(x), y), i(n(y), x)) 998 [148,791] i(i(i(x, y), z), i(n(z), x)) 1109 [291,998] i(i(i(x, y), z), i(i(z, u), i(n(u), x))) 1186 [1109,112] i(i(x, y), i(n(y), n(x))) 1207 [554,1186] i(i(x, y), i(i(i(n(z), n(u)), x), i(i(u, z), y))) 1409 [1207,A4] i(i(i(n(x), n(y)), i(n(z), n(u))), i(i(y, x), i(u, z))) 1561 [1409,791] i(i(x, n(y)), i(y, n(x)))

This completes the proof of the theorem.

6 An example

One of the motivations for this work was the existence of an example of a formula which is double-negation-free, and provable from A1-A4, but for which Wos had been unable to find a double-negation-free proof. The formula in question is

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

Wos could provide a proof with 45 condensed-detachment steps of this theorem, 10 of whose lines involved a double negation. Beeson used this proof as input to a computer program implementing the algorithms implicit in the proof of our main theorem. The output of this program was a double-negation-free proof by modus ponens of the example, from substitution instances of A1-A4. The proof was surprising by its length and size. It was 796 lines long, and many of its lines were thousands of symbols long. The input proof takes about 3.5 kilobytes, the output proof about 200 kilobytes. Now we know what the condensed means in “condensed detachment”! The expansion in size is due to making the substitutions introduced by condensed detachment explicit. The expansion in length is due to duplications of multiply-referenced lines, which must be done before the substitutions are “pushed upwards” in the proof. In other words, one line of the proof can be referenced several times, and when the proof is converted to tree form, each reference will require a separate copy of the referenced line. This 796-line proof, considered as a tree, has substitution instances of the axioms at the leaves. After obtaining this proof, we could have continued with the algorithm, providing proofs of the substitution instances of the axioms. That would have substantially increased the length. Instead, Bill McCune put the lines of the 796-line proof into an Otter input file as “hints”, and Otter produced a 27-line double-negation free condensed-detachment proof of DN1 from A1-A4 and A6-A8. This run generates some 6000 formulae and takes between 0.5 and 2 hours, depending on what machine is used. If the lines of this proof, together with the proofs of A6-A8, are supplied as resonators in a new input file, Otter can then find a 41-step proof of DN1 from A1-A4. “Hints” are explained in [10]. Resonators are explained in [12].

7 D-completeness of intuitionistic logic

Let H be the following formulation of intuitionistic propositional calculus in terms of implication and negation, denoted by i and n:

H1  i(x, i(y, x))
H2  i(i(x, i(y, z)), i(i(x, y), i(x, z)))
H3  i(i(x, n(x)), n(x))
H4  i(x, i(n(x), y))

The inference rules of H are modus ponens and substitution. It is also possible to consider H1-H4 with condensed detachment. These two systems have the same theorems, as will be shown in detail below.

Lemma 7 D1-D3 have double-negation-free condensed-detachment proofs from H1-H4.

Proof : Here is a double-negation-free condensed-detachment proof of D1 from H1-H4 (found by hand):

5  [H2,H1]  i(i(x, y), i(x, x))
6  [5,H1]  i(x, x)

D2 is i(i(x, x), i(n(x), n(x))). Here is a double-negation-free condenseddetachment proof of D2 from H1-H4, found using a specially-compiled version of Otter. Curiously, H3 is not used.

94  [H1,H1]  i(x, i(y, i(z, y)))
95  [H2,H2]  i(i(i(x, i(y, z)), i(x, y)), i(i(x, i(y, z)), i(x, z)))

97  [H2,H1]  i(i(x, y), i(x, x))

100 [H2,H4] i(i(x, n(x)), i(x, y)) 107 [H1,94] i(x, i(y, i(z, i(u, z)))) 111 [95,94] i(i(x, i(i(y, x), z)), i(x, z)) 113 [95,97] i(i(x, i(x, y)), i(x, y)) 116 [H1,97] i(x, i(i(y, z), i(y, y))) 213 [H2,116] i(i(x, i(y, z)), i(x, i(y, y))) 220 [H1,100] i(x, i(i(y, n(y)), i(y, z))) 753 [95,113] i(i(x, i(x, x)), i(x, x)) 783 [753,116] i(i(x, x), i(x, x)) 785 [753,107] i(i(x, i(y, x)), i(x, i(y, x))) 833 [783,213] i(i(x, i(y, y)), i(x, i(y, y))) 903 [785,94] i(i(x, y), i(y, i(x, y))) 1541 [111,220] i(n(x), i(x, y)) 1563 [833,1541] i(n(x), i(x, x)) 1605 [903,1563] i(i(x, x), i(n(x), i(x, x))) 1706 [213,1605] i(i(x, x), i(n(x), n(x)))

Here is a double-negation-free condensed-detachment proof of D3 from H1-H4. Again H3 is not used.

177  [H1,H1]  i(x, i(y, i(z, y)))
178  [H2,H2]  i(i(i(x, i(y, z)), i(x, y)), i(i(x, i(y, z)), i(x, z)))
179  [H1,H2]  i(x, i(i(y, i(z, u)), i(i(y, z), i(y, u))))
180  [H2,H1]  i(i(x, y), i(x, x))

194 [178,177] i(i(x, i(i(y, x), z)), i(x, z)) 196 [178,180] i(i(x, i(x, y)), i(x, y)) 273 [2,194] i(x, i(i(y, i(i(z, y), u)), i(y, u))) 275 [194,179] i(i(x, y), i(i(z, x), i(z, y))) 310 [3,275] i(i(i(x, y), i(z, x)), i(i(x, y), i(z, y))) 351 [194,273] i(i(i(x, y), z), i(y, z)) 442 [351,310] i(i(x, y), i(i(y, z), i(x, z))) 655 [442,442] i(i(i(i(x, y), i(z, y)), u), i(i(z, x), u)) 1010 [655,655] i(i(x, i(y, z)), i(i(u, y), i(x, i(u, z)))) 1036 [655,442] i(i(x, y), i(i(i(x, z), u), i(i(y, z), u))) 1355 [1010,1036] i(i(x, i(i(y, z), u)), i(i(y, v), i(x, i(i(v, z), u)))) 2170 [196,275] i(i(x, x), i(x, x)) 2188 [275,2170] i(i(x, i(y, y)), i(x, i(y, y))) 2211 [2170,177] i(i(x, i(y, x)), i(x, i(y, x))) 2335 [2188,275] i(i(x, x), i(i(y, x), i(y, x))) 2404 [2211,1355] i(i(x, i(i(y, z), u)), i(i(y, y), i(x, i(i(y, z), u)))) 2537 [2404,2335] i(i(x, x), i(i(y, y), i(i(x, y), i(x, y))))

Theorem 7 The same theorems are provable from H1-H4, when we take condensed detachment as the sole rule of inference, as when we take modus ponens and substitution as rules of inference. Moreover, if b is provable without double negations by modus ponens from substitution instances of axioms, then there is a double-negation-free condensed detachment proof of b.

Remark. The present proof gives no assurance that a general H proof, using substitution arbitrarily and not just in axioms, can be converted to a condenseddetachment proof without introducing additional double negations. That in general it can be will follow from Theorem 8 below. Proof : The first claim is an immediate consequence of Theorem 2 and Lemma 7. To prove the second claim, suppose b has a double-negation-free modus ponens proof from substitution instances of axioms. By Lemma 3, we can supply double-negation-free condensed-detachment proofs of the substitution instances of axioms which are used in the proof. Adjoining these proofs, we obtain a double-negation-free condensed detachment proof of b as required.

8 H 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 of Lemma 12 below. We shall use the notation Γ ⇒ Δ for a sequent. We remind the reader that what distinguishes intuitionistic from classical sequent calculus is that the consequent Δ in a sequent Γ ⇒ Δ in the intuitionistic calculus is restricted to contain at most one formula.^{4}

We give a translation of H into G.Namely, if A is a formula of H, 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 H in the following manner. First we assign to each formula A of G a corresponding formula A′ of H, given by

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

4The translations given here can also be given for Lukasiewicz’s logic L1-L3, but many additional complications are introduced by the necessity of translating a sequent containing more than one formula, and in view of the simpler proofs of double negation elimination given above, we treat the Gentzen translation only for intuitionistic logic. Note that we used Otter only for the H-proofs of D2 and D3; but if we treat L this way instead of H, we need Otter for twenty-one additional lemmas.

where again A′ = A for proposition letters A. We need to define Γ′ also, where Γ is a list of formulas; since we are treating only the intuitionistic calculus, we need this definition only for lists occurring on the left of ⇒. If Γ = A_{1}, …, A_{n} is a list of formulas occurring on the left of ⇒, then Γ′ is A′_{1}, …, A′_{n}. ^{5}

These two translations are inverse:

Lemma 8 Let A be a formula of H. 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 H, 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.

The following lemma gives several variations of the deduction theorem for H.

Lemma 9 (Deduction theorem for H) (i) If H proves a from assumptions δ, b, then i(b, a) is a theorem proved in H from assumptions δ, provided the assumptions contain only constant proposition letters.

(ii) If a is provable from assumptions δ, b by condensed detachment from H1-H4, then i(b, a) is derivable by condensed detachment from δ., provided the assumptions contain only constant proposition letters.

(iii) If there is a proof of a by modus ponens from δ, b and substitution instances of H1-H4, then there is a proof of i(a, b) by modus ponens from δ and substitution instances of H1-H4.

(iv) In part (i), if the given proof of a has no double negations, then the proof of i(b, a) from δ has no double negations.

5We note that a similar translation has been given in [7] in connection with Lukasiewicz’s multi-valued logics (which include the infinite-valued logic discussed in another section of this paper). It is the obvious translation of Gentzen calculus into the implication-and-negation fragment of propositional calculus. We cannot appeal to any of the results of [7], since we are dealing with different logics, and besides we need to pay attention to double negations.

(v) In part (iii), if the given proof of a has no double negations, then the proof of i(b, a) from δ has no double negations.

Remarks: One interesting thing is that we do not prove a claim about double negations for condensed detachment proofs, only for modus ponens proofs. That is, there is no part (vi) analogous to parts (iv) and (v), but for condensed detachment proofs. The reason for the restriction to constant assumptions in (i) and (ii) is this: From the assumption i(n(n(x)), x), we can derive any theorem of classical logic, for instance i(n(n(a)), a), by substitution or condensed detachment. But we cannot derive the proposition that the first of these implies the second, i(i(n(n(x)), x), i(n(n(a)), a)). So the deduction theorem is false without the restriction. Proofs by modus ponens from substitution instances of axioms do not suffer from this difficulty, which is one reason they are so technically useful in this paper. Proof. We first show that (ii) follows from (iii). If we are given a condenseddetachment proof of a from assumptions δ, b using H1-H4, we can find, by Theorem 1, a modus-ponens proof of a from δ, b and substitution instances of H1-H4. Applying (iii) we have a modus ponens proof of i(b, a) from δ and substitution instances of H1-H4. By Theorem 7, this proof can be converted to a condenseddetachment proof of i(b, a) from δ, completing the derivation of (ii) from (iii).

Next we show that (i) follows from (iii). Suppose we are given a proof of a from δ, b in H. By Theorem 1, we can find a modus-ponens-only proof of a from assumptions δ, b and substitution instances of H1-H4. By (iii) we then can find a modus-ponens proof of i(b, a) from δ and substitution instances of H1-H4. Adding one substitution step above each such substitution instance, we have a proof in H of i(b, a) from δ. That completes the proof that (i) follows from (iii).

We now show that (v) implies (iv). This requires going over the previous paragraph with attention to double negations: Suppose we are given a doublenegation-free proof of a from δ, b in H. By Theorem 1, we can find a modusponens-only proof of a from assumptions δ, b and substitution instances of H1-H4, which is also double-negation-free. By the (v) we then can find a doublenegation-free modus-ponens proof of i(b, a) from δ and substitution instances of H1-H4. Adding one substitution step above each such substitution instance, we have a double-negation-free proof in H of i(b, a) from δ. That completes the proof that (iv) follows from (v).

Now we prove (iii) and (v) simultaneously by induction on the number of steps in a pure modus-ponens proof of a from δ and substitution instances of H1-H4.

Base case: a is b or of a member of δ, or a substitution instance of one of H1-H4.

If a is a substitution instance of an axiom of H1-H4, then by Lemma 3 there is a condensed-detachment proof of a from H1-H4 which contains only double negations already occurring in a.

If a is b, then we use the fact that i(b, b) is a theorem of H, provable without double negations (except those occurring in b) by Lemma 1. Hence by Theorem 1, it is provable by modus ponens from substitution instances of H1-H4.

If a is a member of δ, then consider the formula i(a, i(b, a)), which is a substitution instance of axiom H1. We can deduce i(b, a) by modus ponens from this formula and a; adjoining this step to a one-step proof of a from δ “by assumption”, we have a proof of i(b, a) from δ.

Turning to the induction step, suppose the last step in the given proof infers a from i(p, a) and p. By the induction hypothesis, we have proofs of i(b, p) and i(b, i(p, a)) from δ. By axiom H2 and modus ponens (which is a special case of condensed detachment) we have i(i(b, p), i(b, a)). Applying modus ponens once more, we have i(b, a) 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.

We shall refer to proofs by modus ponens from substitution instances of H1-H4 as M-proofs for short. Thus M-proofs use modus ponens only but can use substitution instances of axioms, as opposed to H-proofs which can use substitution anywhere as well as modus ponens. We have already shown how to convert condensed-detachment proofs to M-proofs (in Theorem 1), and viceversa (since every substitution instance of the axioms is derivable by condensed detachment).

Lemma 10 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 11 The translation from H to G is sound. That is, if H proves a from assumptions δ, then G proves the sequent Δ ⇒ A (where A is the translation a^{0}, and Δisδ^{0}).

Proof. By induction on the length of proofs. When the length is zero, we must exhibit a proof in G of each of the axioms H1-H4. This is a routine exercise in the Gentzen sequent calculus, which we omit. Now for the induction step: Suppose we have proofs in H from assumptions δ of a and i(a, b). Then by the induction hypothesis, we have proofs in G of Δ ⇒ A and Δ ⇒ A → B. It is another exercise in Gentzen rules to produce a proof of Δ ⇒ B. One solves this exercise by first proving

A → ((A → B) → B))

and then using the cut rule twice. This completes the proof of the lemma.

Lemma 12 (i) Suppose G proves the sequent Γ ⇒ A. Then there is an M-proof of a from assumptions γ. If G proves Γ ⇒ [], where [] is the empty list, then there is an M-proof of p from assumptions γ, where p is any formula of H.

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

(iii) If in part (i) the H-translation of the given sequent Γ ⇒ Δ does not contain any double negations, then the M-proof 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 H 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, Γ ⇒ Θ \atop A → B, Δ, Γ ⇒ Θ}

By the induction hypothesis, we have an M-proof of a from δ, and an Mproof of θ from b and γ. We must give an M-proof of θ from i(a, b), δ, and γ.

Applying modus ponens 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. No double negations are introduced by this step.

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

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

By the induction hypothesis, we have an M-proof from H1-H4 of b from γ and a. Applying the deduction theorem for H1-H4 with M-proofs, we have an M-proof in H 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, by part (v) of the deduction theorem. (This is why we must use M-proofs instead of condensed detachment.)

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

{A, Γ ⇒ [] \atop Γ ⇒ ¬A}

By the induction hypothesis, there is an M-proof of n(a) from a and γ. By the deduction theorem for H1-H4 with M-proofs, there is a proof of i(a, n(a)) from γ. So it suffices to show that n(a) is derivable from i(a, n(a)). This follows from a substitution instance of H3, which is i(i(x, n(x)), n(x)), substituting a for x.

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

{Γ ⇒ A \atop ¬A, Γ ⇒ []}

By the induction hypothesis, we have an M-proof of a from γ. We must show that from n(a) and γ, we can deduce b in L, where b is any formula of H. We have i(a, i(n(a), b) as a substitution instance of axiom H4. Applying modus ponens twice, we have the desired M-proof of b from γ, completing case 4.

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

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

By the induction hypothesis we have an M-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 thinning in the antecedent:

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

By the induction hypothesis, we have an M-proof from H1-H4 of θ from assumptions Γ′. That counts as an M-proof from assumptions C, γ as well. That completes case 6.

Case 7, 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 H, and all the theorems of H that we used have been given double-negation-free condensed-detachment proofs from H1-H4. By Theorem 1, they have double-negation-free M-proofs too. Although we may not have pointed it out in each case, the argument given produces an M-proof in which any double negations arise from the translations into H of doubly-negated subformulas of the final sequent. In particular, if the final sequent contains no double negations, then the M-proof produced also contains no double negations.

Theorem 8 Suppose H proves b from assumptions δ and neither δ nor b contains double negation. Then there is a condensed-detachment proof of b from H1-H4 and assumptions δ that does not contain double negation.

More generally, if δ and b are allowed to contain double negation, then there is a condensed detachment proof of b from H1-H4 and assumptions δ that contains no new double negations. That is, all doubly-negated formulas occurring in the proof are subformulas of δ or of b.

Proof. Let b^{0} = B be the translation of b into G defined earlier. Double negations in B arise only from double negations in b. Suppose b is provable in H from assumptions δ. By Theorem 1, there is an M-proof of b from δ. By Lemma 11, the sequent Δ ⇒ B is provable in G. Hence, by Gentzen’s cut-elimination theorem, there is a proof in G of Δ ⇒ b. By the previous lemma, there is an M-proof of B′ from assumptions Δ^{0}′ that contains no new double negations. But by Lemma 8, B′ = b and Δ′ = δ. Thus we have an M-proof of b from δ. By the D-completeness of H, Theorem 7, there is also a condensed-detachment proof of b from δ. The second part of Theorem 7 says that we can find a doublenegation-free condensed detachment proof of b from δ. It is important that we are working with M-proofs here, since the second part of the D-completeness theorem, about double negations, only applies to M-proofs.

This completes the proof.

Theorem 9 Suppose A is provable from H1-H4 using condensed detachment as the only rule of inference. Then A has a proof from H1-H4 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 H1-H4 using condensed detachment. Each condensed detachment step can be converted to three steps using substitution and modus ponens, so A is provable in H. By the preceding theorem, A has a condensed detachment proof from H1-H4 in which no doubly negated formulas occur except those that already occur in A. This completes the proof. Remark. Note that since the translation back from Gentzen calculus produces M-proofs, we do not need to appeal to d-completeness for arbitrary H-proofs. This is good, since we do not know a proof of d-completeness that avoids the possible introduction of double negations, except when restricted to M-proofs.

Corollary 2 Let T be any set of axioms for intuitionistic propositional logic. Suppose that there exist condensed-detachment proofs of H1-H4 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 H1-H4.

Proof . Let b be provable from T. Then b is provable from H1-H4, since T is a set of axioms for intuitionistic logic. By the theorem, there is a proof of b from H1-H4 that contains no double negations (except those occurring in b, if any). Supplying the given proofs of H1-H4 from T, we construct a proof of b from T which contains no double negations except those occurring in T or in b (if any). That completes the proof.

References

[1] Chang, C.C., Algebraic analysis of many valued logics, Trans. Amer. Math. Soc. 88, 467-490 (1958).

[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] McCune, W. W.,Otter 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois (1994).

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

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

[8] Rose, Alan, and Rosser, J. Barkley, Fragments of many-valued statement calculi, Trans. Amer. Math. Soc. 87 (1958) 1–53.

[9] Ulrich, D., A Legacy Recalled and a Tradition Continued, Journal of Automated Reasoning, 27(2), 2001, 97–122.

[10] Veroff, R., Using hints to increase the effectiveness of an automated reasoning program: Case studies”, J. Automated Reasoning 16(3), pp. 223-239.

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

[12] Wos, L., The resonance strategy, in Wos, L., The Collected Works of Larry Wos, Volume II, pp. 1317-1377, World Scientific, Singapore (2000).

[13] Wos, L., Conquering the Meredith Single Axiom, J. Automated Reasoning 27 (2001), pp. 175-199.