

This paper provides a reformulation of OntoClean's notion of Unity and Identity within a formal theory of classes, and evaluates how the reformulations apply to BFO's theory of types, which was previously given within the same formal theory. For Unity, a definition schema and explication together express the underlying dependency between a unifying relation and some proper subrelation of the ‘part of’ relation, which together define how a particular of a class is a whole. For Identity, the notion of an identity criterion is ontologically grounded and formalized as an identity procedure. For both Unity and Identity the formulations are expressed within a sorted first-order logic, where staying within first-order expressivity proved difficult in past work. With our reformulations in hand we evaluate the primary type dichotomy for material entities of BFO, Object and ObjectAggregate. Together with the work that integrates OntoClean's notion of Rigidity with BFO's theory of types, this work augments ongoing efforts to build software designed to evaluate and standardize OBO Foundry candidate ontologies, of which BFO is the upper level ontology.