Sutton and Filip (2021): The Count/Mass Distinction for Granular Nouns

Sutton and Filip account for the lexical count/mass distinction and answer the accessibility puzzle: rice denotes stuff made of perceptually salient grains, yet three rices cannot mean three grains of rice. A lexical entry is tripartite, (33): a basic predicate, a counting base built from it by the object identifying function and an individuation schema, and an extension that is the counting base or its closure under sum. Grammatical counting is defined over disjoint counting bases only, (A1), so an entry is count exactly when its counting base is disjoint. The grains of rice are in its basic predicate and not in its counting base, which overlaps; lentil, over a frame of the same kind, counts its units.

Main definitions

• Frame, Frame.objects: a basic predicate with its unit field, (28) to (30).
• Entry, Entry.cbase, Entry.extn: a lexical entry with its counting base and extension.
• Entry.IsCount: an entry is count when its counting base is disjoint.
• unitShift, containerExtn: the unit extracting and container classifiers.

Main results

• Entry.isCount_of_perspective, Entry.isCount_iff_of_null: every [+S] entry is count, and a [−S] entry is count exactly when the predicate its schema applies to is disjoint.
• rice_mass, lentil_count: a [−O,−S] granular is mass and a [+O,+S] one is count.
• isCount_unitShift: grain of, (49) and (50), makes every entry count.
• cum_extn_of_sumClosed, not_cum_extn_of_singular: a container classifier's argument, (45), can be sum-closed but not singular count.
• furniture_two_perspectives, rice_accessibility: the two halves of the puzzle on a model.
• isCount_iff_english: the categorization agrees with the English lexicon, where a numeral counts lentil and neither furniture nor rice.

Implementation notes

A specific schema is a function from predicates to perspectives in the paper; an entry here records the perspective the schema of utterance selects on the predicate it applies to, with its maximality, since only that value enters the counting base. Overlap is the substrate's Mereology.Overlap, a shared non-null part. The cardinality comparisons licensed by [+O], the perceptual content of frames, the composition with verbs of Appendix B, and the notional classes of Table 9.1 are not formalized.

References

• [SF21]
• [Lan11]
• [Lan16]
• [Kri89]

structure SuttonFilip2021.Frame (α : Type u_2) : Type u_2

A basic predicate frame (28)–(29): its extension and, when the concept has perceptually or functionally identified units, its unit field.

• extn : Set α
• unit : Option (Set α)

def SuttonFilip2021.Frame.objects {α : Type u_1} (F : Frame α) : Set α

The object identifying function (30): the unit field where there is one, the predicate itself otherwise.

Equations

• F.objects = F.unit.getD F.extn

def SuttonFilip2021.Frame.substance {α : Type u_1} (stuff : Set α) : Frame α

A substance frame has no unit field.

Equations

• SuttonFilip2021.Frame.substance stuff = { extn := stuff, unit := none }

@[simp]

theorem SuttonFilip2021.Frame.objects_substance {α : Type u_1} (stuff : Set α) : (substance stuff).objects = stuff

def SuttonFilip2021.Frame.ofUnits {α : Type u_1} [SemilatticeSup α] (units : Set α) : Frame α

A frame whose extension is its units and their sums, the unit and collection fields of (28)–(29): granular for disjoint units, a collective artifact for overlapping ones.

Equations

• SuttonFilip2021.Frame.ofUnits units = { extn := {x : α | Mereology.AlgClosure (fun (x : α) => x ∈ units) x}, unit := some units }

@[simp]

theorem SuttonFilip2021.Frame.objects_ofUnits {α : Type u_1} [SemilatticeSup α] (units : Set α) : (ofUnits units).objects = units

structure SuttonFilip2021.Entry (α : Type u_2) [SemilatticeSup α] : Type u_2

A lexical entry (33): the basic predicate; whether the counting base applies the object identifying function, [±O]; whether the extension is closed under sum, the (*) of (33); and the perspective the schema of utterance selects, [+S], or none for the null schema, [−S].

• frame : Frame α
• objectFn : Bool
• sumClosed : Bool
• perspective : Option (Set α)
• perspective_max (D : Set α) : self.perspective = some D → Mereology.IsMaxDisjointIn Mereology.Overlap D (if self.objectFn = true then self.frame.objects else self.frame.extn)

def SuttonFilip2021.Entry.base {α : Type u_1} [SemilatticeSup α] (E : Entry α) : Set α

The predicate the schema applies to is the objects under [+O] and the basic predicate under [−O].

Equations

• E.base = if E.objectFn = true then E.frame.objects else E.frame.extn

def SuttonFilip2021.Entry.cbase {α : Type u_1} [SemilatticeSup α] (E : Entry α) : Set α

The counting base is the perspective under a specific schema, the null schema otherwise.

Equations

