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

Grimm and Dočekal account for the Czech morphology that counts aggregates, groups, and kinds. The suffix -í derives strongly non-countable nouns from countable roots, listí 'foliage' from list 'leaf', which take no plural, no cardinal, and no packaging (derived_aggregates_noncountable); the group numeral -ice yields a countable group, dvě trojice námořníků 'two groups of three sailors', whereas the aggregate numeral -oje and the taxonomic numeral -ojí yield phrases that no outer cardinal or universal quantifier can take (complex_numerals_uncounted); -oje selects nouns whose referents come in connected sets (aggregate_numeral_selects); and Czech nouns are inflexible, with no grinding and a taxonomic plural confined to non-episodic contexts where the taxonomic numeral is free (taxonomic_plural_nonepisodic). Section 5 extends Krifka's nominal semantics with Landman's groups for -ice and with Grimm's mereotopology for -í and -oje: a cluster is a sum of entities transitively connected through entities of their kind (Mereology.IsCluster), a maximal cluster absorbs every cluster it overlaps, -oje counts the maximal clusters below its argument, whose number is therefore determinate (ojeSem_determinate), and -ojí counts subkinds and so fails on a kind-less argument (oji_needs_subkinds).

Implementation notes

The connection relation is a parameter, the paper's proximate or external connectedness, which (63) binds existentially; the cluster of (61) uses a finite set of members and its supremum. The group numeral is stated over the library's Plurality.GroupStructure, whose up packs a sum into an atom, which is why a group can be counted again. The paper's Table 1, the twenty-two nouns derived by -í, is lexical data for the Czech Fragment and is not retyped here.

References

• [GD21]
• [Kri95a]
• [Lan89]
• [Gri12]
• [CV99]

TODO

Table 1's derived aggregates belong in Fragments/Slavic/Czech/; Krifka's kind and object unit operators of section 4 are not formalized.

The judged noun phrases, section 2

inductive GrimmDocekal2021.Noun : Type

A noun falls into one of these classes, which numerals and operations select.

• ordinary : Noun
• animate : Noun
• derivedAggregate : Noun

  The noun is derived by -í.

• pluraleTantum : Noun
• multiple : Noun

  The noun is countable, and its referents typically come in multiples, klíče 'keys'.

• substance : Noun
• abstract : Noun
• unique : Noun

  The phrase refers uniquely, noha tohoto stolu 'this table's leg'.

• proper : Noun

@[instance_reducible]

instance GrimmDocekal2021.instDecidableEqNoun : DecidableEq Noun

Equations

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

@[instance_reducible]

instance GrimmDocekal2021.instReprNoun : Repr Noun

Equations

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

def GrimmDocekal2021.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

inductive GrimmDocekal2021.Numeral : Type

A phrase carries one of these numerals, or none.

• none : Numeral
• simple : Numeral
• group : Numeral

  The group numeral is -ice.

• aggregate : Numeral

  The aggregate numerals are -oje and -ery.

• taxonomic : Numeral

  The taxonomic numerals are -ojí and -ero.

@[instance_reducible]

instance GrimmDocekal2021.instDecidableEqNumeral : DecidableEq Numeral

Equations

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

@[instance_reducible]

instance GrimmDocekal2021.instReprNumeral : Repr Numeral

Equations

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

def GrimmDocekal2021.instReprNumeral.repr : Numeral → ℕ → Std.Format

Equations

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

inductive GrimmDocekal2021.Operation : Type

A judged phrase tests one of these operations.

• none : Operation
• pluralization : Operation
• simpleCardinal : Operation
• vagueQuantifier : Operation

  The vague quantifier is mnohé 'many'.

• universal : Operation

  The universal quantifier is všechny 'all'.

• outerCardinal : Operation

  A simple cardinal applies over a complex numeral.

• packaging : Operation
• grinding : Operation
• derivation : Operation

  An aggregate is derived with -í.

@[instance_reducible]

instance GrimmDocekal2021.instDecidableEqOperation : DecidableEq Operation

Equations

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

@[instance_reducible]

instance GrimmDocekal2021.instReprOperation : Repr Operation

Equations

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

def GrimmDocekal2021.instReprOperation.repr : Operation → ℕ → Std.Format

Equations

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

inductive GrimmDocekal2021.Context : Type

A reading is judged in one of these contexts.

