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 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.