PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 63 (77), 1998, 9–20

BETWEEN TW_{→} AND RW_{→}

Aleksandar Kron

To the memory of V. A. Smirnov (1931–1996)

Communicated by Žarko Mijajlović

Abstract. We investigate some pure implicational systems placed between the implicational fragments TW_{→} and RW_{→} of the well-known relevance systems TW and RW For one them, TRW_{→}+RP, we prove (1) and (2):

(1) if both ⊢ A → B and ⊢ B → A in TRW_{→}+RP, then B can be obtained from A by substitution of occurrences of formulas of the form D → .C → E for some occurrences of subformulas of A of the form C → .D → E (CONGR);

(2) CONGR is equivalent to NOASS: for any A and B,

⊬ A → .A → B → B

in TRW_{→}+RP.

CONGR is a generalization of the solution to the P–W problem, solved for TW_{→} in [6] (cf. also [1]–[4] for other solutions).

The equivalence of CONGR and NOASS is a generalization of the Dwyer-Powers theorem for TW_{→} to the effect that the P–W problem is equivalent to NOID: there is no theorem of TW_{→}-ID of the form AA.

The proof of the equivalence of CONGR and NOASS is obtained by double induction applied jointly with a normal form theorem.

1. Introduction

The only connective in the propositional language investigated here is →. We write (AB) for (A → B); furthermore, ABC and A.BC stand for (AB)C and A(BC), respectively.

For any A the set c(A) is the smallest set satisfying (1) and (2): (1) A ∈ c(A);

(2) let B ∈ c(A) be such that C.DE is a subformula of B, for some C, D and E,

AMS Subject Classification (1991): Primary 03B46 Supported by the Science Fund of Serbia, grant number 04M01A through the Mathematical

Institute in Belgrade.

and let B^{∗} be obtained by substitution of D.CE for C.DE, at a single occurrence of C.DE in B; then B^{∗} ∈ c(A).

A and B are congruent (in symbols A ∼ B) iff B ∈ c(A). A ≁ B means B ∉ c(A).

For any A by A^{∗} we denote any formula B such that A ∼ B.

In the sequel several sub-systems of RW_{→} are investigated. If S and T are any two of them, we write (S ⊂ T), S ⊆ T, and S = T if the set of theorems of S is a (proper) subset of or equal to the set of theorems of T, respectively.

Let U be either an axiom-scheme or a rule; if U is adjoined (deleted) to (from) a system S, the result is denoted by S+U (S–U).

RW_{→} can be defined by modus ponens (MP) and the following axiomschemata:

ID  AA
ASU  AB.BC.AC
APR  BC.AB.AC
AP  A(BC).B.AC.

An equivalent formulation of RW_{→} is obtained by substitution of the axiomscheme A.ABB (axiom-scheme of assertion, ASS) for AP (axiom-scheme of permutation). Sometimes it is important to distinguish between these two formulations; on such occasions the first will be called RW_{→AP} and the second RW_{→ASS}.

RW_{→} is closed under substitution of equivalents and, hence, under the rule of permutation:

P  If ⊢ A, then ⊢ A^{∗}

Also, RW_{→} is closed under the rules

ASS1 If ⊢ A, then ⊢ ABB
ASS2 If ⊢ A and ⊢ B_{1}. . . . .B_{k}. . . . .B_{n}C, then ⊢ B_{1}. . . . .AB_{k}. . . . .B_{n}C.

The closure under ASS1 follows by ASS and MP, and the closure under ASS2 by P, ASS1 and TR. On the other hand, when we have ID, ASS1 is obtained by ASS2.

TW_{→} is defined by MP and the axiom-schemata ID, ASU and APR. It has the Anderson-Belnap property (A-B): if both ⊢ AB and ⊢ BA in TW_{→}, then A and B denote the same formula.

A-B is equivalent to the Dwyer-Powers property (D-P): for any A, ⊬ AA in TW_{→}–ID.

TW_{→} and TW_{→}–ID have alternative formulations TRW_{→} and TRW_{→}– ID, respectively, obtained by deleting MP and by adjoining the following rules instead:

SU  If ⊢ AB, then ⊢ BC.AC
PR  If ⊢ BC, then ⊢ AB.AC
TR  If ⊢ AB and ⊢ BC, then ⊢ AC

TW_{→}+P is an equivalent formulation of RW_{→}. On the other hand, adding P to TRW_{→} does not suffice to produce RW_{→} – we must add ASS1 as well.

