I’ve been looking into some different logics recently, and I think I’ve figured out a way to do Modus Ponens in systems like Visser’s Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). There is a direct translation between formulas of these logics and formulas of Modal Logic, i.e. the Gödel-Tarski translation, except that BPL translates to K4 and FPL to GL.
The rule for BPL (and should be for FPL as well) is as follows:
$i. A \to B$
$.$ $\:\:\:|$
$.$ $\:\:\:|$
$.$ $\:\:\:|$
$j. \:\:|A$
$k. \:\:|B$
where $A$ occurs in a sub-proof strictly deeper than the sub-proof in which $A \to B$ occurs.
The reason I ask is that I know Modus Ponens is invalid for arbitrary formulas without having a reflexive accessibility relation, but I also know that, by definition of $\to$, when $A$ is true at an accessible state, $B$ is also true at that state.
Am I correct that this interpretation soundly preserves/codifies the possible-worlds reasoning inherent in both Modal Logic and those logics with similar sub-proofs to the strict sub-proofs of Modal Logic?