Hyperformalism for Relevant Modal Logics

The property of hyperformalism has proven to be a powerful tool in the analysis of relevant logics, revealing that increasingly weak relevant logics are closed under increasingly strong classes of non-uniform substitutions. In such substitutions, two instances of the same atom may be treated independently in virtue of syntactic features of their appearances in a complex. In this work, we extend the scope of hyperformalism to relevant modal logics by considering MPos-hyperformalism, that is, a property in which relevant modal logics are closed under substitutions in which nesting within the scope of modal operators is taken into account. We prove that the weak relevant modal logic B-Box is MPos-hyperformal and investigate the classes of non-uniform substitutions under which several extensions are closed. We then consider corresponding refinements of the variable sharing property that hold of such logics. We conclude by introducing a modal logic K-MPos that constitutes the largest MPos-hyperformal sublogic of the classical modal logic K and provide soundness and completeness results.