Cut-elimination theorem for relevant logics

G. E. Mints

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part V, Tome 32 (1972), pp. 90-97

Résumé

Cut-elimination theorem is proved for $R^+$ that is the positive fragment of $R$ (cf. [4]) supplied with $S4$-modality and intensional conjunction. This gives a decision procedure for the $\{\rightarrow,\,0\}$ fragment of $R$. An extension of cut-elimination theorem to the positive part of Aekermann's calculus $E$ is only sketched. The formula $[(a\to u\vee v)\(a\to(u\to v))]\to(a\to v)$ proposed as a counterexample to the conjencture that the replacement of $A\to B$ by $N(A\to B)$ is an embedding of $E$ into $R^+$. Formula (4) is a counterexample to Anderson's conjencture: if $\rceil((A\to B)\to(C\to D))$ is provable in $E$ then $A\to B$ is too.