Blending margins: The modal logic K has nullary unification type

TL;DR

This paper analyzes the unification properties of the modal logic K, showing it has the worst unification type (nullary) due to specific formula behaviors, and extends these findings to description logic ALC.

Contribution

It provides a complete characterization of unifiers for the formula p → □p in K and demonstrates that K has nullary unification type, contrasting with well-behaved transitive modal logics.

Findings

K satisfies an infinitary variant of the rule of margins.

The formula p → □p in K has a complete set of unifiers.

K has nullary unification type, the worst possible.

Abstract

We investigate properties of the formula $p \to \Box p$ in the basic modal logic K. We show that K satisfies an infinitary weaker variant of the rule of margins $\phi \to \Box\phi / \phi, \neg\phi$, and as a consequence, we obtain various negative results about admissibility and unification in K. We describe a complete set of unifiers (i.e., substitutions making the formula provable) of $p \to \Box p$, and use it to establish that K has the worst possible unification type: nullary. In well-behaved transitive modal logics, admissibility and unification can be analyzed in terms of projective formulas, introduced by Ghilardi; in particular, projective formulas coincide for these logics with formulas that are admissibly saturated (i.e., derive all their multiple-conclusion admissible consequences) or exact (i.e., axiomatize a theory of a substitution). In contrast, we show that in K, the formula $p \to \Box p$ is admissibly saturated, but neither projective nor exact. All our results for K also apply to the basic description logic ALC.