Vol. 63 (77), pp. 9--20 (1998)

Previous Article

Next Article

Contents of this Issue

Other Issues

ELibM Journals

ELibM Home



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

Aleksandar Kron

Filozofski fakultet, Beograd, Yugoslavia

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:

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
© 2000--2001 ELibM for the EMIS Electronic Edition