Boolean basis, formula size, and number of modal operators

TL;DR

This paper investigates how the choice of Boolean operators affects the size and succinctness of formulas in modal logic, revealing exponential differences in some cases and equivalences in others, with implications for logic representation.

Contribution

It demonstrates that, unlike propositional logic, modal logic can have exponential increases in formula size when eliminating certain operators, and characterizes the succinctness of Boolean operator sets in modal logic.

Findings

Elimination of bi-implication causes exponential increase in modal formula size.

Boolean operator sets are generally equally succinct in modal logic, except for specific cases.

In S5 modal logic, the choice of Boolean operators does not significantly affect formula size.

Abstract

Is it possible to write significantly smaller formulae when using Boolean operators other than those of the De Morgan basis (and, or, not, and the constants)? For propositional logic, a negative answer was given by Pratt: formulae over one set of operators can always be translated into an equivalent formula over any other complete set of operators with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that elimination of bi-implication is only possible at the cost of an exponential number of occurrences of the modal operator $\lozenge$ and therefore of an exponential increase in formula size, i.e., the De Morgan basis and its extension by bi-implication differ in succinctness. Moreover, we prove that any complete set of Boolean operators agrees in succinctness with the De Morgan basis or with its extension by bi-implication. More precisely, these results are shown for the modal logic $\mathrm{T}$ (and therefore for $\mathrm{K}$). We complement them showing that the modal logic $\mathrm{S5}$ behaves as propositional logic: the choice of Boolean operators has no significant impact on the size of formulae.