We present a cut-free sequent calculus for a class of first-order theories in negation normal form which include coherent and co-coherent theories alike. All structural rules, including cut, are admissible.

This paper offers a critical reconstruction of the motivations that led to the development of mereology as we know it today, along with a brief description of some problems that define current research in the field.