Guerrini (2026): Distributive Kind Predication

Guerrini explains why generalizations with kind-denoting plurals, English bare plurals and Italian definite plurals, are distributed unlike singular indefinite generics: they can also be accidental, cumulative and near-universal in episodic sentences. Such a sentence is structurally ambiguous, (28). In the Bona Fide Generic parse the kind restricts a modalized universal Gen, as a singular indefinite does; in Distributive Kind Predication the predicate distributes over the kind's members at the evaluation world, as with a definite plural, so the generalization can be accidental. Which parses a nominal has follows from what it denotes, (10), and with the Nominal Mapping Parameter, (145), from the language and the noun's number.

Main definitions

• bonaFideGeneric, distributiveKindPred, cumulativeKindPred: the kind parses.
• cumulativeBelowGen: the rival with the cumulative operator below Gen, (74c).
• Parse.Available: the parses a nominal has.

Main results

• distributiveKindPred_of_bonaFideGeneric, not_bonaFideGeneric_of_exception: the generic parse entails distribution at the actual world and fails at an accessible exception, (53).
• forall_of_cumulativeBelowGen: the rival makes every member relate to every location, the reason the paper rejects it for elephants live in Africa and Asia.
• Parse.available_iff: the singular indefinite, whose kind formation is undefined, (16), has only Gen and the existential of Derived Property Predication.

Implementation notes

Gen is the paper's black box: a universal over the worlds an accessibility relation reaches and over the members of the kind there, so its law-likeness is a frame condition rather than a normality ordering. Kinds are represented by their sum at each world, a finite set of atoms, which is what DIST and the cumulative operator see. Homogeneity and its removal by all and always (section 3.3, Table 3), the subjunctive diagnostic (section 3.5), and the epistemic-adjective argument for a separate property parse (section 5.2.2) are recorded in the rows but not formalized, since they need a trivalent Gen and a mood licensing substrate.

References

• [Gue26]
• [Chi98]
• [BS00]

The two parses of a generalization, section 3.2

def Guerrini2026.bonaFideGeneric {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) (P : Atom → W → Prop) (w : W) : Prop

In the Bona Fide Generic parse (29) the kind restricts Gen, a universal over the worlds R accesses and the members of the kind there, so the kind's world variable stays bound.

Equations

• Guerrini2026.bonaFideGeneric R k P w = ModalLogic.Box R (fun (v : W) => ∀ a ∈ k v, P a v) w

@[reducible, inline]

abbrev Guerrini2026.distributiveKindPred {Atom : Type u_1} {W : Type u_2} (k : W → Finset Atom) (P : Atom → W → Prop) (w : W) : Prop

In Distributive Kind Predication (30) the kind is interpreted at the evaluation world and the predicate distributes over its members.

Equations

• Guerrini2026.distributiveKindPred k P w = ∀ a ∈ k w, P a w

theorem Guerrini2026.bonaFideGeneric_iff {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) (P : Atom → W → Prop) {w : W} : bonaFideGeneric R k P w ↔ ∀ (v : W), (w, v) ∈ R → distributiveKindPred k P v

The generic parse is Distributive Kind Predication at every accessible world (28).

theorem Guerrini2026.distributiveKindPred_of_bonaFideGeneric {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) (P : Atom → W → Prop) {w : W} [R.IsRefl] (h : bonaFideGeneric R k P w) : distributiveKindPred k P w

A law-like generalization holds of the actual members: under a reflexive accessibility the generic parse entails Distributive Kind Predication.

theorem Guerrini2026.not_bonaFideGeneric_of_exception {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) (P : Atom → W → Prop) {w v : W} (hv : (w, v) ∈ R) {a : Atom} (ha : a ∈ k v) (hp : ¬P a v) : ¬bonaFideGeneric R k P w

In the accidental case (53), distribution over the actual members says nothing about other worlds, so it survives an exception at an accessible world, which falsifies the generic parse.

