  We introduce labelled sequent calculi for the basic normal non-distributive
modal logic L and 31 of its axiomatic extensions, where the labels are atomic
formulas of a first order language which is interpreted on the canonical
extensions of the algebras in the variety corresponding to the logic L. Modular
proofs are presented that these calculi are all sound, complete and
conservative w.r.t. L, and enjoy cut elimination and the subformula property.
The introduction of these calculi showcases a general methodology for
introducing labelled calculi for the class of LE-logics and their analytic
axiomatic extensions in a principled and uniform way.