• episodic : Context
• generic : Context
• portion : Context

  The context is a fast-food order, section 2.2.2.

@[instance_reducible]

instance GrimmDocekal2021.instDecidableEqContext : DecidableEq Context

Equations

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

@[instance_reducible]

instance GrimmDocekal2021.instReprContext : Repr Context

Equations

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

def GrimmDocekal2021.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

structure GrimmDocekal2021.Row : Type

A row records a noun phrase and its judgment.

• noun : Noun
• numeral : Numeral
• operation : Operation
• context : Option Context
• taxonomic : Bool
• judgment : Judgment

@[instance_reducible]

instance GrimmDocekal2021.instDecidableEqRow : DecidableEq Row

Equations

• GrimmDocekal2021.instDecidableEqRow = GrimmDocekal2021.instDecidableEqRow.decEq

def GrimmDocekal2021.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def GrimmDocekal2021.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GrimmDocekal2021.instReprRow : Repr Row

Equations

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

def GrimmDocekal2021.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def GrimmDocekal2021.rows : List Row

The rows are the judged phrases of sections 2, 4, and 5.

Equations

• GrimmDocekal2021.rows = List.filterMap GrimmDocekal2021.Row.ofDatum GrimmDocekal2021.Examples.all

theorem GrimmDocekal2021.derived_aggregates_noncountable (r : Row) : r ∈ rows → r.noun = Noun.derivedAggregate → r.numeral ≠ Numeral.aggregate → r.operation ≠ Operation.none → r.judgment ≠ Judgment.acceptable

Nouns derived by -í take neither plural, nor simple cardinal, nor a vague quantifier, nor a packaging reading, (9) to (12).

theorem GrimmDocekal2021.derivation_restricted (r : Row) : r ∈ rows → r.operation = Operation.derivation → r.judgment = Judgment.ungrammatical

-í does not apply to an arbitrary countable noun, (13).

theorem GrimmDocekal2021.group_numeral_countable : (∃ r ∈ rows, r.numeral = Numeral.group ∧ r.operation = Operation.outerCardinal ∧ r.judgment = Judgment.acceptable) ∧ (∃ r ∈ rows, r.numeral = Numeral.group ∧ r.operation = Operation.vagueQuantifier ∧ r.judgment = Judgment.acceptable) ∧ ∀ r ∈ rows, r.numeral = Numeral.group → r.operation = Operation.universal → r.judgment ≠ Judgment.acceptable

A group numeral phrase is counted again and quantified by mnohé, (17) and (18), but not by všechna, (19).

theorem GrimmDocekal2021.complex_numerals_uncounted (r : Row) : r ∈ rows → r.numeral = Numeral.aggregate ∨ r.numeral = Numeral.taxonomic → r.operation = Operation.outerCardinal ∨ r.operation = Operation.universal → r.judgment ≠ Judgment.acceptable

Aggregate and taxonomic numeral phrases take no outer cardinal and no universal quantifier, (26), (27), (32), (33).

theorem GrimmDocekal2021.aggregate_numeral_selects : (∀ r ∈ rows, r.numeral = Numeral.aggregate → r.operation = Operation.none → r.noun = Noun.derivedAggregate ∨ r.noun = Noun.pluraleTantum ∨ r.noun = Noun.multiple → r.judgment = Judgment.acceptable) ∧ ∀ r ∈ rows, r.numeral = Numeral.aggregate → r.noun = Noun.ordinary → r.judgment ≠ Judgment.acceptable

-oje takes nouns derived by -í, pluralia tantum, and nouns of entities that come in multiples, (20) to (24), and rejects ordinary countable nouns, (25) and (68).

theorem GrimmDocekal2021.taxonomic_plural_nonepisodic : (∀ r ∈ rows, r.operation = Operation.grinding → r.judgment ≠ Judgment.acceptable) ∧ (∀ r ∈ rows, r.taxonomic = true → r.numeral ≠ Numeral.taxonomic → (r.judgment = Judgment.acceptable ↔ r.context = some Context.generic)) ∧ ∀ r ∈ rows, r.taxonomic = true → r.numeral = Numeral.taxonomic → r.judgment = Judgment.acceptable

In section 2.3, grinding is rejected, (34) and (35); the taxonomic reading of a plural or a simple cardinal phrase needs a non-episodic context, (36) to (40), while the taxonomic numeral is free in both.