Theorem 1.1. TW_{→}+P = TRW_{→}+P+ASS1.

Proof. It was proved in [5, Theorem 5] that TW_{→}+P–ID = TRW_{→}+P+ ASS1–ID. The inductive proof given there was to the effect that TRW_{→}+P+ASS1– ID is closed under the following Ackermann’s rule δ (and hence under MP): if

(a) ⊢ A_{i}  and  (b) ⊢ A_{1}. . . . .A_{i−1}.A_{i}.A_{i+1}. . . . .A_{n}p,

then

(c) ⊢ A_{1}. . . . .A_{i−1}.A_{i+1}. . . . .A_{n}p.

The induction is on the weight of (b) and has to be extended here by considering ID. This is easy.

Can we substitute the rules SU, PR and TR for MP in RW_{→AP} and RW_{→ASS} such that the resulting systems are equivalent to the old ones and to each other?

The negative answer is a surprise. We shall show that these new systems are not closed under MP. Moreover, they are not equivalent to each other. This shows that between TW_{→} and RW_{→} there is more room for some interesting intermediate systems than we believed to be. One of them is TRW_{→}+RP; we shall show that it enjoys CONGR – a property analogous to A-B: if both ⊢ AB and ⊢ BA in TRW_{→}+RP, then A ∼ B. This property is not shared by all systems between TW_{→} and RW_{→}; for example, ⊢ AA.AAAA and ⊢ AAAA.AA in TRW_{→}+P; obviously, AA ≁ AAAA.

2. The intermediate systems

Let us define the rule of restricted permutation:

RP  If ⊢ AB, then ⊢ A^{∗}B^{∗}

Since TRW_{→}+AP is closed under substitution of equivalents, it is easy to prove

Theorem 2.1. TRW_{→}+RP = TRW_{→}+AP.

Theorem 2.2. TW_{→}+RP = RW_{→}.

Proof. It is clear that TW_{→}+RP ⊆ RW_{→}.

In TW_{→}+RP ID and RP yield AP. Also, TW_{→}+RP is closed under MP. Hence, RW_{→} = RW_{→AP} ⊆ TW_{→}+RP.

The main property of TRW_{→}+RP is given in the next theorem.

Theorem 2.3. If A ≁ B, then

⊢ AB in TRW_{→}+RP iff ⊢ AB in TRW_{→}+RP–ID.

Proof. Suppose that A ≁ B and proceed by induction on theorems of TRW_{→}+RP.

If AB is an axiom of TRW_{→}+RP, then AB is an axiom of TRW_{→}+RP–ID. Let AB = CD.ED, ⊢ CD.ED by ⊢ EC and SU; since CD ≁ ED, it follows

that E ≁ C; by induction hypothesis, ⊢ EC in TRW_{→}+RP–ID, . Hence, by SU ⊢ CD.ED in TRW_{→}+RP–ID.

In the case of PR we proceed in a similar way. If ⊢ AB by ⊢ AC, ⊢ CB and TR, then either A ≁ C or C ≁ B. If

both A ≁ C and C ≁ B, then by induction hypothesis, ⊢ AC and ⊢ CB in TRW_{→}+RP–ID; hence, ⊢ AB in TRW_{→}+RP–ID by TR.

If A ∼ C, by induction hypothesis ⊢ CB in TRW_{→}+RP–ID; we obtain ⊢ AB by ⊢ CB and RP. If C ∼ B, by induction hypothesis ⊢ AC in TRW_{→}+RP– ID; we obtain ⊢ AB by ⊢ AC and RP.

Let AB = C^{∗}D^{∗} and ⊢ C^{∗}D^{∗} by ⊢ CD and RP; since C^{∗} ≁ D^{∗}, we have C ≁ D; by induction hypothesis, ⊢ CD in TRW_{→}+RP–ID, and ⊢ C^{∗}D^{∗} by RP.

Since TRW_{→}+RP–ID ⊂ TRW_{→}+RP, the theorem is proved.

It was shown in [4] that TRW_{→}+P+ASS1–ID (called there K) has an equivalent Genzten-style formulation J that contains no theorem of any of the forms AA, A.ABB, ABBA or AABB. We shall state this fact in the form of a theorem, for further reference.

Theorem 2.4. In TRW_{→}+P+ASS1–ID:

(a) (No identity, NOID) There is no theorem of the form AA.

(b) (No assertion, NOASS_{1}) There is no theorem of the form A.ABB.