• E.cbase = E.perspective.getD (Mereology.nullSchema Mereology.Overlap E.base)

def SuttonFilip2021.Entry.extn {α : Type u_1} [SemilatticeSup α] (E : Entry α) : Set α

The extension is the counting base, closed under sum when the entry is.

Equations

• E.extn = if E.sumClosed = true then {x : α | Mereology.AlgClosure (fun (x : α) => x ∈ E.cbase) x} else E.cbase

def SuttonFilip2021.Entry.IsCount {α : Type u_1} [SemilatticeSup α] (E : Entry α) : Prop

Grammatical counting (A1) is defined over disjoint counting bases only: an entry is count when its base is disjoint.

Equations

• E.IsCount = Mereology.DisjointPred Mereology.Overlap E.cbase

def SuttonFilip2021.Entry.features {α : Type u_1} [SemilatticeSup α] (E : Entry α) : Bool × Bool

The features [±O] and [±S].

Equations

• E.features = (E.objectFn, E.perspective.isSome)

theorem SuttonFilip2021.Entry.isCount_of_perspective {α : Type u_1} [SemilatticeSup α] {E : Entry α} {D : Set α} (h : E.perspective = some D) : E.IsCount

A [+S] entry is count: its perspective is disjoint.

theorem SuttonFilip2021.Entry.cbase_of_null {α : Type u_1} [SemilatticeSup α] {E : Entry α} (h : E.perspective = none) : E.cbase = E.base

Under the null schema the counting base is the predicate the schema applies to.

theorem SuttonFilip2021.Entry.isCount_iff_of_null {α : Type u_1} [SemilatticeSup α] {E : Entry α} (h : E.perspective = none) : E.IsCount ↔ Mereology.DisjointPred Mereology.Overlap E.base

A [−S] entry is count exactly when the predicate its schema applies to is disjoint.

def SuttonFilip2021.Entry.withPerspective {α : Type u_1} [SemilatticeSup α] (E : Entry α) (D : Set α) (h : Mereology.IsMaxDisjointIn Mereology.Overlap D E.base) : Entry α

The substitution of the null schema by the schema of utterance, ⟦furniture⟧^{𝒮₀ ↦ 𝒮ᵢ}.

Equations

• E.withPerspective D h = { frame := E.frame, objectFn := E.objectFn, sumClosed := E.sumClosed, perspective := some D, perspective_max := ⋯ }

theorem SuttonFilip2021.Entry.withPerspective_isCount {α : Type u_1} [SemilatticeSup α] (E : Entry α) (D : Set α) (h : Mereology.IsMaxDisjointIn Mereology.Overlap D E.base) : (E.withPerspective D h).IsCount

Unit extracting and container classifiers

def SuttonFilip2021.unitShift {α : Type u_1} [SemilatticeSup α] (E : Entry α) (D : Set α) (h : Mereology.IsMaxDisjointIn Mereology.Overlap D E.frame.objects) : Entry α

The unit extracting classifier (49): the object identifying function and the schema of utterance inserted into the counting base of any entry, the extension closed under sum.

Equations

• SuttonFilip2021.unitShift E D h = { frame := E.frame, objectFn := true, sumClosed := true, perspective := some D, perspective_max := ⋯ }

theorem SuttonFilip2021.features_unitShift {α : Type u_1} [SemilatticeSup α] (E : Entry α) (D : Set α) (h : Mereology.IsMaxDisjointIn Mereology.Overlap D E.frame.objects) : (unitShift E D h).features = (true, true)

The unit shift is the generalized [−O,−S] to [+O,+S] shift (9.5.4).

theorem SuttonFilip2021.isCount_unitShift {α : Type u_1} [SemilatticeSup α] (E : Entry α) (D : Set α) (h : Mereology.IsMaxDisjointIn Mereology.Overlap D E.frame.objects) : (unitShift E D h).IsCount

The unit shift makes every entry count.

def SuttonFilip2021.containerExtn {α : Type u_1} [SemilatticeSup α] (R P : Entry α) (contain : α → α → Prop) : Set α

The extension of the container reading (44): sums of counted receptacles, each of which contains something in the argument's extension; counting proceeds by the receptacle's counting base, which the argument does not touch.

Equations

• SuttonFilip2021.containerExtn R P contain = {x : α | Mereology.AlgClosure (fun (x : α) => x ∈ R.cbase) x ∧ ∀ z ∈ R.cbase, z ≤ x → ∃ v ∈ P.extn, contain z v}

theorem SuttonFilip2021.cum_extn_of_sumClosed {α : Type u_1} [SemilatticeSup α] {E : Entry α} (h : E.sumClosed = true) : Mereology.CUM fun (x : α) => x ∈ E.extn

The container classifier presupposes, (45), that the argument's extension is cumulative, which every sum-closed extension is.

