3.2. What a description logic cannot express
A description logic captures the taxonomy but is structurally unable to capture the calculus. The recurring gap is arithmetic, operations, definedness-conditions, laws, and proofs:
-
Dimension arithmetic (
\dim(a\cdot b) = \dim a + \dim b): OWL2 has no datatype arithmetic; in Lean it is an ordinary function with a homomorphism theorem. -
The interaction algebra (torque
\timesangle=energy): role chains are binary, regular, and carry no arithmetic side-conditions; in Lean it is a ternary relation with a dimensional-coherence proof obligation. -
Scale-type operator gating (which of
=,<,+,\timesare defined): DL has no operations; in Lean the scale indexes which typeclasses apply, and monotonicity of availability is a proved meta-theorem. -
Extensivity (
\mathrm{value}(\text{whole}) = \sum \mathrm{value}(\text{parts})): no quantified arithmetic in DL; in Lean it is a\forall-theorem. -
Units (a unit is a chosen value of a kind; conversion is a ratio): no arithmetic in DL; in Lean it is a definition with a round-trip theorem.
-
Meta-theorems (specialization is a preorder;
\dimis a homomorphism): a DL reasoner checks consistency, not laws — proving the laws is the point.