(c) (NOASS_{2}) There is no theorem of the form ABBA.

(d) (NOE_{1}) ⊢ (A_{1}.A_{2}. . . . .A_{n}B)B iff ⊢ A_{1}, …, ⊢ A_{n}.

(e) (NOE_{2}) There is no theorem of the form AABB.

NOASS_{1} and NOASS_{2} are equivalent whenever we have SU. In the sequel we write NOASS both for NOASS_{1} and NOASS_{2}.

Since TRW_{→}+RP–ID ⊆ TRW_{→}+P–ID ⊆ TRW_{→}+P+ASS1–ID, NOID, NOASS and NOE_{2} hold for TRW_{→}+RP–ID as well.

Now we can prove CONGR.

Theorem 2.5. (CONGR) If both ⊢ AB and ⊢ BA in TRW_{→}+RP, then A ∼ B.

Proof. Suppose that both ⊢ AB and ⊢ BA in TRW_{→}+RP, and that A ≁ B. By Theorem 2.3, ⊢ AB and ⊢ BA in TRW_{→}+RP–ID. Hence, ⊢ AA in TRW_{→}+RP–ID by TR, contrary to NOID.

The Anderson–Belnap property A-B is a special case of CONGR. Another surprise is that NOASS holds for some systems having the axiom-

scheme ID.

Theorem 2.6. For any A and any B, ⊬ A.ABB in TRW_{→}+RP.

Proof. Suppose that there are A and B such that ⊢ A.ABB in TRW_{→}+RP; by A ≁ ABB and Theorem 2.3, ⊢ A.ABB in TRW_{→}+RP –ID, contrary to NOASS.

Theorem 2.6 shows that TRW_{→}+RP is closed neither under MP nor under P; otherwise, from the axiom pp.pq.pq we would obtain pp.p.pqq by RP and then p.pqq by pp and MP.

Theorem 2.7. In TRW_{→}+RP CONGR implies NOASS.

Proof. Suppose that ⊢ A.ABB in TRW_{→}+RP, for some A and B. By SU we obtain (a) ⊢ ABB(CB).A.CB for any C. Also, (b) ⊢ C(AB).ABB.CB by ASU. Hence, (c) ⊢ A(CB).ABB.CB by RP. Now by (a), (c) and CONGR we have A(CB) ∼ ABB.CB, which is impossible. Hence, in TRW_{→}+RP CONGR implies NOASS.

Let us compare TRW_{→}+AP and TRW_{→}+ASS.

Theorem 2.8. TRW_{→}+AP ⊂ TRW_{→}+ASS.

Proof. As in the proof of Theorem 2.7, we have (a) and (b). Hence, we have ⊢ B(AC).A.BC in TRW_{→}+ASS, by TR; thus TRW_{→}+AP ⊆ TRW_{→}+ASS. By NOASS, TRW_{→}+AP ≠ TRW_{→}+ASS.

Since TRW_{→}+ASS is closed under substitution of equivalents, it is closed under RP. Moreover, we have

Theorem 2.9. TRW_{→}+ASS is closed under P.

Proof. By induction on theorems of TRW_{→}+ASS. Suppose that ⊢ D.EF in TRW_{→}+ASS. If it is an instance of ID, then

⊢ E.DF by ASS, and conversely, if ⊢ D.EF by ASS, then ⊢ E.DF by ID. If ⊢ D.EF by ASU (APR), then ⊢ E.DF by APR (ASU). Suppose that ⊢ D.EF by (a) ⊢ ED_{1} and SU, where D = D_{1}F. Now (b)

⊢ D_{1}.D_{1}F F is an axiom; hence, ⊢ E.DF by (a), (b) and TR.

Suppose that ⊢ D.EF by (a) ⊢ D_{1}F and PR, where D = ED_{1}. By (a) and PR we have (b) ⊢ ED_{1}D_{1}.ED_{1}F. On the other hand, (c) ⊢ E.ED_{1}D_{1} by ASS. Therefore, ⊢ E.DF by (c), (b) and TR.

Suppose that ⊢ D.EF by (a) ⊢ DG, (b) ⊢ G.EF and TR. By induction hypothesis, (c) ⊢ E.GF. On the other hand, (d) ⊢ GF.DF by (a) and SU; hence, ⊢ E.DF by (c), (d) and TR.

Therefore, if ⊢ D.EF in TRW_{→}+ASS, then ⊢ E.DF in TRW_{→}+ASS. This, together with the closure under RP gives us the closure under P.

