Grimm & Dočekal (2021) — Counting Aggregates, Groups and Kinds

[GD21]

Formalizes the formal core of:

Grimm, S. & Dočekal, M. (2021). Counting aggregates, groups and kinds: Countability from the perspective of a morphologically complex language. In H. Filip (ed.), Countability in Natural Language, 85–120. Cambridge University Press.

The data

Czech makes the individuation scale morphologically visible. Beyond the count/non-count contrast, its derivational morphology targets entity types English leaves undifferentiated:

• Derived aggregates (suffix -í, Table 3.1): countable roots yield strongly non-countable collection nouns — list 'leaf' → listí 'foliage', strom 'tree' → stromoví 'clump of trees' — requiring coherence (spatial proximity, functional interdependence) of the members, with no pluralization, no cardinals ((10)–(11)), and no packaging shifts ((12)).
• Group numerals (-ice, §3.2.2.1): troj-ice námořníků 'a group of three sailors' — animate-only, collective-only interpretation, and the output is fully countable (dvě trojice 'two groups of three', (54)) via [Lan89]-style group formation.
• Aggregate numerals (-oje/-ery, §3.2.2.2): dv-oje klíče 'two sets of keys' — select connected-entity nouns ((21)–(23)), and the output cannot be recounted (*tři dvoje klíče, (27)).
• Taxonomic numerals (-ojí/-ero, §3.2.2.3): dvojí víno 'two kinds of wine' — licensed in both episodic and non-episodic contexts, unlike bare-plural taxonomic readings ((40)).
• Restricted flexibility (§3.2.3): no grinding ((34)–(35)), conventional-only packaging ((8)), episodic-restricted sorting — the inverse of what flexibility-foundational theories predict (§3.3: against Borer's mass-to-count trajectory, since -í manufactures non-countables from countables; against single-source vagueness accounts, since listí's parts are non-vaguely atomic).

The formalization

Their §3.5 extends [Kri95a]'s kind-based semantics with [Gri12] mereotopology ([CV99] connection axioms (56)–(59)). This file formalizes that extension:

• ChainIn/IsCluster/IsMaxCluster — transitive connection (60), cluster individuals (61), maximal clusters (63), over an arbitrary connection relation (their proximate vs external varieties).
• isCluster_sup — joining clusters across a connection yields a cluster: the honest version of their cumulativity remark for -í nouns (sums of connected clusters, not arbitrary sums).
• maxClusters_disjointPred — distinct maximal clusters never overlap: the -oje counting base is disjoint, so aggregate counting is certified by exactly the disjointness that [Lan20]'s counting theorems require (Mereology.DisjointPred; cf. Studies/Landman2020.lean).
• ojeSem_determinate — the (64) semantics fixes the cardinality of maximal clusters uniquely: the formal content of *tři dvoje klíče ((27)) and *všechny dvoje ((26)) — an aggregate-numeral output has determinate cardinality that no outer numeral can re-specify.
• ojiSem and oji_needs_subkinds — the taxonomic numeral (50) is empty on kind-less arguments (proper names, (52b)).
• The individuation-scale junction (third consumer of Features/Individuation.lean): -í is a morphological descent of the scale (isuffix_descends), and the Czech countability map is monotone on it (czech_monotone), the [Gri18] order-preservation thesis in a language where the boundary is drawn by derivation rather than lexical class alone.

Cluster mereotopology (their §3.5.2)

[CV99] connection: a reflexive, symmetric relation C ((56)–(57)); the varieties relevant to aggregates are external and proximate connectedness. Clusters are sums of property-bearers pairwise connected through the cluster ((60)–(61)); maximal clusters absorb every overlapping cluster ((63)).

def GrimmDocekal2021.ChainIn {α : Type u_1} (C : α → α → Prop) (Z : Finset α) : α → α → Prop

(60): connected through a chain of members of Z.

Equations

• GrimmDocekal2021.ChainIn C Z = Relation.ReflTransGen fun (a b : α) => a ∈ Z ∧ b ∈ Z ∧ C a b

def GrimmDocekal2021.IsCluster {α : Type u_1} [SemilatticeSup α] (C : α → α → Prop) (P : α → Prop) (x : α) : Prop

(61): a cluster individual — the sum of a nonempty set of P-entities, pairwise transitively connected through the set.

Equations

• GrimmDocekal2021.IsCluster C P x = ∃ (Z : Finset α) (hZ : Z.Nonempty), (∀ z ∈ Z, P z) ∧ x = Z.sup' hZ id ∧ ∀ z ∈ Z, ∀ z' ∈ Z, GrimmDocekal2021.ChainIn C Z z z'

