Inverse images of box formulas in modal logic (Q383565)

The paper investigates some properties of modal logics that do not have the cancellation rule ``from \(\square A \leftrightarrow \square B\) infer \(A \leftrightarrow B\)''. The latter is the converse of the congruence rule (alias the rule of equivalents) ``from \(A \leftrightarrow B\) infer \(\square A \leftrightarrow \square B\)''. When the congruence rule is admissible -- as is the case, e.g. in the basic modal logic \(\mathsf{K}\) -- then for a given formula \(A\), every formula \(B\) such that \(\square A\) is logically equivalent to \(\square B\) must be logically equivalent to \(A\). This is not necessarily the case for logics where the cancellation rule is not admissible. It makes therefore sense to define the \textit{inverse image} of \(A\) in logic \(\mathsf{S}\), noted \(\square^{{-}1}[A]^{\mathsf{S}}\), as the set of all \(B\) such that \(\square B\) is logically equivalent to \(\square A\) in \(\mathsf{S}\). The paper investigates the properties of that set. It is shown that (1) for some \(\mathsf{S}\) such as \(\mathsf{K}\), \(\square^{{-}1}[A]^{\mathsf{S}}\) is a singleton up to logical equivalence; (2) for some \(\mathsf{S}\) such as \(\mathsf{S4}\), each \(\square^{{-}1}[A]^{\mathsf{S}}\) has elements that are logically strongest up to logical equivalence (such as \(\square B\) in the case of \(\mathsf{S4}\)); (3) for some \(\mathsf{S}\), each \(\square^{{-}1}[A]^{\mathsf{S}}\) has elements that are logically strongest and elements that are logically weakest, up to logical equivalence; (4) for some \(\mathsf{S}\) such as \(\mathsf{KD45}\), there are formulas \(A\) such that \(\square^{{-}1}[A]^{\mathsf{S}}\) has neither strongest nor weakest elements. It is also shown that there are logics such as \(\mathsf{KT}\) where there is no general result: while \(\square^{{-}1}[\square p]^{\mathsf{KT}}\) contains logically strongest and weakest formulas, this does not necessarily hold when the propositional variable \(p\) is replaced by a complex formula.