theorem SuttonFilip2021.not_cum_extn_of_singular {α : Type u_1} [SemilatticeSup α] {E : Entry α} (hs : E.sumClosed = false) (hc : E.IsCount) {u v : α} (hu : u ∈ E.cbase) (hv : v ∈ E.cbase) (hne : u ≠ v) (hu0 : ¬IsBot u) (hv0 : ¬IsBot v) : ¬Mereology.CUM fun (x : α) => x ∈ E.extn

A singular count extension with two distinct units is not cumulative: the sum of two units is not a unit, so #a bowl of an apple.

Granular frames

theorem SuttonFilip2021.overlapPred_extn_ofUnits {α : Type u_1} [SemilatticeSup α] {units : Set α} {u v : α} (hu : u ∈ units) (hv : v ∈ units) (hne : u ≠ v) (hu0 : ¬IsBot u) (hv0 : ¬IsBot v) : Mereology.OverlapPred Mereology.Overlap (Frame.ofUnits units).extn

A frame of units and their sums overlaps as soon as it has two distinct non-null units: a unit and its sum with another share the unit.

theorem SuttonFilip2021.rice_mass {α : Type u_1} [SemilatticeSup α] {units : Set α} {u v : α} (hu : u ∈ units) (hv : v ∈ units) (hne : u ≠ v) (hu0 : ¬IsBot u) (hv0 : ¬IsBot v) (E : Entry α) (hF : E.frame = Frame.ofUnits units) (hO : E.objectFn = false) (hS : E.perspective = none) : ¬E.IsCount

A [−O,−S] entry over a frame of units and their sums with two distinct non-null units is mass: the grains of rice and čočka are in the basic predicate, not in the counting base.

def SuttonFilip2021.lentil {α : Type u_1} [SemilatticeSup α] (units : Set α) (hd : Mereology.DisjointPred Mereology.Overlap units) (sumClosed : Bool) : Entry α

The [+O,+S] entry over a frame of disjoint units, lentil (36)–(37): the perspective is the units themselves.

Equations

• SuttonFilip2021.lentil units hd sumClosed = { frame := SuttonFilip2021.Frame.ofUnits units, objectFn := true, sumClosed := sumClosed, perspective := some units, perspective_max := ⋯ }

theorem SuttonFilip2021.lentil_count {α : Type u_1} [SemilatticeSup α] {units : Set α} (hd : Mereology.DisjointPred Mereology.Overlap units) (sumClosed : Bool) : (lentil units hd sumClosed).IsCount ∧ (lentil units hd sumClosed).cbase = units

lentil is count, with the units as its counting base.

Furniture and rice on three atoms

@[reducible, inline]

abbrev SuttonFilip2021.Part : Type

Parts are subsets of three atoms; overlap is a shared non-empty part.

Equations

• SuttonFilip2021.Part = Finset (Fin 3)

@[instance_reducible]

instance SuttonFilip2021.instDecidableRelPartOverlap : DecidableRel Mereology.Overlap

Equations

• SuttonFilip2021.instDecidableRelPartOverlap s t = decidable_of_iff (¬Disjoint s t) ⋯

@[instance_reducible]

instance SuttonFilip2021.instDecidablePredPartMemSetInsert {a : Part} {P : Set Part} [DecidablePred fun (x : Part) => x ∈ P] : DecidablePred fun (x : Part) => x ∈ insert a P

Equations

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

@[instance_reducible]

instance SuttonFilip2021.instDecidableOverlapPredPartOverlap {P : Set Part} [DecidablePred fun (x : Part) => x ∈ P] : Decidable (Mereology.OverlapPred Mereology.Overlap P)

Equations

• SuttonFilip2021.instDecidableOverlapPredPartOverlap = id inferInstance

@[instance_reducible]

instance SuttonFilip2021.instDecidableDisjointPredPartOverlap {P : Set Part} [DecidablePred fun (x : Part) => x ∈ P] : Decidable (Mereology.DisjointPred Mereology.Overlap P)

Equations

• SuttonFilip2021.instDecidableDisjointPredPartOverlap = decidable_of_iff (¬Mereology.OverlapPred Mereology.Overlap P) ⋯

@[instance_reducible]

instance SuttonFilip2021.instDecidableLeSetPartOfDecidablePredMem {P Q : Set Part} [DecidablePred fun (x : Part) => x ∈ P] [DecidablePred fun (x : Part) => x ∈ Q] : Decidable (P ⊆ Q)

Equations

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

@[instance_reducible]

instance SuttonFilip2021.instDecidableIsMaxDisjointInPartOverlap {D P : Set Part} [DecidablePred fun (x : Part) => x ∈ D] [DecidablePred fun (x : Part) => x ∈ P] : Decidable (Mereology.IsMaxDisjointIn Mereology.Overlap D P)

Equations

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

def SuttonFilip2021.furnitureUnits : Set Part