Corollary. TRW_{→}+ASS = TRW_{→}+P.

Proof. Obviously, TRW_{→}+ASS ⊆ TRW_{→}+P, by ID and P. TRW_{→}+ASS is closed under P, by Theorem 2.9; hence, TRW_{→}+P ⊆ TRW_{→}+ASS.

It is interesting to notice that TRW_{→}+ASS–ID ≠ TRW_{→}+P–ID. For, NOASS holds in TRW_{→}+P–ID, but in TRW_{→}+ASS–ID we have the axiomscheme ASS. Hence, it is easy to prove AP in TRW_{→}+ASS–ID (look at (a), (b) and TR in the proof of Theorem 2.7). Thus, some instances of ID are theorems of TRW_{→}+ASS–ID. However, we can prove neither pp nor pq.pq nor pqr.pqr nor etc.

By induction on theorems one can prove that TRW_{→}+ASS contains no theorem of the form ABp; hence, it contains no theorem of the form App. This shows that TRW_{→}+ASS is not closed under ASS1. It follows that TRW_{→}+ASS is not closed under MP (otherwise, by MP and ASS, it is closed under ASS1).

It was shown in [3] that TRW_{→}+P–ID has an equivalent Genzten-style formulation L that enjoys the properties NOID and NOASS and contains no theorem of the form ABB. But we have more than that.

Theorem 2.10. (NOABB). For any A and any B, ⊬ ABB in TRW_{→}+RP.

Proof. Suppose that ⊢ ABB in TRW_{→}+RP, for some A and B. Since B ≁ AB, by Theorem 2.3, ⊢ ABB in TRW_{→}+RP–ID ⊂ TRW_{→}+P–ID, which is impossible.

What happens when either ASS1 or MP is added to any of these systems? TRW_{→}+ASS1 and TRW_{→}+ASS1–ID are closed under MP. This is proved

by induction on the weight of the major premiss of MP. In the first of these systems we have the axiom-scheme AABB – the characteristic axiom-scheme of EW_{→}; in the latter we have NOE_{2}.

It is easy to show that TRW_{→}+ASS+ASS1 and TRW_{→}+ASS+ASS1–ID are closed under MP. Since AP is a theorem of TRW_{→}+ASS+ASS1–ID, the systems TRW_{→}+ASS+ASS1 and TRW_{→}+ASS+ASS1–ID are closed under P. Therefore, TRW_{→}+ASS+ASS1 = TRW_{→}+P+ASS1 = RW_{→}.

However, in TRW_{→}+P+ASS1–ID we have both NOID and NOASS, but none of them in TRW_{→}+ASS+ASS1–ID. Therefore, TRW_{→}+P+ASS1–ID ⊂ TRW_{→}+ASS+ASS1–ID.

Adding ASS1 to TRW_{→}+RP destroys CONGR. Since (a) ⊢ AA(AA).AA and (b) ⊢ AA.AA.AA in TRW_{→}+RP+ASS1, we see that CONGR does not hold here. By (a) and SU we have (c) ⊢ AA(AA).(AA.AA).AA; by (b), (c) and TR we obtain ⊢ AA.(AA.AA).AA – an instance of ASS. Therefore, NOASS does not hold in TRW_{→}+RP+ASS1. Since NOASS holds for TRW_{→}+RP+ASS1–ID, there are A and B such that ⊢ AB in TRW_{→}+RP+ASS1, A ≁ B and ⊬ AB in TRW_{→}+RP+ASS1–ID.

Adding MP to TRW_{→}+RP would collapse it to RW_{→}. Adding MP to TRW_{→}+RP+ASS1–ID destroys NOABB. For example, let A = pp.pp.pp and B = (pp.pp)p.ppp; then A and AB are instances of ASU. By RP and AB.BC.AC we get (a) ⊢ AB.A.BCC; hence, by (a) and MP, ⊢ BCC.

Let us summarize the comparison of the systems investigated here. TW_{→} = TRW_{→} ⊂ TRW_{→}+RP = TRW_{→}+AP ⊂ TRW_{→}+P = TRW_{→}+ASS ⊂ TRW_{→}+P+ASS1 = TRW_{→}+ASS+ASS1 = TW_{→}+RP = TW_{→}+P = RW_{→} = RW_{→AP} = RW_{→ASS}.

Also, TW_{→}–ID = TRW_{→}–ID ⊂ TRW_{→}+RP –ID ⊂ TRW_{→}+P–ID ⊂ TRW_{→}+P+ASS1–ID.

