15.1. Extensive and conditionally-extensive kinds (Dybkær §13.5)🔗

Definition15.1.1

Group: Mass is extensive: the mass of a whole is the sum of the masses of its parts. Volume on mixing is not: ethanol and water mix sub-additively. Tracking which kinds are extensive is a precondition for soundly aggregating measurements. (30)

Group member previews

Preview

Theorem 15.1.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 8.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 10

Reverse dependency previews

Preview

Theorem 10.1.9

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A kind is extensive when, for any carving of a system into parts, the quantity of the whole equals the sum over the parts — the mereological structure the foundations chapter supplies.

Lean code for Definition15.1.1●1 definition

structure(2 fields)defined in PropertyKindCalculus/Extensivity.lean

complete

structure PropertyKindCalculus.Extensive.{u} {O : Type u}
  (k : PropertyKindCalculus.KindOfProperty)
  (m : PropertyKindCalculus.Measurement O) : Prop

structure PropertyKindCalculus.Extensive.{u}
  {O : Type u}
  (k :
    PropertyKindCalculus.KindOfProperty)
  (m :
    PropertyKindCalculus.Measurement O) :
  Prop

**§13.5 extensive kind.** A kind `k` is *extensive* under a measurement `m`
when (i) every part is measured as a value *of kind* `k` (one shared reference, so
the numerals are commensurable) and (ii) the numeral on a disjoint union is the sum
of the numerals on the parts. Mass satisfies this; volume on mixing does not.

Fields

ofKind : ∀ (d : PropertyKindCalculus.Decomposition O), (m d).kind = k

Every measured part is a value of the kind `k`.

additive : ∀ (a b : PropertyKindCalculus.Decomposition O), (m (a.union b)).numeral = (m a).numeral + (m b).numeral

The single-split additivity law: a union measures as the sum of its two parts.

Proof for Definition 15.1.1

uses 0

Realized as Extensive k m, a predicate over a kind k and a measurement m (the property value observed on each node of a Decomposition): it asserts that every part is measured as a value of kind k, and that the numeral on a disjoint union is the sum of the numerals on its two parts.

Theorem15.1.2

Group member previews

Preview

Definition 15.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

EffortmediumTagscapstoneproved

Extensive aggregation. For an extensive kind k and a system decomposed into parts s_1, \dots, s_n, \mathrm{value}_k\Bigl(\bigsqcup_i s_i\Bigr) = \sum_i \mathrm{value}_k(s_i). The \forall-quantified additivity law itself — not a single instance — is the deliverable, and it is exactly what OWL2 has no vocabulary for. Builds on extensive kinds.

Lean code for Theorem15.1.2●1 theorem

theoremdefined in PropertyKindCalculus/Extensivity.lean

complete

theorem PropertyKindCalculus.extensive_additive.{u} {O : Type u}
  {k : PropertyKindCalculus.KindOfProperty}
  {m : PropertyKindCalculus.Measurement O}
  (h : PropertyKindCalculus.Extensive k m)
  (d : PropertyKindCalculus.Decomposition O) :
  (m d).numeral = PropertyKindCalculus.leafSum m d

theorem PropertyKindCalculus.extensive_additive.{u}
  {O : Type u}
  {k :
    PropertyKindCalculus.KindOfProperty}
  {m : PropertyKindCalculus.Measurement O}
  (h : PropertyKindCalculus.Extensive k m)
  (d :
    PropertyKindCalculus.Decomposition
      O) :
  (m d).numeral =
    PropertyKindCalculus.leafSum m d

**Extensive aggregation (the capstone).** For an extensive kind, the value
measured on the *whole* equals the sum over *all* atomic parts of a decomposition,
$$`\mathrm{value}\Bigl(\bigsqcup_i s_i\Bigr) = \sum_i \mathrm{value}(s_i),`
to arbitrary depth. The $`\forall`-quantified law itself — not a single instance —
is the deliverable: it is proved by induction on the decomposition, lifting the
single-split `additive` field to the whole tree.

Proof for Theorem 15.1.2

uses 0

Proved in the Extensivity module by induction on the Decomposition: at a leaf the law is reflexivity; at a union the single-split additive field plus the two induction hypotheses give the numeral of the whole as the sum of the leaf sums.

Theorem15.1.3

Group member previews

Preview

Definition 15.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Counterexample — volume on mixing is not extensive. Volume fails the additivity law for a water/ethanol mixture: the volume of the mixture is strictly less than the sum of the component volumes. Stating the negation keeps the extensive predicate honest. Uses extensive kinds.

Lean code for Theorem15.1.3●1 theorem

theoremdefined in PropertyKindCalculus/Extensivity.lean

complete

theorem PropertyKindCalculus.mixing_subadditive :
  (PropertyKindCalculus.volMix PropertyKindCalculus.mixture).numeral <
      (PropertyKindCalculus.volMix
            PropertyKindCalculus.waterPart).numeral +
        (PropertyKindCalculus.volMix
            PropertyKindCalculus.ethanolPart).numeral ∧
    ¬PropertyKindCalculus.Extensive PropertyKindCalculus.volume
        PropertyKindCalculus.volMix

theorem PropertyKindCalculus.mixing_subadditive :
  (PropertyKindCalculus.volMix
          PropertyKindCalculus.mixture).numeral <
      (PropertyKindCalculus.volMix
            PropertyKindCalculus.waterPart).numeral +
        (PropertyKindCalculus.volMix
            PropertyKindCalculus.ethanolPart).numeral ∧
    ¬PropertyKindCalculus.Extensive
        PropertyKindCalculus.volume
        PropertyKindCalculus.volMix

**Volume on mixing is not extensive.** The mixture's volume is *strictly less*
than the sum of the component volumes (96 < 50 + 50), so additivity fails and
`volume` is not extensive under this measurement. Matching the extensive law would
be unsound here — which is exactly why extensivity must be tracked, not assumed.

Proof for Theorem 15.1.3

uses 0

Proved in the Extensivity module. 50 mL of water and 50 mL of ethanol measure 96 mL when mixed; the strict inequality 96 < 50 + 50 is by decide, and the same volMix measurement witnesses \neg\,\mathrm{Extensive}\ \mathrm{volume} by refuting its additive field on that two-part decomposition.