Christoph Berkholz ; Dietrich Kuske ; Christian Schwarz - Boolean basis, formula size, and number of modal operators

lmcs:14094 - Logical Methods in Computer Science, July 28, 2025, Volume 21, Issue 3 - https://doi.org/10.46298/lmcs-21(3:10)2025
Boolean basis, formula size, and number of modal operatorsArticle

Authors: Christoph Berkholz ; Dietrich Kuske ; Christian Schwarz

    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.


    Volume: Volume 21, Issue 3
    Published on: July 28, 2025
    Accepted on: May 11, 2025
    Submitted on: August 22, 2024
    Keywords: Logic in Computer Science, Logic

    Consultation statistics

    This page has been seen 1100 times.
    This article's PDF has been downloaded 324 times.