Only TRW_{→}+RP has the property stated in CONGR; it is not shared by stronger systems between TRW_{→} and RW_{→} investigated here.

The congruence relation ∼ defined for formulas is determined here by logical means only - by provability in TRW_{→}+RP.

3. The equivalence of congr and noass

The final surprise is the fact that in TRW_{→}+RP CONGR and NOASS are equivalent. To prove it we need some other facts.

In the sequel ⊢ A means ⊢ A in TRW_{→}+AP.

Theorem 3.1. If either ⊢ Ap or ⊢ pA, then A = p; if ⊢ B.pp, then B = pp.

Proof. By induction on theorems.

Proofs in TRW_{→}+AP can be written in a normal form.

Theorem 3.2. For any proof of a theorem containing n applications of TR there is a proof of the same theorem containing n applications of TR such that no application of TR precedes an application of another rule.

Proof. If ⊢ AC by (a) ⊢ AB, (b) ⊢ BC and TR, and then ⊢ CD.AD by SU, then (c) ⊢ BD.AD by (a) and SU, as well as (d) ⊢ CD.BD by (b) and SU; hence, ⊢ CD.AD by (c), (d) and TR.

In a similar way we take care of PR.

If the old proof contains n applications of TR, so does the new one.

In the sequel we assume that in proofs of theorems no application of TR precedes an application of another rule.

The sequence of theorems

⊢ AB.C_{1}D_{1}, ⊢ C_{1}D_{1}.C_{2}D_{2}, …, ⊢ C_{n−1}D_{n−1}.C_{n}D_{n}, ⊢ C_{n}D_{n}.EF

is called a transitive chain (TR-chain) from AB to EF iff TR is not applied in the proof of any member of the chain.

Theorem 3.3. If (a) ⊢ AB and (b) ⊢ BC such that (a) is obtained by an application of SU (PR) in the last step and (b) is obtained by an application of PR (of SU) in the last step, then there is a proof of ⊢ AC by TR such that the left premiss (a’) in this application of TR is obtained by PR (SU) in the last step and the right premiss (b’) is obtained by SU (PR) in the last step.

Proof. Suppose that (a) ⊢ DE.F E by (a’) ⊢ F D and SU, and that (b) ⊢ F E.F G by (b’) ⊢ EG and PR. We have (b’) ⊢ DE.DG by (b’) and PR, and ⊢ DG.F G by (a’) and SU.

Suppose that (a) ⊢ ED.EF by (a’) ⊢ DF and PR, and (b) ⊢ EF.GF by (b’) ⊢ GE and SU. We have ⊢ ED.GD by (b’) and SU, and ⊢ GD.GF by (a’) and PR.

Theorem 3.4. If (a) ⊢ AB and (b) ⊢ BC such that (a) is obtained by an application of SU in the last step and (b) is an instance of AP, then there is a proof of ⊢ AC by TR such that the left premiss (a’) is an instance of AP and the right premiss (b’) is obtained by PR in the last step.

Proof. Suppose that (a) ⊢ D(EG).F.EG by (a”) ⊢ F D and SU, and that (b) ⊢ F (EG).E.F G by AP. We have (a’) ⊢ D(EG).E.DG by AP and (b”) ⊢ DG.F G by (a”) and SU, and then (b’) ⊢ E(DG).E.F G by (b”) and PR.

Theorem 3.5. If (a) ⊢ AB and (b) ⊢ BC such that (a) is obtained by (a’) and PR in the last step, (b) is an instance of AP, and (a’) is obtained from (a”) either by SU or by PR, then there is a proof of ⊢ AC by TR such that the left premiss (c) is an instance of AP and the right premiss (b’) is obtained either by SU or by PR in the last step, respectively.

Proof. Suppose that (a”) ⊢ ED, (a’) ⊢ DF.EF, (a) ⊢ C(DF).C.EF and (b) ⊢ C(EF).E.CF. We have (c) ⊢ C(DF).D.CF by AP, and ⊢ D(CF).E.CF by (a”) and SU.

Suppose that (a”) ⊢ ED, (a’) ⊢ F E.F D, (a) ⊢ C(F E).C.F D and (b) ⊢ C(F D).F.CD. We have (c) ⊢ C(F E).F.CE by AP, and ⊢ F (CE).F.CD by (a”) and PR applied twice.

Theorem 3.6. Let