def GrimmDocekal2021.IsMaxCluster {α : Type u_1} [SemilatticeSup α] (C ov : α → α → Prop) (P : α → Prop) (x : α) : Prop

(63): a maximal cluster absorbs every overlapping cluster.

Equations

• GrimmDocekal2021.IsMaxCluster C ov P x = (GrimmDocekal2021.IsCluster C P x ∧ ∀ (y : α), GrimmDocekal2021.IsCluster C P y → ov y x → y ≤ x)

theorem GrimmDocekal2021.maxClusters_disjointPred {α : Type u_1} [SemilatticeSup α] (C ov : α → α → Prop) {P : α → Prop} (hsym : ∀ (a b : α), ov a b → ov b a) : Mereology.DisjointPred ov {x : α | IsMaxCluster C ov P x}

Maximal clusters are pairwise disjoint (their remark after (63)): two distinct maximal clusters cannot overlap — each would absorb the other. This is what makes the -oje counting base a disjoint set, the precondition the [Lan20] counting theorems certify as sufficient for counting.

theorem GrimmDocekal2021.isCluster_sup {α : Type u_1} [SemilatticeSup α] (C : α → α → Prop) {P : α → Prop} {Z₁ Z₂ : Finset α} (hsymC : ∀ (a b : α), C a b → C b a) (h₁ : Z₁.Nonempty) (h₂ : Z₂.Nonempty) (hP₁ : ∀ z ∈ Z₁, P z) (hP₂ : ∀ z ∈ Z₂, P z) (hc₁ : ∀ z ∈ Z₁, ∀ z' ∈ Z₁, ChainIn C Z₁ z z') (hc₂ : ∀ z ∈ Z₂, ∀ z' ∈ Z₂, ChainIn C Z₂ z z') {z₁ z₂ : α} (hz₁ : z₁ ∈ Z₁) (hz₂ : z₂ ∈ Z₂) (hlink : C z₁ z₂) : IsCluster C P (Z₁.sup' h₁ id ⊔ Z₂.sup' h₂ id)

Joining two clusters connected at some pair of members yields a cluster: the honest form of their cumulativity remark for -í nouns — sums of connected clusters are clusters (arbitrary sums are not, which is exactly why -oje counts maximal clusters). Uses connection symmetry ((57)).

The aggregate numeral -oje (their (64))

def GrimmDocekal2021.ojeSem {α : Type u_1} [SemilatticeSup α] (C ov : α → α → Prop) (n : ℕ) (P : α → Prop) (x : α) : Prop

(64): n-oje P holds of x iff the maximal P-clusters properly below x number exactly n.

Equations

• GrimmDocekal2021.ojeSem C ov n P x = ∃ (Y : Finset α), (∀ (z : α), z < x ∧ GrimmDocekal2021.IsMaxCluster C ov P z ↔ z ∈ Y) ∧ Y.card = n

theorem GrimmDocekal2021.ojeSem_determinate {α : Type u_1} [SemilatticeSup α] (C ov : α → α → Prop) {n m : ℕ} {P : α → Prop} {x : α} (hn : ojeSem C ov n P x) (hm : ojeSem C ov m P x) : n = m

Aggregate-numeral cardinality is determinate: the witnessing set of (64) is the set of maximal clusters below x, so its cardinality is unique. This is the formal content of *tři dvoje klíče ((27)) and *všechny dvoje ((26)): the output of an aggregate numeral cannot be re-specified by an outer cardinal — unlike the -ice group numerals, whose [Lan89]-style group atoms are freely recountable (dvě trojice, (54)).

The taxonomic numeral -ojí (their (50))

def GrimmDocekal2021.ojiSem {κ : Type u_2} (T : κ → κ → Prop) (n : ℕ) (k : κ) (X : Finset κ) : Prop

(50), extensionalized over a subkind relation T: n-ojí k holds of a set of kinds all of which are subkinds of k, numbering n.

Equations

• GrimmDocekal2021.ojiSem T n k X = ((∀ z ∈ X, T z k) ∧ X.card = n)

theorem GrimmDocekal2021.oji_needs_subkinds {κ : Type u_2} {T : κ → κ → Prop} {k : κ} (hk : ∀ (z : κ), ¬T z k) {n : ℕ} (hn : n ≠ 0) : ¬∃ (X : Finset κ), ojiSem T n k X