theorem GrimmDocekal2021.taxonomic_needs_kind (r : Row) : r ∈ rows → r.numeral = Numeral.taxonomic → r.noun = Noun.unique ∨ r.noun = Noun.proper → r.judgment ≠ Judgment.acceptable

The taxonomic numeral fails on a uniquely referring or proper argument, (52).

The three numerals, sections 4.2 and 5

The aggregate numeral counts clusters, section 5.2. Connection is reflexive and symmetric ((56), (57)) and whatever is connected to a part is connected to the whole (58): the axioms of Mereology.IsConnection, from which overlap entails connection ((59), Mereology.IsConnection.of_overlap). A cluster ((60), (61)) is Mereology.IsCluster, the sum of entities of a property any two of which are transitively connected through such entities. Inside a connected component clusters are cumulative (Mereology.cum_isClusterIn), the cumulativity of -í nouns, listí and listí making listí; a maximal cluster absorbs every cluster it overlaps (63), so two maximal clusters do not overlap (Mereology.disjointPred_isMaxCluster), the paper's remark after (63).

def GrimmDocekal2021.iceSem {α : Type u_1} [SemilatticeSup α] (G : Plurality.GroupStructure α) (n : ℕ) (P : α → ℕ → Prop) (x : α) : Prop

The group numeral (55) packs a sum of n members of P into a group atom.

Equations

• GrimmDocekal2021.iceSem G n P x = ∃ (y : α), x = G.up y ∧ P y n

theorem GrimmDocekal2021.iceSem_atom {α : Type u_1} [SemilatticeSup α] {G : Plurality.GroupStructure α} {n : ℕ} {P : α → ℕ → Prop} {x : α} (h : iceSem G n P x) : Mereology.Atom x

A group numeral phrase denotes an atom, which is why it is counted again, (17) and (54).

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

By (64), n-oje P holds of a P-entity x when the maximal P-clusters properly below x number n.

Equations

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

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

The cardinality an aggregate numeral asserts is determinate, the witnessing set being the maximal clusters below the argument, so no outer cardinal can re-specify it, (27) and (26).

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

By (50), over a subkind relation T, n-ojí k holds of a set of 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

A kind-less argument defeats the taxonomic numeral (52), since a proper name has no subkinds.

Three leaves in a row

The leaves of listí need only be proximately connected, section 5.2.1. Three leaves lie in a row, each near its neighbours: the outer two are not near each other, yet their sum is a cluster, since they are transitively connected through the middle leaf, which (61) lets lie outside the cluster. Without the middle leaf the outer two form no cluster.

@[reducible, inline]

abbrev GrimmDocekal2021.LeafSum : Type

Leaf sums are the sets of three leaves in a row.

Equations

• GrimmDocekal2021.LeafSum = Finset (Fin 3)

def GrimmDocekal2021.Near (s t : LeafSum) : Prop

Two sums are near when they contain the same or neighbouring leaves.

Equations

• GrimmDocekal2021.Near s t = ∃ i ∈ s, ∃ j ∈ t, ↑i ≤ ↑j + 1 ∧ ↑j ≤ ↑i + 1

@[instance_reducible]

instance GrimmDocekal2021.instDecidableRelLeafSumNear : DecidableRel Near

Equations

• GrimmDocekal2021.instDecidableRelLeafSumNear s t = id inferInstance

def GrimmDocekal2021.Leaf (s : LeafSum) : Prop

A leaf sum is a single leaf when it has one member.

Equations

• GrimmDocekal2021.Leaf s = (Finset.card s = 1)

@[instance_reducible]

instance GrimmDocekal2021.instDecidablePredLeafSumLeaf : DecidablePred Leaf

Equations

• GrimmDocekal2021.instDecidablePredLeafSumLeaf s = id inferInstance

def GrimmDocekal2021.OuterLeaf (s : LeafSum) : Prop

The outer leaves are the leaves other than the middle one.

Equations

• GrimmDocekal2021.OuterLeaf s = (s = {0} ∨ s = {2})

@[instance_reducible]

instance GrimmDocekal2021.instDecidablePredLeafSumOuterLeaf : DecidablePred OuterLeaf

Equations

• GrimmDocekal2021.instDecidablePredLeafSumOuterLeaf s = id inferInstance