⊢ AB.D_{1}E_{1}, ⊢ D_{1}E_{1}.D_{2}E_{2}, …, ⊢ D_{n−1}E_{n−1}.D_{n}E_{n}, ⊢ D_{n}E_{n}.CD

be a TR-chain from AB to CD; if no member of the chain is an axiom, then either

(a)  ⊢ CA and B = D,

if all members of the chain are obtained by SU in the last step, or

(b)  ⊢ BD and A = C,

if all members of the chain are obtained by PR in the last step, or

(c)  ⊢ CA and ⊢ BD.

otherwise.

Proof. If all members of the TR-chain from AB to CD are obtained by SU (PR), then ⊢ CA and B = D (A = C and ⊢ BD); the proof is by induction on the number of members of the chain.

Apply Theorem 3.3. Let every member in

⊢ AB.D_{1}E_{1}, ⊢ D_{1}E_{1}.D_{2}E_{2}, …, ⊢ D_{k−1}E_{k−1}.D_{k}E_{k},

be obtained by SU, and let every member in

⊢ D_{k}E_{k}.D_{k+1}E_{k+1}, …, ⊢ D_{n−1}E_{n−1}.D_{n}E_{n}, ⊢ D_{n}E_{n}.CD

be obtained by PR; then ⊢ D_{k}A, B = E_{k}, C = D_{k}, and ⊢ E_{k}D.

Corollary. Let

⊢ AB.D_{1}E_{1}, ⊢ D_{1}E_{1}.D_{2}E_{2}, …, ⊢ D_{n−1}E_{n−1}.D_{n}E_{n}, ⊢ D_{n}E_{n}.CD

be a TR-chain from AB to CD; if no member of the chain is an instance of either ASU or APR, then either ⊢ CA and B ∼ D (in case every member of the chain is either an instance of AP or obtained by SU in the last step) or else ⊢ BD and A ∼ C (in case every member of the chain is either an instance of AP or obtained by PR in the last step) or ⊢ CA and ⊢ BD otherwise.

Proof. By Theorems 3.4 and 3.5, we may assume that all instances of AP in the TR-chain from AB to CD precede the members obtained by either SU or PR. Hence, apply Theorem 3.6.

Now we can prove that NOASS implies CONGR.

Theorem 3.7. If ⊢ AB, ⊢ BA, then A ∼ B.

Proof. Assume NOASS in TRW_{→}+AP (forgetting that it is already proved) and ⊢ AB and ⊢ BA. If either A = p or B = p or A = pp or B = pp, then A = B, by Theorem 3.1.

By Theorem 3.2, we have the TR-chain (∗)

⊢ AB_{1}, ⊢ B_{1}B_{2}, …, ⊢ B_{k−1}B_{k}, ⊢ B_{k}B_{k+1}, ⊢ B_{k+1}B_{k+2}, … ⊢ B_{m−1}B_{m}, ⊢ B_{m}A

Lemma 3.8 No member of (∗) is an instance of either ASU or APR.

Proof of the lemma. Suppose that ⊢ DE.EF.DF is a member of (∗); then we have (a) ⊢ (EF.DF).DE as well. But ⊢ EF.DE.DF and (b) ⊢ (DE.DF)(DF).EF.DF by APR and SU; hence, ⊢ (DE.DF)(DF).DE by (a),

(b) and TR, contrary to NOASS.

Let ⊢ EF.DE.DF be a member of (∗); then (a) ⊢ (DE.DF).EF as well. Now ⊢ DE.EF.DF and (b) ⊢ (EF.DF)(DF).DE.DF by ASU and SU; hence, ⊢ (EF.DF)(DF).EF by (a), (b) and TR, contrary to NOASS.

Lemma 3.9 No member of the chain (∗) is obtained by PR in the last step from either ASU or APR.

Proof of the lemma. Let (a’) ⊢ DE.EF.DF, (a) ⊢ G(DE).G.EF.DF by (a’) and PR, and let (a) be a member of (∗); then (b) ⊢ G(EF.DF).G.DE, for there is a member ⊢ HI of (∗) such that H^{∗}I^{∗} ∼ G(EF.DF).G.DE. Now (c) ⊢ EF.G(DE).G.DF by ⊢ EF.DE.DF, ⊢ DE(DF).G(DE).G.DF and TR. Hence,

(d) ⊢ (G(DE).G.DF)(DF).EF.DF by (c) and SU, (e)

⊢ G((G(DE).G.DF)(DF)).G.EF.DF