Kind-less arguments defeat the taxonomic numeral ((52): #dvojí Petr Novák — proper names supply no subkinds).

The individuation-scale junction (their Table 3.1, §3.2.1)

Third consumer of Features/Individuation.lean. The suffix -í maps individuated roots to coherent-collection denotations — a morphological descent of the scale ([Gri18]'s types) — and Czech's countability boundary is monotone on the scale, with the twist that the collective-aggregate region is populated derivationally.

structure GrimmDocekal2021.DerivedAggregate : Type

A Table 3.1 row: root, derived aggregate, glosses.

• root : String
• rootGloss : String
• derived : String
• derivedGloss : String

def GrimmDocekal2021.instDecidableEqDerivedAggregate.decEq (x✝ x✝¹ : DerivedAggregate) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GrimmDocekal2021.instDecidableEqDerivedAggregate : DecidableEq DerivedAggregate

Equations

• GrimmDocekal2021.instDecidableEqDerivedAggregate = GrimmDocekal2021.instDecidableEqDerivedAggregate.decEq

def GrimmDocekal2021.instReprDerivedAggregate.repr : DerivedAggregate → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GrimmDocekal2021.instReprDerivedAggregate : Repr DerivedAggregate

Equations

• GrimmDocekal2021.instReprDerivedAggregate = { reprPrec := GrimmDocekal2021.instReprDerivedAggregate.repr }

def GrimmDocekal2021.table31 : List DerivedAggregate

A sample of Table 3.1 (trees, plants, complex objects, nautical terms). Roots are countable individual nouns (their fn. 5: 21 of the 22 listed roots are purely countable; dřevo 'wood' is the ambiguous exception).

Equations

• One or more equations did not get rendered due to their size.

def GrimmDocekal2021.rootType : IndividuationType

The scale position of -í inputs (countable individual roots) and outputs (coherent collections — spatial proximity or functional interdependence, their §3.2.1).

Equations

• GrimmDocekal2021.rootType = IndividuationType.individualEntity

def GrimmDocekal2021.derivedType : IndividuationType

Equations

• GrimmDocekal2021.derivedType = IndividuationType.collectiveAggregate

theorem GrimmDocekal2021.isuffix_descends : derivedType < rootType

-í descends the individuation scale: derivational morphology moves a noun from the individual region into the collective-aggregate region — the inverse of the mass-to-count trajectory flexibility-foundational theories predict (their §3.3 against Borer).

inductive GrimmDocekal2021.CzechClass : Type

Czech grammatical countability (combination with simple cardinals, pluralization, mnozí): individuals are count (pes, (4)); substances (bláto, (5)), granulars (písek, (8b)), and derived aggregates (listí, (9)–(11)) are non-count.

• nonCount : CzechClass
• count : CzechClass

@[implicit_reducible]

instance GrimmDocekal2021.instDecidableEqCzechClass : DecidableEq CzechClass

Equations

• GrimmDocekal2021.instDecidableEqCzechClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GrimmDocekal2021.instReprCzechClass.repr : CzechClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GrimmDocekal2021.instReprCzechClass : Repr CzechClass

Equations

• GrimmDocekal2021.instReprCzechClass = { reprPrec := GrimmDocekal2021.instReprCzechClass.repr }

def GrimmDocekal2021.CzechClass.toNat : CzechClass → ℕ

Equations

• GrimmDocekal2021.CzechClass.nonCount.toNat = 0
• GrimmDocekal2021.CzechClass.count.toNat = 1

@[implicit_reducible]

instance GrimmDocekal2021.instLinearOrderCzechClass : LinearOrder CzechClass

Equations

• GrimmDocekal2021.instLinearOrderCzechClass = LinearOrder.lift' GrimmDocekal2021.CzechClass.toNat GrimmDocekal2021.instLinearOrderCzechClass._proof_1

def GrimmDocekal2021.czechClassify : IndividuationType → CzechClass

The Czech countability map on the individuation scale.

Equations

• GrimmDocekal2021.czechClassify IndividuationType.substance = GrimmDocekal2021.CzechClass.nonCount
• GrimmDocekal2021.czechClassify IndividuationType.granularAggregate = GrimmDocekal2021.CzechClass.nonCount
• GrimmDocekal2021.czechClassify IndividuationType.collectiveAggregate = GrimmDocekal2021.CzechClass.nonCount
• GrimmDocekal2021.czechClassify IndividuationType.individualEntity = GrimmDocekal2021.CzechClass.count

theorem GrimmDocekal2021.czech_monotone : Monotone czechClassify

Czech draws its countability boundary monotonically on the individuation scale — the [Gri18] order-preservation thesis, holding in a language where the collective-aggregate region is reached by derivation (-í) rather than only by lexical class.

theorem GrimmDocekal2021.isuffix_decountabilizes : czechClassify rootType = CzechClass.count ∧ czechClassify derivedType = CzechClass.nonCount

The derivational route: -í carries a count root to a non-count output — countability change without coercion, the data point against derive-count-from-mass architectures (their §3.3).