The functional units of furniture: a table, a mirror, and the vanity they compose.

Equations

• SuttonFilip2021.furnitureUnits = {s : SuttonFilip2021.Part | s = {0} ∨ s = {1} ∨ s = {0, 1}}

@[instance_reducible]

instance SuttonFilip2021.instDecidablePredPartMemSetFurnitureUnits : DecidablePred fun (x : Part) => x ∈ furnitureUnits

Equations

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

def SuttonFilip2021.piecePerspective : Set Part

The piece perspective counts the table and the mirror.

Equations

• SuttonFilip2021.piecePerspective = {s : SuttonFilip2021.Part | s = {0} ∨ s = {1}}

@[instance_reducible]

instance SuttonFilip2021.instDecidablePredPartMemSetPiecePerspective : DecidablePred fun (x : Part) => x ∈ piecePerspective

Equations

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

def SuttonFilip2021.vanityPerspective : Set Part

The vanity perspective counts the composed unit.

Equations

• SuttonFilip2021.vanityPerspective = {s : SuttonFilip2021.Part | s = {0, 1}}

@[instance_reducible]

instance SuttonFilip2021.instDecidablePredPartMemSetVanityPerspective : DecidablePred fun (x : Part) => x ∈ vanityPerspective

Equations

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

def SuttonFilip2021.furniture : Entry Part

furniture (40): [+O,−S] over the functional units and their sums.

Equations

• SuttonFilip2021.furniture = { frame := SuttonFilip2021.Frame.ofUnits SuttonFilip2021.furnitureUnits, objectFn := true, sumClosed := true, perspective := none, perspective_max := ⋯ }

theorem SuttonFilip2021.furniture_mass : ¬furniture.IsCount

The functional units overlap, so furniture is mass although its units are identified.

theorem SuttonFilip2021.furniture_two_perspectives : Mereology.IsMaxDisjointIn Mereology.Overlap piecePerspective furnitureUnits ∧ Mereology.IsMaxDisjointIn Mereology.Overlap vanityPerspective furnitureUnits ∧ piecePerspective ≠ vanityPerspective ∧ Mereology.OverlapPred Mereology.Overlap furniture.cbase

Two perspectives on the furniture units, the pieces and the vanity, are both maximal and differ, which is why the null schema's base overlaps.

def SuttonFilip2021.huonekalut : Entry Part

huonekalut (41): furniture with the null schema replaced by the piece perspective, and count.

Equations

• SuttonFilip2021.huonekalut = SuttonFilip2021.furniture.withPerspective SuttonFilip2021.piecePerspective SuttonFilip2021.huonekalut._proof_1

theorem SuttonFilip2021.huonekalut_count : huonekalut.IsCount

def SuttonFilip2021.riceGrains : Set Part

The grains of rice: the atoms.

Equations

• SuttonFilip2021.riceGrains = {s : SuttonFilip2021.Part | s = {0} ∨ s = {1} ∨ s = {2}}

@[instance_reducible]

instance SuttonFilip2021.instDecidablePredPartMemSetRiceGrains : DecidablePred fun (x : Part) => x ∈ riceGrains

Equations

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

def SuttonFilip2021.rice : Entry Part

rice (38): [−O,−S] over the grains and their sums.

Equations

• SuttonFilip2021.rice = { frame := SuttonFilip2021.Frame.ofUnits SuttonFilip2021.riceGrains, objectFn := false, sumClosed := true, perspective := none, perspective_max := ⋯ }

theorem SuttonFilip2021.riceGrains_disjoint : Mereology.DisjointPred Mereology.Overlap riceGrains

theorem SuttonFilip2021.rice_accessibility : riceGrains ⊆ rice.frame.extn ∧ ¬rice.IsCount ∧ unitShift rice riceGrains ⋯ = lentil riceGrains riceGrains_disjoint true ∧ (lentil riceGrains riceGrains_disjoint true).IsCount ∧ (lentil riceGrains riceGrains_disjoint true).cbase = riceGrains

The accessibility puzzle, both halves ((Q2), 9.5.3): the grains are disjoint and in the basic predicate, yet rice is mass; grains of rice (50) is the lentil entry over the same frame, count with the grains as its counting base.

def SuttonFilip2021.mud : Entry Part

mud (39): [−O,−S] over the parts of some mud, which overlap.

Equations

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

theorem SuttonFilip2021.mud_mass : ¬mud.IsCount

theorem SuttonFilip2021.isCount_iff_english : (furniture.IsCount ↔ English.Nouns.furniture.IsCount) ∧ (rice.IsCount ↔ English.Nouns.rice.IsCount) ∧ ((lentil riceGrains riceGrains_disjoint true).IsCount ↔ English.Nouns.lentil.IsCount)

The categorization agrees with the English lexicon: a numeral counts lentil and neither furniture nor rice.