by (d) and PR, (f) ⊢ ((G(DE).G.DF).G.DF).G.EF.DF by (e) and RP, and, eventually, ⊢ ((G(DE).G.DF).G.DF).G.DE by (f), (b) and TR, contrary to NOASS.

Suppose that (a’) ⊢ EF.DE.DF, (a) ⊢ G(EF).G.DE.DF by (a’) and PR, and that (a) is a member of (∗); then (b) ⊢ G(DE.DF).G.EF, for there is a member ⊢ HI of (∗) such that H^{∗}I^{∗} ∼ G(DE.DF).G.EF. Now (c) ⊢ DE.G(EF).G.DF by ⊢ DE.EF.DF, ⊢ EF (DF).G(EF).G.DF and TR, (d) ⊢ G(EF)(G.DF)(DF).DE.DF by (c) and SU, (e)

⊢ G((G(EF).G.DF)(DF)).G.DE.DF

by (d) and PR, (f) ⊢ ((G(EF).G.DF).G.DF).G.DE.DF by (e) and RP, and, eventually, ⊢ ((G(EF).G.DF).G.DF).G.EF by (f), (b) and TR, contrary to NOASS.

Returning to the proof of the theorem, proceed by double induction: on the degree of A and on the length l of the TR-chain (∗). Suppose that the theorem is true for any formula of degree smaller than the degree of A and any TR-chain (Hyp 1), and for A and any TR-chain of length smaller than l (Hyp 2).

Let us analyze the TR-chain (∗); by theorems 3.2-6 and lemmas 3.8-9, there is a TR-chain (∗) from A to A such that no member of (∗) is an instance of either ASU or APR. Moreover, we may assume that all instances of AP precede all instances obtained by either SU or PR in the last step.

If the member ⊢ B_{m}A of (∗) is an instance of AP, so are all members of (∗) and the theorem is proved.

Suppose that

⊢ AB_{1}, ⊢ B_{1}B_{2}, …, ⊢ B_{k−1}B_{k},

are instances of AP, and that

⊢ B_{k}B_{k+1}, ⊢ B_{k+1}B_{k+2}, …, ⊢ B_{m−1}B_{m}, ⊢ B_{m}A

are obtained either by SU or by PR in the last step. By Theorem 3.3 all applications of SU in the last steps precede all applications of PR in the last step.

Let A = A_{1}.A_{2}A_{3} and let B_{k} = B_{k}^{1}.B_{k}^{2}B_{k}^{3}, …, B_{m} = B_{m}^{1}.B_{m}^{2}B_{m}^{3}.

Case I A = B_{k}.

I.1 B_{m}A is obtained by SU; hence, ⊢ A_{1}B_{m}^{1} and A_{2}A_{3} = B_{m}^{2}B_{m}^{3}. Also, all members of ⊢ B_{k+1}B_{k+2}, …, ⊢ B_{m−1}B_{m} are obtained by SU in the last step. Hence, ⊢ B_{k+1}^{1}A_{1} and A_{2}A_{3} = B_{k+1}^{2}B_{k+1}^{3}. By Theorem 3.6 ⊢ B_{m}^{1}B_{k+1}^{1}. We have ⊢ A_{1}B_{m}^{1} and ⊢ B_{m}^{1}A_{1}; by Hyp 1 A_{1} ∼ B_{m}^{1}, A ∼ B_{m} and there is a TR-chain from A to A of length l − 1. By Hyp 2, A ∼ B_{1} ∼ … ∼ B_{m} ∼ A.

I.2 B_{m}A is obtained by PR; hence A_{1} = B_{m}^{1} and ⊢ B_{m}^{2}B_{m}^{3}.A_{2}A_{3}.

I.2.1 ⊢ AB_{k+1} by PR; hence, A_{1} = B_{k+1}^{1}, ⊢ A_{2}A_{3}.B_{k+1}^{2}B_{k+1}^{3} and all members of ⊢ B_{k+1}B_{k+2}, …, ⊢ B_{m−1}B_{m} are obtained by PR in the last step. Hence, ⊢ A_{2}A_{3}.B_{k+1}^{2}B_{k+1}^{3}, … ⊢ B_{m}^{2}B_{m}^{3}.A_{2}A_{3}. By Hyp 1, A_{2}A_{3} ∼ B_{k+1}^{2}B_{k+1}^{3} ∼ ⋯ ∼ B_{m}^{2}B_{m}^{3} and A ∼ B_{1} ∼ … ∼ B_{m} ∼ A.

