PUBLICATIONS DE L'INSTITUT MATHÉMATIQUE (BEOGRAD) (N.S.) Vol. 63 (77), pp. 920 (1998) 

Between TW$_{\to}$ and RW$_{\to}$Aleksandar KronFilozofski fakultet, Beograd, YugoslaviaAbstract: We investigate some pure implicational systems placed between the implicational fragments TW$_{\to}$ and RW$_{\to}$ of the wellknown relevance systems TW and RW For one them, TRW$_{\to}+$RP, we prove (1) and (2): (1) if both $\vdash A\rightarrow B$ and $\vdash B\rightarrow A$ in TRW$_{\to}+$RP, then $B$ can be obtained from $A$ by substitution of occurrences of formulas of the form $D\to.C\to E$ for some occurrences of subformulas of $A$ of the form $C\to.D\to E$ (CONGR); (2) CONGR is equivalent to NOASS: for any $A$ and $B$, $$ \not \vdash A\to .A\to B\to B $$ in TRW$_{\to}+$RP. \par CONGR is a generalization of the solution to the PW problem, solved for TW$_{\to}$ in [6] (cf.\ also [1][4] for other solutions). \par The equivalence of CONGR and NOASS is a generalization of the DwyerPowers theorem for TW$_{\to}$ to the effect that the PW problem is equivalent to NOID: there is no theorem of TW$_{\to}$ID of the form $AA$. \par The proof of the equivalence of CONGR and NOASS is obtained by double induction applied jointly with a normal form theorem. Classification (MSC2000): 03B46 Full text of the article:
Electronic fulltext finalized on: 6 Apr 2000. This page was last modified: 16 Nov 2001.
© 2000 Mathematical Institute of the Serbian Academy of Science and Arts
