8.2. The ontological square🔗

The correspondence with Lowe's four-category ontology ( (Lowe, 2005)E. J. Lowe (December 2005). “The Four-Category Ontology: A Metaphysical Foundation for Natural Science”. Oxford University Press. ., Fig. 7.1 — the ontological square) is worth stating edge by edge, because the calculus carries the relations of the square and not only its corners. The corners: SortOfSystem is his Kinds (the substantial universal), the object index his Substances (the substantial particular), KindOfProperty his Attributes (the non-substantial universal), IndividualQuantity his Modes. The edges: Sorted.sortOf is the left instantiated by edge — substances instantiate kinds. The right instantiated by edge — modes instantiate attributes — is the kind index of an individual quantity, and the bottom characterized by edge — substances characterized by modes — is its object index: both edges into the mode are carried in the type of an individual quantity, which is what puts the arithmetic under the type checker — two quantities disagreeing on either edge are of two different types, so nothing combines them, and the refusal is the compiler's rather than a convention's. The top characterized by edge — kinds characterized by attributes — is the dedicated kind (the dedicated-kinds chapter), refined by Dybkær's pertinent component, a refinement the square itself does not carry.

Figure 1, up front, draws the square with the calculus's identifiers at its corners and these mechanisms on its edges, and two things it shows are worth reading against the correspondence just stated. The two heavy edges are the two type indices of an individual quantity — the object index o along the bottom and the kind index k down the right — and the plates behind the Modes corner are the carrier R, which indexes that corner alone: R is no ontological category and has neither a corner nor an edge, so a change of carrier stacks copies of the mode and moves nothing else. The columns and rows are braced because the square's whole content is a two-by-two — universals over particulars, substantial beside non-substantial — and naming the columns keeps the two senses of kind apart: Lowe's Kinds corner is a kind of system, while the k of Quantity k R is a kind-of-property, the Attributes corner.

A word on index, which this chapter uses throughout. In Lean's own vocabulary the arguments of IndividualQuantity are structure parameters: a structure has no indices, those being the arguments an inductive declares to the right of the colon and may vary from one constructor to the next. The prose says index deliberately, because what the correspondence needs to name is the role rather than the declaration form — each argument is fixed in the type of any given quantity, so that two quantities differing in one of them are of two different types, and that is the property the square's edges are identified with here. A reader who wants the declaration's own term should read parameter wherever this chapter writes index.

The diagonal is a structural agreement rather than a construct. Lowe's exemplified by — a substance exemplifying an attribute — is derivative for him, factoring through either path around the square, and the calculus likewise has no primitive object-to-kind-of-property construct: the dispositional route (up the left edge, then across the top) is dedicatedFor, and the occurrent route (across the bottom, then up the right) is an inhabitant of IndividualQuantity o k R. The reading is not idiosyncratic: surveying the square's grounding relations, Simons states the occurrent half as a definition — an object exemplifies an attribute "when a mode which instantiates an attribute characterizes an object" — and counts exemplification "definable in terms of instantiation, characterization, and some logic"  (Simons, 2018)Peter Simons, 2018. “Lowe, the Primacy of Metaphysics, and the Basis of Categorial Distinctions”. In Ontology, Modality, and Mind: Themes from the Metaphysics of E. J. Lowe (Oxford University Press).. Where the calculus narrows Lowe: the attributes here are kinds-of-property specifically — quantitative attributes carrying a scale and an examination — not attributes at large.

One stance the implementation takes silently is worth making explicit. The calculus's universals are catalogue entries: a SortOfSystem and a KindOfProperty are data, declared by a model, and a sort no object instantiates is idle data rather than a Platonic surplus. That is the immanentist reading Lowe himself settled on — universals as "abstractions from, or invariants across, particulars", incapable of existing uninstantiated (Lowe 2012, quoted in Heil  (Heil, 2018)John Heil, 2018. “Existents and Universals”. In Ontology, Modality, and Mind: Themes from the Metaphysics of E. J. Lowe (Oxford University Press).) — and it is the only reading a terminological ontology in Dybkær's style needs.