Coequivalence Relations and Descent in Modal Logic

A coequivalence relation over a modal logic L is a formula ρ(p 1 , p 2 ) such that the logic L proves that ρ is an equivalence relation.They were introduced by Ghilardi and Zawadowski in the context of the categorical study of non-classical logics.A coequivalence relation is said to separate variables or to be separating if it corresponds to a conjunction of formulas of the form ψ(p 1 ) ↔ ψ(p 2 ), which serve as explicit definitions of quotients.A logic L where all coequivalence relations are separating is said to have the coequivalence separation property (CoSP).Ghilardi and Zawadowski showed that CoSP fails for IPC.In previous work, the second author showed that such a phenomenon happens already in presumably simpler systems like S5. Ghilardi and Zawadowski therefore raised the question whether a weaker property, formulated in categorical terms related to descent theory, was still true.In this paper, we identify the logical meaning of such a property in relation to CoSP.We introduce the notion of local coequivalence relations, which have the additional structure of a local transition term, ξ (p, q 1 , q 2 , r), intuitively capturing the structure of elements lying in the same fiber.We introduce the local coequivalence separation property (LCoSP), and prove it to be equivalent, in good cases, to the almost Barr-exactness of Alg(L) op f p .We conclude by showing that S5 has the LCoSP.