Blending margins: The modal logic K has nullary unification type

Abstract

We investigate properties of the formula $p\to \square p$ in the basic modal logic K. We show that K satisfies an infinitary weaker variant of the rule of margins $\varphi \to \square \varphi /\varphi ,\neg \varphi$, 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 \square 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 \square p$ is admissibly saturated, but neither projective nor exact. All our results for K also apply to the basic description logic ALC.

12 pages, 1 figure

References in corpus (1)

• Unification in the Description Logic EL

Cited by in corpus (3)

• Exact Unification and Admissibility
• About the unification types of the modal logics determined by classes of deterministic frames
• Unification in pretabular extensions of S4