Blending margins: The modal logic K has nullary unification type

الأصل · EN

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