Sutton & Filip (2021) — The Count/Mass Distinction for Granular Nouns

[SF21]

Formalizes the core of:

Sutton, P. R. & Filip, H. (2021). The count/mass distinction for granular nouns. In H. Filip (ed.), Countability in Natural Language, 252–291. Cambridge University Press.

The account

Lexical entries are tripartite (their (33)): a basic predicate (baspred, number-neutral conceptual content), a counting base (cbase), and an extension. Two mechanisms mediate between them: the object identifying function 𝒪 (their (30)), which selects the perceptually/functionally salient units if the concept specifies any, and individuation schemas 𝒮ᵢ, which select a maximally disjoint subset of those units; the null schema 𝒮₀ (their (32)) instead unions all maximally disjoint subsets. Grammatical counting requires a disjoint counting base, so:

• count = [+O, +S] (a specific schema over identified objects — cat, lentil, Finnish huonekalut 'items of furniture');
• mass = [−S] (null schema): either [+O, −S] (furniture — objects identified but overlapping, so cardinality comparison is available) or [−O, −S] (rice, Czech čočka 'lentil', mud — no object function in the counting base at all).

The accessibility puzzle: rice denotes stuff made of perceptually salient, disjoint grains, yet #three rices cannot mean 'three grains of rice' (only container/subkind readings). On this account the grains live in baspred but are not passed to cbase — and an implicit unit-extracting shift would be a generalized [−O,−S] → [+O,+S] operation, incompatible with a lexicalized mass/count distinction (their §9.5.4; Yudja, which lacks one, counts everything — cf. Grimm2018.yudjaClassify).

Main declarations

• OverlapPred/IsMaxDisjointIn/nullSchema — the schema machinery over an arbitrary overlap relation. The disjoint-counting-base thesis and the multiple-perspectives ("variants") idea this packages originate with [Lan11] and [Lan16]; the chapter's own contribution is the null schema 𝒮₀ and the unified 𝒪/𝒮ᵢ mechanism. The machinery is a graduation candidate when a Landman-anchored study lands.
• overlapPred_union_of_maxDisjoint_ne — the load-bearing generic fact: the union of two distinct maximal disjoint subsets overlaps. Hence nullSchema-saturated entries are mass whenever individuation is perspectival (overlapPred_nullSchema), and stable for prototypical objects (nullSchema_eq_of_disjoint).
• Categorization ([±O, ±S]) and Table 9.1 (table91) over the graduated individuation scale (Features/Individuation.lean), with the junction theorems: the count option ascends the scale (count_option_monotone) and the mass option descends it (mass_option_antitone). Ordering Table 9.1 by [Gri18]'s scale is this study's bridge, not the chapter's (it cites [Gri12] and Grimm & Levin 2017, not [Gri18]); the theorems show the two frameworks' landscapes coincide.
• A concrete furniture/rice model on nonempty Finsets: furniture's identified units overlap (table vs. vanity), rice's grains are disjoint in baspred yet its counting base overlaps — the accessibility puzzle's two halves (furniture_units_overlap, rice_accessibility).

Connections

