15. Extensivity🔗

Dybkær §13.5 divides kinds-of-quantity "according to physical (and arithmetic) additivity", presenting Bunge's four types: unconditionally extensive (§13.5.1, the value for the total equals the arithmetic sum over the parts), quasiextensive (§13.5.2, approximately equal — an uncertainty question, not a mereological one), conditionally extensive (§13.5.3, the addition exists but the total may differ "due to the respective internal and environmental conditions" — volume on mixing), and intensive (§13.5.4, no physical addition, the value "invariant with the extent of a system of constant composition"). These are quantified arithmetic laws over the mereology of systems — again something a description logic cannot state — and all four are realized, sorry-free: three of them in the Mathlib-free Extensivity module — the predicates over the Mereology module's carving, the two inductions that lift a single split to the whole tree, and a checked witness for each — and §13.5.2 in Uncertainty.QuasiExtensive, because "approximately" is a claim about measurement and not about the mereology.

Four cases Bunge's four do not name are added. A value the parts do not determine at all (whole-proper); a value that adds only about a shared parameter — an axis, a frame, a reference point — where the parallel-axis theorem lives and the transport tower with it; a weighted mean, which is neither a sum nor a shared constant and whose license is that the total weight is not zero; and a value that reads no part at all but an interface between two, whose additivity is purchased by a cancellation law. The chapter closes on what a carving cannot say at all: how many parts there are.