A dynamic characterization of the pure logic of relevant implication (Q5935796)

In this interesting paper the author shows that the relevance logic \(R_\to\) is given by Modus Ponens, Substitution and the Weak Deduction Rule: WDT If \(\Gamma , A\vdash B\) and \(\Gamma \not\vdash B\) then \(\Gamma \vdash A\to B\). This dynamic logic does not have the usual set-theoretic interpretation by which an additional rule can, at most, supply additional theorems. If EQ \(A\to (A\to B)\vdash B\) is added, an equivalence logic results in which \(\vdash (A\to (A\to B))\to (A \to B)\) is no longer provable! Reviewer's remark: The author calls this equivalence logic \(E_\to\), this notation is usually used for Anderson and Belnap's system for entailment.