Between TW$_{\to}$ and RW$_{\to}$

Aleksandar Kron

Abstract: We investigate some pure implicational systems placed between the implicational fragments TW$_{\to}$ and RW$_{\to}$ of the well-known 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 P--W 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 Dwyer-Powers theorem for TW$_{\to}$ to the effect that the P--W 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:

• Compressed DVI file (20 kilobytes)
• PostScript file (159 kilobytes)
• Compressed PostScript file (62 kilobytes)
• PDF file (158 kilobytes)