  We introduce sound and complete labelled sequent calculi for the basic normal
non-distributive modal logic L and some of its axiomatic extensions, where the
labels are atomic formulas of the first order language of enriched formal
contexts, i.e., relational structures based on formal contexts which provide
complete semantics for these logics. We also extend these calculi to provide a
proof system for the logic of rough formal contexts.