def Guerrini2026.singularIndefiniteGeneric {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (P N : Atom → W → Prop) (w : W) : Prop

The singular indefinite generic, (19) and (31), is Gen over the noun's property.

Equations

• Guerrini2026.singularIndefiniteGeneric R P N w = ModalLogic.Box R (fun (v : W) => ∀ (a : Atom), N a v → P a v) w

theorem Guerrini2026.bonaFideGeneric_iff_singularIndefiniteGeneric {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) (P : Atom → W → Prop) {w : W} : bonaFideGeneric R k P w ↔ singularIndefiniteGeneric R P (fun (a : Atom) (v : W) => a ∈ k v) w

The generic parse of a kind-denoting plural is the singular indefinite generic over membership in the kind (28a), which is why the two have very similar meanings.

Cumulativity, section 4

@[reducible, inline]

abbrev Guerrini2026.cumulativeKindPred {Atom : Type u_1} {W : Type u_2} (k : W → Finset Atom) {Loc : Type u_3} (S : Atom → Loc → Prop) (locs : Finset Loc) (w : W) : Prop

Cumulative Kind Predication (74b) relates the kind's sum at the evaluation world to the locations by [BS00]'s cumulative operator.

Equations

• Guerrini2026.cumulativeKindPred k S locs w = Set.LiftRel S ↑(k w) ↑locs

def Guerrini2026.cumulativeBelowGen {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) {Loc : Type u_3} (S : Atom → Loc → Prop) (locs : Finset Loc) (w : W) : Prop

With the cumulative operator below Gen (74c), Gen ranges over the sub-pluralities of the kind, so every nonempty sample of the kind at every accessible world relates cumulatively to the locations.

Equations

• Guerrini2026.cumulativeBelowGen R k S locs w = ModalLogic.Box R (fun (v : W) => ∀ X ⊆ k v, X.Nonempty → Set.LiftRel S ↑X ↑locs) w

theorem Guerrini2026.forall_of_cumulativeBelowGen {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) {w : W} {Loc : Type u_3} (S : Atom → Loc → Prop) (locs : Finset Loc) [R.IsRefl] (h : cumulativeBelowGen R k S locs w) {a : Atom} (ha : a ∈ k w) {l : Loc} (hl : l ∈ locs) : S a l

(74c) is the strong reading. Taken at a singleton sample, it makes every member of the kind relate to every location, so it is false of elephants and Africa and Asia.

theorem Guerrini2026.cumulativeKindPred_of_cumulativeBelowGen {Atom : Type u_1} {W : Type u_2} (R : SetRel W W) (k : W → Finset Atom) {w : W} {Loc : Type u_3} (S : Atom → Loc → Prop) (locs : Finset Loc) [R.IsRefl] (hne : (k w).Nonempty) (h : cumulativeBelowGen R k S locs w) : cumulativeKindPred k S locs w

The strong reading entails Cumulative Kind Predication, the salient weak one.

Derived Property Predication, section 5.3

def Guerrini2026.dpp {Atom : Type u_1} {W : Type u_2} (P N : Atom → W → Prop) (w : W) : Prop

Derived Property Predication (105b) is the low-scoped existential over a property.

Equations

• Guerrini2026.dpp P N w = ∃ (a : Atom), N a w ∧ P a w

theorem Guerrini2026.dpp_of_distributiveKindPred {Atom : Type u_1} {W : Type u_2} (k : W → Finset Atom) (P : Atom → W → Prop) {w : W} (hne : (k w).Nonempty) (h : distributiveKindPred k P w) : dpp P (fun (a : Atom) (v : W) => a ∈ k v) w

The near-universal reading of an episodic bare plural is Distributive Kind Predication and the existential one Derived Property Predication over the same noun (105); the first entails the second once the kind has members.

Which parses a nominal has, sections 2 and 5.4

inductive Guerrini2026.Nominal : Type

The nominal expressions of (145) and (31).

• englishBarePlural : Nominal
• italianDefinitePlural : Nominal
• italianBarePlural : Nominal
• singularIndefinite : Nominal

@[instance_reducible]

instance Guerrini2026.instDecidableEqNominal : DecidableEq Nominal

Equations

• Guerrini2026.instDecidableEqNominal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Guerrini2026.Nominal.mapping : Nominal → Genericity.NominalMapping

Under [Chi98]'s Nominal Mapping Parameter (146), English nouns can be kinds or properties and Italian nouns are properties.

Equations

• Guerrini2026.Nominal.italianDefinitePlural.mapping = Genericity.NominalMapping.predOnly
• Guerrini2026.Nominal.italianBarePlural.mapping = Genericity.NominalMapping.predOnly
• x✝.mapping = Genericity.NominalMapping.argAndPred

def Guerrini2026.Nominal.definite : Nominal → Bool

A nominal is definite when it carries the definite article, Italian's kind-forming operator (13).

Equations

• Guerrini2026.Nominal.italianDefinitePlural.definite = true
• x✝.definite = false

def Guerrini2026.Nominal.number : Nominal → Number

The noun's number, which decides whether kind formation is defined for it (16).

Equations

• Guerrini2026.Nominal.singularIndefinite.number = Number.singular
• x✝.number = Number.plural

def Guerrini2026.Nominal.CanDenoteKind (n : Nominal) : Prop

The expression denotes a kind when the parameter or the article makes kind formation available and the noun is plural, (10a) and (16).

Equations

• n.CanDenoteKind = (n.mapping.CanDenoteKind (n.definite = true) ∧ n.number = Number.plural)

def Guerrini2026.Nominal.CanDenoteProperty (n : Nominal) : Prop

The expression denotes a property when the parameter allows it and no article has formed a kind (145).

Equations

• n.CanDenoteProperty = (n.mapping.CanDenoteProperty ∧ n.definite = false)

@[instance_reducible]

instance Guerrini2026.Nominal.instDecidablePredCanDenoteKind : DecidablePred CanDenoteKind

Equations

• n.instDecidablePredCanDenoteKind = id inferInstance

@[instance_reducible]

instance Guerrini2026.Nominal.instDecidablePredCanDenoteProperty : DecidablePred CanDenoteProperty

Equations

• n.instDecidablePredCanDenoteProperty = id inferInstance

inductive Guerrini2026.Parse : Type

The operator that takes the subject in (28), (74b), and (105).

• gen : Parse
• dist : Parse
• cumul : Parse
• dpp : Parse

@[instance_reducible]

instance Guerrini2026.instDecidableEqParse : DecidableEq Parse

Equations

• Guerrini2026.instDecidableEqParse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Guerrini2026.Parse.Available (n : Nominal) : Parse → Prop

DIST and the cumulative operator apply to a sum and so need a kind, the existential of Derived Property Predication needs a property, and Gen takes either (10).

Equations

• Guerrini2026.Parse.Available n Guerrini2026.Parse.gen = (n.CanDenoteKind ∨ n.CanDenoteProperty)
• Guerrini2026.Parse.Available n Guerrini2026.Parse.dist = n.CanDenoteKind
• Guerrini2026.Parse.Available n Guerrini2026.Parse.cumul = n.CanDenoteKind
• Guerrini2026.Parse.Available n Guerrini2026.Parse.dpp = n.CanDenoteProperty

@[instance_reducible]

instance Guerrini2026.instDecidablePredParseAvailable (n : Nominal) : DecidablePred (Parse.Available n)

Equations

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

theorem Guerrini2026.Parse.available_iff (p : Parse) : Available Nominal.englishBarePlural p ∧ (Available Nominal.italianDefinitePlural p ↔ p ≠ dpp) ∧ (Available Nominal.italianBarePlural p ↔ p = gen ∨ p = dpp) ∧ (Available Nominal.singularIndefinite p ↔ p = gen ∨ p = dpp)

By (145) and Tables 1 and 2, the English bare plural has all four parses, the Italian definite plural the three kind parses, and the Italian bare plural and the singular indefinite, which cannot denote a kind, only Gen and the existential, so no accidental or cumulative generalization.