• Second consumer of the individuation scale — the graduation that moved IndividuationType to Features/Individuation.lean (with [Gri18]).
• MassCount records the outcome of categorization (Categorization.massCount); the [±O, ±S] features are its analysis.
• The cluster/MSSC content of granular baspred frames is [Gri12]'s mereotopology ([CV99] self-connection), not formalized here.
• Their counting condition (cardinality only over disjoint bases, their (A1), after [Lan11]'s overlap thesis) is the semantic ground for why countability classes, not Number values, carry the count/mass distinction (Features/Number/Basic.lean).

Overlap, disjointness, and individuation schemas

Their (16)–(18): the schema machinery (Mereology.OverlapPred, Mereology.IsMaxDisjointIn, Mereology.nullSchema for 𝒮₀, their (32)) lives in Semantics/Mereology.lean, shared with [Lan20] (Studies/Landman2020.lean), whose disjointness thesis it packages. A predicate is overlapping if two distinct members overlap (their (17) omits the distinctness, under which any inhabited predicate self-overlaps via x ∘ x; the substrate states the intended reading).

The [±O, ±S] categorization and Table 9.1

[+O]: the counting base contains the object identifying function 𝒪; [+S]: it is interpreted under a specific schema 𝒮ᵢ rather than 𝒮₀. Count nouns are [+O, +S]; mass nouns are [−S].

structure SuttonFilip2021.Categorization : Type

The two binary features classifying counting bases (their §9.4.4).

• hasObjectFn : Bool

  The counting base contains the object identifying function 𝒪.

• hasSpecificSchema : Bool

  The counting base is interpreted under a specific schema 𝒮ᵢ (rather than the null schema 𝒮₀).

def SuttonFilip2021.instDecidableEqCategorization.decEq (x✝ x✝¹ : Categorization) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance SuttonFilip2021.instDecidableEqCategorization : DecidableEq Categorization

Equations

• SuttonFilip2021.instDecidableEqCategorization = SuttonFilip2021.instDecidableEqCategorization.decEq

@[implicit_reducible]

instance SuttonFilip2021.instReprCategorization : Repr Categorization

Equations

• SuttonFilip2021.instReprCategorization = { reprPrec := SuttonFilip2021.instReprCategorization.repr }

def SuttonFilip2021.instReprCategorization.repr : Categorization → ℕ → Std.Format

Equations

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

def SuttonFilip2021.Categorization.massCount : Categorization → MassCount

Count iff [+O, +S]; everything [−S] is mass (Table 9.1's generalizations).

Equations

• { hasObjectFn := true, hasSpecificSchema := true }.massCount = MassCount.count
• x✝.massCount = MassCount.mass

def SuttonFilip2021.table91 : IndividuationType → List Categorization

Table 9.1: the categorization options available to each notional class, stated over the graduated individuation scale. Substances are [−O, −S] only (mud); granulars lexicalize either way (lentil vs rice/čočka); collective artifacts are [+O, ±S] (huonekalut vs furniture); prototypical objects are [+O, +S] (cat).

Equations

• SuttonFilip2021.table91 IndividuationType.substance = [{ hasObjectFn := false, hasSpecificSchema := false }]
• SuttonFilip2021.table91 IndividuationType.granularAggregate = [{ hasObjectFn := true, hasSpecificSchema := true }, { hasObjectFn := false, hasSpecificSchema := false }]
• SuttonFilip2021.table91 IndividuationType.collectiveAggregate = [{ hasObjectFn := true, hasSpecificSchema := true }, { hasObjectFn := true, hasSpecificSchema := false }]
• SuttonFilip2021.table91 IndividuationType.individualEntity = [{ hasObjectFn := true, hasSpecificSchema := true }]

theorem SuttonFilip2021.count_option_monotone : Monotone fun (i : IndividuationType) => (table91 i).any fun (c : Categorization) => c.hasObjectFn && c.hasSpecificSchema

A count lexicalization is available from granular aggregates upward — availability of [+O, +S] is monotone on the individuation scale.

theorem SuttonFilip2021.mass_option_antitone : Antitone fun (i : IndividuationType) => (table91 i).any fun (c : Categorization) => !c.hasSpecificSchema

A mass lexicalization is available from collective aggregates downward — availability of [−S] is antitone on the scale. Together with count_option_monotone, this is [Gri18]'s Table 20 landscape derived from the [±O, ±S] analysis: the count/mass boundary can only fall across the scale, never gerrymander it.

theorem SuttonFilip2021.variable_classes : (∀ (i : IndividuationType), table91 i ≠ []) ∧ ∀ (i : IndividuationType), (table91 i).length = 2 ↔ i = IndividuationType.granularAggregate ∨ i = IndividuationType.collectiveAggregate

Every notional class has at least one lexicalization, and the cross-linguistically variable classes (granular, collective artifact) are exactly those with two ([SF21] §9.3.1: lentil vs čočka, furniture vs huonekalut).

A concrete model: furniture and rice

Carrier: nonempty subsets of a small atom domain, overlap = nonempty intersection. Furniture (their §9.4.2–9.4.3): a table t, a mirror m, and the vanity t ⊔ m are all functional units, so 𝒪(furniture) overlaps — two individuation perspectives exist (count the vanity as one, or the table and mirror as two). Rice: the basic predicate knows the grains (disjoint!) and their aggregates, but the [−O, −S] counting base is the null schema over the whole predicate — overlapping. The grains are real and inaccessible: the accessibility puzzle.

def SuttonFilip2021.fovl (s t : Finset (Fin 3)) : Prop

Mereological overlap on Finset parts: nonempty intersection.

Equations

• SuttonFilip2021.fovl s t = (s ∩ t).Nonempty

@[implicit_reducible]

instance SuttonFilip2021.instDecidableFovl (s t : Finset (Fin 3)) : Decidable (fovl s t)

Equations

• SuttonFilip2021.instDecidableFovl s t = SuttonFilip2021.instDecidableFovl._aux_1 s t

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetInsert_linglib {a : Finset (Fin 3)} {P : Set (Finset (Fin 3))} [DecidablePred fun (x : Finset (Fin 3)) => x ∈ P] : DecidablePred fun (x : Finset (Fin 3)) => x ∈ insert a P

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetInsert_linglib x = decidable_of_iff (x = a ∨ x ∈ P) ⋯

@[implicit_reducible]

instance SuttonFilip2021.instDecidableOverlapPredFinsetFinOfNatNatFovlOfDecidablePredMemSet {P : Set (Finset (Fin 3))} [DecidablePred fun (x : Finset (Fin 3)) => x ∈ P] : Decidable (Mereology.OverlapPred fovl P)

Equations

• SuttonFilip2021.instDecidableOverlapPredFinsetFinOfNatNatFovlOfDecidablePredMemSet = id inferInstance

@[implicit_reducible]

instance SuttonFilip2021.instDecidableDisjointPredFinsetFinOfNatNatFovlOfDecidablePredMemSet {P : Set (Finset (Fin 3))} [DecidablePred fun (x : Finset (Fin 3)) => x ∈ P] : Decidable (Mereology.DisjointPred fovl P)

Equations

• SuttonFilip2021.instDecidableDisjointPredFinsetFinOfNatNatFovlOfDecidablePredMemSet = decidable_of_iff (¬Mereology.OverlapPred SuttonFilip2021.fovl P) ⋯

@[implicit_reducible]

instance SuttonFilip2021.instDecidableSubsetSetFinsetFinOfNatNatOfDecidablePredMem_linglib {P Q : Set (Finset (Fin 3))} [DecidablePred fun (x : Finset (Fin 3)) => x ∈ P] [DecidablePred fun (x : Finset (Fin 3)) => x ∈ Q] : Decidable (P ⊆ Q)

Equations

• SuttonFilip2021.instDecidableSubsetSetFinsetFinOfNatNatOfDecidablePredMem_linglib = decidable_of_iff (∀ x ∈ P, x ∈ Q) ⋯

@[implicit_reducible]

instance SuttonFilip2021.instDecidableIsMaxDisjointInFinsetFinOfNatNatFovlOfDecidablePredMemSet {D P : Set (Finset (Fin 3))} [DecidablePred fun (x : Finset (Fin 3)) => x ∈ D] [DecidablePred fun (x : Finset (Fin 3)) => x ∈ P] : Decidable (Mereology.IsMaxDisjointIn fovl D P)

Equations

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

def SuttonFilip2021.furnitureUnits : Set (Finset (Fin 3))

The identified units of furniture on a two-atom domain: table {0}, mirror {1}, and the vanity {0, 1} they jointly compose.

Equations

• SuttonFilip2021.furnitureUnits = {s : Finset (Fin 3) | s = {0} ∨ s = {1} ∨ s = {0, 1}}

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetFurnitureUnits : DecidablePred fun (x : Finset (Fin 3)) => x ∈ furnitureUnits

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetFurnitureUnits s = decidable_of_iff (s = {0} ∨ s = {1} ∨ s = {0, 1}) ⋯

def SuttonFilip2021.piecePerspective : Set (Finset (Fin 3))

The piece perspective: count the table and the mirror.

Equations

• SuttonFilip2021.piecePerspective = {s : Finset (Fin 3) | s = {0} ∨ s = {1}}

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetPiecePerspective : DecidablePred fun (x : Finset (Fin 3)) => x ∈ piecePerspective

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetPiecePerspective s = decidable_of_iff (s = {0} ∨ s = {1}) ⋯

def SuttonFilip2021.vanityPerspective : Set (Finset (Fin 3))

The vanity perspective: count the composed unit.

Equations

• SuttonFilip2021.vanityPerspective = {s : Finset (Fin 3) | s = {0, 1}}

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetVanityPerspective : DecidablePred fun (x : Finset (Fin 3)) => x ∈ vanityPerspective

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetVanityPerspective s = decidable_of_iff (s = {0, 1}) ⋯

theorem SuttonFilip2021.furniture_units_overlap : Mereology.OverlapPred fovl furnitureUnits

𝒪(furniture) is overlapping: the vanity shares parts with the table. Hence furniture is [+O, −S]: object units exist (cardinality comparisons are licensed) but the null schema's base overlaps — mass.

theorem SuttonFilip2021.furniture_two_perspectives : Mereology.IsMaxDisjointIn fovl piecePerspective furnitureUnits ∧ Mereology.IsMaxDisjointIn fovl vanityPerspective furnitureUnits ∧ Mereology.OverlapPred fovl (Mereology.nullSchema fovl furnitureUnits)

The two individuation perspectives on the furniture units — count the pieces, or count the vanity — are both maximally disjoint, and differ; by overlapPred_nullSchema the null-schema counting base is overlapping, which is why #three furnitures fails.

def SuttonFilip2021.riceBaspred : Set (Finset (Fin 3))

Rice on a three-grain domain: the basic predicate contains the grains and their aggregates (its extension = unit ∨ collection, their (29)).

Equations

• SuttonFilip2021.riceBaspred = {s : Finset (Fin 3) | s.Nonempty}

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetRiceBaspred : DecidablePred fun (x : Finset (Fin 3)) => x ∈ riceBaspred

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetRiceBaspred s = SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetRiceBaspred._aux_1 s

def SuttonFilip2021.riceGrains : Set (Finset (Fin 3))

The grains of rice: the atoms.

Equations

• SuttonFilip2021.riceGrains = {s : Finset (Fin 3) | s = {0} ∨ s = {1} ∨ s = {2}}

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetRiceGrains : DecidablePred fun (x : Finset (Fin 3)) => x ∈ riceGrains

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetRiceGrains s = decidable_of_iff (s = {0} ∨ s = {1} ∨ s = {2}) ⋯

def SuttonFilip2021.heapPerspective : Set (Finset (Fin 3))

The heap perspective on rice: one three-grain aggregate.

Equations

• SuttonFilip2021.heapPerspective = {s : Finset (Fin 3) | s = {0, 1, 2}}

@[implicit_reducible]

instance SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetHeapPerspective : DecidablePred fun (x : Finset (Fin 3)) => x ∈ heapPerspective

Equations

• SuttonFilip2021.instDecidablePredFinsetFinOfNatNatMemSetHeapPerspective s = decidable_of_iff (s = {0, 1, 2}) ⋯

theorem SuttonFilip2021.rice_accessibility : riceGrains ⊆ riceBaspred ∧ Mereology.DisjointPred fovl riceGrains ∧ Mereology.OverlapPred fovl (Mereology.nullSchema fovl riceBaspred)

The accessibility puzzle, both halves ((Q2), §9.5.3): the grains are part of rice's basic predicate and are perfectly disjoint — they intuitively count as one — yet the [−O, −S] counting base (the null schema over the whole basic predicate) is overlapping, because grain and heap perspectives are both maximal. Grammatical counting is blocked: salience without accessibility.

Cross-linguistic variation as a schema substitution

Finnish huonekalut 'items of furniture' is the count counterpart of furniture: identical basic predicate, with the null schema replaced by a contextually specified one — ⟦huonekalut⟧^𝒮ᵢ = ⟦furniture⟧^{𝒮₀ ↦ 𝒮ᵢ} (their p. 278). On the model: each specific perspective on the furniture units is disjoint, hence countable. The same substitution relates Czech čočka to English lentil(s) among granulars.

theorem SuttonFilip2021.huonekalut_count : Mereology.DisjointPred fovl piecePerspective ∧ Mereology.DisjointPred fovl vanityPerspective

Each specific individuation perspective on the furniture units is a disjoint counting base — [+O, +S] is count (huonekalut), even though the [+O, −S] null-schema base overlaps (furniture).