I.2.2 ⊢ AB_{k+1} by SU; hence, ⊢ B_{k+1}^{1}A_{1} and A_{2}A_{3} = B_{k+1}^{2}B_{k+1}^{3}. By Theorem 3.6, ⊢ B_{m}^{1}B_{k+1}^{1} and ⊢ B_{k+1}^{2}B_{k+1}^{3}.B_{m}^{2}B_{m}^{3}. We have ⊢ A_{1}B_{k+1}^{1} and ⊢ B_{k+1}^{1}A_{1}. By Hyp 1, A_{1} ∼ B_{k+1}^{1}, A ∼ B_{k+1} and there is a TR-chain from A to A of length l − 1. By Hyp 2, A ∼ B_{1} ∼ … ∼ B_{m} ∼ A.

Case II A_{2}.A_{1}A_{3} = B_{k}^{1}.B_{k}^{2}B_{k}^{3}.

II.1 B_{m}A is obtained by SU and so are all members of ⊢ B_{k+1}B_{k+2}, …, ⊢ B_{m−1}B_{m}; hence, A_{1}A_{3} = B_{k+1}^{2}B_{k+1}^{3} = … = B_{m}^{2}B_{m}^{3} = A_{2}A_{3}. Therefore, A_{1} = A_{2} and we may proceed as in Case I.

II.2 B_{m}A is obtained by PR; hence A_{1} = B_{m}^{1} and ⊢ B_{m}^{2}B_{m}^{3}.A_{2}A_{3}.

II.2.1 ⊢ B_{k}B_{k+1} by PR; hence, A_{2} = B_{k+1}^{1}, ⊢ A_{1}A_{3}.B_{k+1}^{2}B_{k+1}^{3} and all members of ⊢ B_{k+1}B_{k+2}, …, ⊢ B_{m−1}B_{m} are obtained by PR in the last step. Hence, ⊢ A_{1}A_{3}.B_{k+1}^{2}B_{k+1}^{3}, …, ⊢ B_{m}^{2}B_{m}^{3}.A_{2}A_{3}. By Theorem 3.6, A_{1} = A_{2} and we may proceed as in Case I.

II.2.2 ⊢ B_{k}B_{k+1} by SU; hence, ⊢ B_{k+1}^{1}A_{2} and A_{1}A_{3} = B_{k+1}^{2}B_{k+1}^{3}. By Theorem 3.6, ⊢ B_{m}^{1}B_{k+1}^{1} and ⊢ B_{k+1}^{2}B_{k+1}^{3}.B_{m}^{2}B_{m}^{3}. Hence, ⊢ A_{1}B_{k+1}^{1} and ⊢ B_{k+1}^{1}A_{2}. We get ⊢ A_{1}A_{2} and hence ⊢ A_{2}A_{3}.A_{1}A_{3} by SU. But we also have ⊢ A_{1}A_{3}.A_{2}A_{3}. By Hyp 1, A_{1}A_{3} ∼ A_{2}A_{3}. Hence, A_{1} ∼ A_{2} and we may proceed as in Case I.

This completes the proof of the theorem.

4. A concluding remark

It is both logically and philosophicaly interesting that substitution of formulas of the form B.CD for subformulas of the form C.BD in a formula A can be identified with CONGR - with the derivability of certain formulas in the weak logical system TRW_{→}+RP.

Also, it is interesting that the same substitution can be identified with NOASS - with the non-derivability of certain formulas.

References

[1] A.R. Anderson, N.D. Belnap, and J. M. Dunn, Entailment, the Logic of Relevance and Necessity, Vol. II, Princeton Univ. Press, 1992, §66.

[2] Y. Komori, Syntactical Investigations into BI Logic and BB′I Logic, Studia Logica 53 (1994), 397–416.

[3] A. Kron, A constructive proof of a theorem in relevance logic, Z. Math. Logik Grund. Math. 31 (1985), 423–430.

[4] A. Kron, Identity and Permutation, Publi. Inst. Math. (Beograd) (N.S.) 57(71), (1995), 165– 178.

[5] A. Kron, Identity, Permutation and Binary Trees, Filomat (Niš) 9:3 (1995), 765–781.

[6] E. Martin and R.K. Meyer, Solution to the P-W problem, J. Symbolic Logic 47 (1982), 869– 887.

Filozofski fakultet (Received 15 10 1997) Univerzitet u Beogradu 11000 Beograd Yugoslavia

krons@mi.sanu.ac.yu