Between Tw→ and Rw→

Aleksandar Kron

Publications de l'Institut Mathématique, _N_S_63 (1998) no. 77, p. 9

Résumé

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.

Détail

Classification : 03B46