Desarzens proved that a formula in one variable and modal degree one is unifiable
in the basic modal logic K if and only if it is unified by one of the four substitutions
p → ⊤, ⊥, □⊥, ♢⊤, equivalently if and only if it is true everywhere on a certain four-point
Kripke frame. We sharpen this in two directions. First, we show that Desarzens’ frame is
minimal and unique: among finite test frames for Fm ({p}, 1), four points are necessary, and
every four-point test frame is isomorphic to Desarzens’…
Read moreDesarzens proved that a formula in one variable and modal degree one is unifiable
in the basic modal logic K if and only if it is unified by one of the four substitutions
p → ⊤, ⊥, □⊥, ♢⊤, equivalently if and only if it is true everywhere on a certain four-point
Kripke frame. We sharpen this in two directions. First, we show that Desarzens’ frame is
minimal and unique: among finite test frames for Fm ({p}, 1), four points are necessary, and
every four-point test frame is isomorphic to Desarzens’ frame. Second, we classify degree-one
ground substitutions in arbitrary finite languages by pairs of sets A, B recording truth at
leaves and nonleaves. Using this classification, we exhibit a fixed formula Ψ ∈ Fm ({p, q}, 1)
which is true everywhere on every Kripke frame under a suitable valuation, but is not unified
by any ground substitution of modal degree at most one. Consequently, no class of Kripke
frames characterises degree-one ground-unifiability on Fm({p, q}, 1).
