[Gue26]: Distributive kind predication

Janek Guerrini, "Distributive kind predication", Natural Language Semantics 34:85–136 (2026).

Thesis

Generalizations with kind-denoting plurals (English bare plurals, Italian definite plurals) are structurally ambiguous — not because Gen has a complex semantics, but because the kind-denoting plural licenses parses with no Gen at all: Bona Fide Generic (BFG: kind restricts Gen, law-like), and the Gen-free Distributive Kind Predication (DKP: DIST over the kind at s₀, accidental), Cumulative Kind Predication (CKP: **, §4), and Derived Property Predication (DPP: property → low-scoped ∃, §5.3). Singular indefinites cannot denote kinds (∩ undefined for singular count nouns), so DKP/CKP never apply and they are limited to BFG, explaining their narrower distribution (Table 1).

This file derives the LF typology from the shared Chierchia kind-denotation primitive ([Chi98]), states the prevalence bridge to [TG19], and contrasts the non-quantificational DKP/CKP analyses with the quantificational rivals [Coh99] and [Nic09]. Empirical stimuli are typed rows in Data/Examples/Guerrini2026.json (Examples.all).

The four LF parses

inductive Guerrini2026.GeneralizationLF : Type

The four LF parses of a sentence with a kind-denoting plural (diagram (145)). The first three require kind denotation; the fourth requires property denotation. Singular indefinites access only bonaFideGeneric.

• bonaFideGeneric : GeneralizationLF
• distributiveKindPred : GeneralizationLF
• cumulativeKindPred : GeneralizationLF
• existentialDPP : GeneralizationLF

@[implicit_reducible]

instance Guerrini2026.instDecidableEqGeneralizationLF : DecidableEq GeneralizationLF

Equations

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

def Guerrini2026.instReprGeneralizationLF.repr : GeneralizationLF → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprGeneralizationLF : Repr GeneralizationLF

Equations

• Guerrini2026.instReprGeneralizationLF = { reprPrec := Guerrini2026.instReprGeneralizationLF.repr }

def Guerrini2026.lfFlavor : GeneralizationLF → Bool

BFG is law-like (modal Gen); the three Gen-free parses are accidental (DPP, an existential episodic reading, is not a generalization but groups with the non-generic parses here).

Equations

• Guerrini2026.lfFlavor Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.lfFlavor x✝ = false

def Guerrini2026.involvesGen : GeneralizationLF → Bool

Whether a parse involves the silent quantificational adverb Gen. Only BFG does, so only BFG supports Quantificational Variability Effects and is subject to [TG19]'s prevalence inference.

Equations

• Guerrini2026.involvesGen Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.involvesGen x✝ = false

theorem Guerrini2026.only_bfg_involves_gen (lf : GeneralizationLF) : involvesGen lf = true ↔ lf = GeneralizationLF.bonaFideGeneric

Only the Bona Fide Generic parse involves Gen, hence QVEs and threshold inference (examples (8), (90), (92)).

The named operators (foundational by construction)

DKP is DIST over the kind extension; CKP is the cumulative operator **. Both are the theory-layer operators under the paper's names, so theorems about them are theorems about distMaximal / Cumulative.

@[reducible, inline]

abbrev Guerrini2026.distributiveKindPred {Atom W : Type} (kindExt : W → Finset Atom) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (s₀ : W) : Prop

Distributive Kind Predication: distribute P over the kind's extension at s₀ (structure (30): ∀y(y ≤ ∩lions_{s₀}) → ⟦hunt⟧_{s₀}(y)).

Equations

• Guerrini2026.distributiveKindPred kindExt P s₀ = Semantics.Plurality.distMaximal P (kindExt s₀) s₀

@[reducible, inline]

abbrev Guerrini2026.cumulativeKindPred {Atom Loc : Type} (R : Atom → Loc → Prop) (kindExt : Finset Atom) (locations : Finset Loc) : Prop

Cumulative Kind Predication: the cumulative operator ** relates the kind extension to a set of locations (§4, structure (62)).

Equations

• Guerrini2026.cumulativeKindPred R kindExt locations = Semantics.Plurality.Cumulativity.Cumulative R kindExt locations

Nominal Mapping and denotation (diagram (145), §5.3)

inductive Guerrini2026.NominalExpression : Type

Cross-linguistic nominal forms.

• englishBarePlural : NominalExpression
• italianDefinitePlural : NominalExpression
• italianBarePlural : NominalExpression

@[implicit_reducible]

instance Guerrini2026.instDecidableEqNominalExpression : DecidableEq NominalExpression

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprNominalExpression : Repr NominalExpression

Equations

• Guerrini2026.instReprNominalExpression = { reprPrec := Guerrini2026.instReprNominalExpression.repr }

def Guerrini2026.instReprNominalExpression.repr : NominalExpression → ℕ → Std.Format

Equations

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

def Guerrini2026.nominalMapping : NominalExpression → Semantics.Kinds.NMP.NominalMapping

The Nominal Mapping Parameter ([Chi98]) per nominal form.

Equations

• Guerrini2026.nominalMapping Guerrini2026.NominalExpression.englishBarePlural = Semantics.Kinds.NMP.NominalMapping.argAndPred
• Guerrini2026.nominalMapping Guerrini2026.NominalExpression.italianDefinitePlural = Semantics.Kinds.NMP.NominalMapping.predOnly
• Guerrini2026.nominalMapping Guerrini2026.NominalExpression.italianBarePlural = Semantics.Kinds.NMP.NominalMapping.predOnly

def Guerrini2026.HasD : NominalExpression → Prop

Whether an overt determiner D is present (Italian definite plural alone).

Equations

• Guerrini2026.HasD Guerrini2026.NominalExpression.italianDefinitePlural = True
• Guerrini2026.HasD x✝ = False

@[implicit_reducible]

instance Guerrini2026.instDecidablePredNominalExpressionHasD : DecidablePred HasD

Equations

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

def Guerrini2026.CanDenote (ne : NominalExpression) : Semantics.Kinds.NMP.NominalDenotation → Prop

Available denotations per nominal form. Kind denotation from CanDenoteKind; property denotation from the parameter + D-status (predOnly + D maps to a kind, blocking the property reading).

Equations

• One or more equations did not get rendered due to their size.
• Guerrini2026.CanDenote ne Semantics.Kinds.NMP.NominalDenotation.kind = Semantics.Kinds.NMP.CanDenoteKind (Guerrini2026.nominalMapping ne) (Guerrini2026.HasD ne)

@[implicit_reducible]

instance Guerrini2026.instDecidableCanDenote (ne : NominalExpression) (nd : Semantics.Kinds.NMP.NominalDenotation) : Decidable (CanDenote ne nd)

Equations

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

def Guerrini2026.LFAvailable (ne : NominalExpression) : GeneralizationLF → Prop

Kind denotation enables DKP and CKP; property denotation enables DPP; BFG is always available (kind or property can restrict Gen). Diagram (145).

Equations

• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.bonaFideGeneric = True
• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.distributiveKindPred = Guerrini2026.CanDenote ne Semantics.Kinds.NMP.NominalDenotation.kind
• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.cumulativeKindPred = Guerrini2026.CanDenote ne Semantics.Kinds.NMP.NominalDenotation.kind
• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.existentialDPP = Guerrini2026.CanDenote ne Semantics.Kinds.NMP.NominalDenotation.property

@[implicit_reducible]

instance Guerrini2026.instDecidableLFAvailable (ne : NominalExpression) (lf : GeneralizationLF) : Decidable (LFAvailable ne lf)

Equations

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

theorem Guerrini2026.nominal_denotations : (CanDenote NominalExpression.englishBarePlural Semantics.Kinds.NMP.NominalDenotation.kind ∧ CanDenote NominalExpression.englishBarePlural Semantics.Kinds.NMP.NominalDenotation.property) ∧ (CanDenote NominalExpression.italianDefinitePlural Semantics.Kinds.NMP.NominalDenotation.kind ∧ ¬CanDenote NominalExpression.italianDefinitePlural Semantics.Kinds.NMP.NominalDenotation.property) ∧ ¬CanDenote NominalExpression.italianBarePlural Semantics.Kinds.NMP.NominalDenotation.kind ∧ CanDenote NominalExpression.italianBarePlural Semantics.Kinds.NMP.NominalDenotation.property

English BPs are ambiguous (kind and property); Italian definite plurals denote kinds only; Italian bare plurals denote properties only.

theorem Guerrini2026.diagram_145_four_paths : (LFAvailable NominalExpression.englishBarePlural GeneralizationLF.bonaFideGeneric ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.distributiveKindPred ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.cumulativeKindPred ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.existentialDPP) ∧ (LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.distributiveKindPred ∧ ¬LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.existentialDPP) ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ LFAvailable NominalExpression.italianBarePlural GeneralizationLF.existentialDPP

The four LF paths of diagram (145): English BPs access all four; Italian definite plurals the kind paths (no DPP); Italian bare plurals the property paths (no DKP/CKP).

Table 1: distribution of generalizations

inductive Guerrini2026.NominalForm : Type

Nominal form in a generalization.

• kindDenotingPlural : NominalForm
• singularIndefinite : NominalForm

@[implicit_reducible]

instance Guerrini2026.instDecidableEqNominalForm : DecidableEq NominalForm

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprNominalForm : Repr NominalForm

Equations

• Guerrini2026.instReprNominalForm = { reprPrec := Guerrini2026.instReprNominalForm.repr }

def Guerrini2026.instReprNominalForm.repr : NominalForm → ℕ → Std.Format

Equations

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

def Guerrini2026.table1 : NominalForm → Bool → Bool

Table 1: kind-denoting plurals appear in both flavors; singular indefinites only in law-like ones. (true = felicitous; the kind/law-like cell uses lfFlavor-style booleans.)

Equations

• Guerrini2026.table1 Guerrini2026.NominalForm.kindDenotingPlural x✝ = true
• Guerrini2026.table1 Guerrini2026.NominalForm.singularIndefinite x✝ = x✝

theorem Guerrini2026.singular_no_accidental : Semantics.Kinds.NMP.downDefinedFor MassCount.count false = false ∧ (∀ (lf : GeneralizationLF), lfFlavor lf = false → lf = GeneralizationLF.distributiveKindPred ∨ lf = GeneralizationLF.cumulativeKindPred ∨ lf = GeneralizationLF.existentialDPP) ∧ table1 NominalForm.singularIndefinite false = false

Singular indefinites lack the accidental flavor — the end of a four-step chain: ∩ undefined for singular count nouns ⇒ no kind denotation ⇒ no DKP/CKP ⇒ only BFG ⇒ only law-like.

theorem Guerrini2026.table1_from_lf_structure : (∃ (lf : GeneralizationLF), LFAvailable NominalExpression.englishBarePlural lf ∧ lfFlavor lf = true) ∧ (∃ (lf : GeneralizationLF), LFAvailable NominalExpression.englishBarePlural lf ∧ lfFlavor lf = false) ∧ lfFlavor GeneralizationLF.bonaFideGeneric = true ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred

Table 1 is derivable from LF availability + LF→flavor: English BPs have LFs of both flavors; property-only nominals have only BFG (law-like).

Homogeneity removal (Table 3, §3.3)

DIST and Gen each contribute homogeneity. all removes DIST-homogeneity; always (a Q-adverb, = overt Gen) removes Gen-homogeneity.

inductive Guerrini2026.HomogeneityRemover : Type

The adverb/quantifier that removes a homogeneity source.

• all : HomogeneityRemover
• always : HomogeneityRemover

@[implicit_reducible]

instance Guerrini2026.instDecidableEqHomogeneityRemover : DecidableEq HomogeneityRemover

Equations

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

def Guerrini2026.instReprHomogeneityRemover.repr : HomogeneityRemover → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprHomogeneityRemover : Repr HomogeneityRemover

Equations

• Guerrini2026.instReprHomogeneityRemover = { reprPrec := Guerrini2026.instReprHomogeneityRemover.repr }

def Guerrini2026.removesHomogeneity : HomogeneityRemover → Bool → Bool

all targets DIST-homogeneity, always targets Gen-homogeneity. The boolean argument is true for DIST, false for Gen.

Equations

• Guerrini2026.removesHomogeneity Guerrini2026.HomogeneityRemover.all x✝ = x✝
• Guerrini2026.removesHomogeneity Guerrini2026.HomogeneityRemover.always x✝ = !x✝

theorem Guerrini2026.table3 : (removesHomogeneity HomogeneityRemover.all true = true ∧ removesHomogeneity HomogeneityRemover.always true = false) ∧ removesHomogeneity HomogeneityRemover.all false = false ∧ removesHomogeneity HomogeneityRemover.always false = true

Referential definite plurals (DIST only) accept all not always; singular indefinite generics (Gen only) accept always not all; kind-denoting plural generics (both, by ambiguity) accept both.

Subjunctive and aspect diagnostics (§3.5, §3.4)

inductive Guerrini2026.ItalianMood : Type

Italian mood on the relative clause modifying the subject DP.

• indicative : ItalianMood
• subjunctive : ItalianMood

@[implicit_reducible]

instance Guerrini2026.instDecidableEqItalianMood : DecidableEq ItalianMood

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprItalianMood : Repr ItalianMood

Equations

• Guerrini2026.instReprItalianMood = { reprPrec := Guerrini2026.instReprItalianMood.repr }

def Guerrini2026.instReprItalianMood.repr : ItalianMood → ℕ → Std.Format

Equations

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

def Guerrini2026.lfAvailableWithMood : ItalianMood → GeneralizationLF → Bool

The subjunctive is licensed only inside Gen's restrictor, so it forces the BFG parse (example (44)); the indicative keeps all parses.

Equations

• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.indicative x✝ = true
• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.subjunctive Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.subjunctive x✝ = false

theorem Guerrini2026.subjunctive_disambiguates (lf : GeneralizationLF) : lfAvailableWithMood ItalianMood.subjunctive lf = true ↔ lf = GeneralizationLF.bonaFideGeneric

The subjunctive disambiguates to BFG; the indicative preserves ambiguity.

inductive Guerrini2026.VPAspect : Type

VP aspect. Episodic VPs have no Hab/Gen, so BFG is unavailable and only the Gen-free parses survive — why episodic bare plurals get near-universal readings without generic quantification (§5).

• habitual : VPAspect
• episodic : VPAspect

@[implicit_reducible]

instance Guerrini2026.instDecidableEqVPAspect : DecidableEq VPAspect

Equations

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

def Guerrini2026.instReprVPAspect.repr : VPAspect → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprVPAspect : Repr VPAspect

Equations

• Guerrini2026.instReprVPAspect = { reprPrec := Guerrini2026.instReprVPAspect.repr }

def Guerrini2026.lfCompatibleWithAspect : VPAspect → GeneralizationLF → Bool

In episodic sentences BFG is unavailable; DKP/CKP/DPP remain.

Equations

• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.habitual x✝ = true
• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.episodic Guerrini2026.GeneralizationLF.bonaFideGeneric = false
• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.episodic x✝ = true

theorem Guerrini2026.episodic_kind_plural_advantage : lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.distributiveKindPred = true ∧ CanDenote NominalExpression.englishBarePlural Semantics.Kinds.NMP.NominalDenotation.kind ∧ Semantics.Kinds.NMP.downDefinedFor MassCount.count false = false ∧ lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.bonaFideGeneric = false

The episodic kind-plural advantage: DKP is available in episodics, BFG is not, and singular indefinites (∩ undefined for singular count) lack DKP.

Epistemic adjectives and singular kinds (§5.2.2, §6.2)

inductive Guerrini2026.AdjReading : Type

Adjective reading: a nonlocal (propositional) reading blocks kind denotation, hence DKP (examples (99)–(104)).

• localReading : AdjReading
• nonlocal : AdjReading

@[implicit_reducible]

instance Guerrini2026.instDecidableEqAdjReading : DecidableEq AdjReading

Equations

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

def Guerrini2026.instReprAdjReading.repr : AdjReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprAdjReading : Repr AdjReading

Equations

• Guerrini2026.instReprAdjReading = { reprPrec := Guerrini2026.instReprAdjReading.repr }

def Guerrini2026.adjSupportsKind : AdjReading → Bool

Only local adjective readings support kind predication.

Equations

• Guerrini2026.adjSupportsKind Guerrini2026.AdjReading.localReading = true
• Guerrini2026.adjSupportsKind Guerrini2026.AdjReading.nonlocal = false

def Guerrini2026.singularKindLFAvailable : GeneralizationLF → Bool

Singular kind terms are atomic (following [Bar92], [Sch96b], [Day04]): DIST and ** need pluralities, so only BFG is available — no accidental or cumulative readings (§6.2, examples (133)–(136)).

Equations

• Guerrini2026.singularKindLFAvailable Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.singularKindLFAvailable x✝ = false

theorem Guerrini2026.singular_kind_law_like_only (lf : GeneralizationLF) : singularKindLFAvailable lf = true ↔ lf = GeneralizationLF.bonaFideGeneric

Singular kind terms support only law-like readings.

Prevalence bridge to [TG19] (§3.6)

Threshold semantics applies to the BFG parse. The DKP parse has no Gen: its truth conditions are extensional (DIST over the actual kind extension), hence stronger than any threshold generic. Prevalence is the bridge quantity.

def Guerrini2026.prevalenceAtWorld {Atom W : Type} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (ext : Finset Atom) (w : W) : ℚ

Prevalence of P among the atoms of an extension at w: |{a ∈ ext | P a w}| / |ext|. (Generalizes to Quantification.prevalenceOn ext (fun _ => True) (P · w).)

Equations

• Guerrini2026.prevalenceAtWorld P ext w = if ext.card = 0 then 0 else ↑{a ∈ ext | P a w}.card / ↑ext.card

theorem Guerrini2026.dkp_true_iff_prevalence_one {Atom W : Type} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (ext : Finset Atom) (w : W) (hne : ext.Nonempty) : Semantics.Plurality.distMaximal P ext w ↔ prevalenceAtWorld P ext w = 1

DKP is true (all actual kind members satisfy P) iff prevalence is 1: the extensional, non-generic truth condition of the DKP parse.

theorem Guerrini2026.dkp_false_iff_prevalence_zero {Atom W : Type} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (ext : Finset Atom) (w : W) : Semantics.Plurality.noneSatisfy P ext w ↔ prevalenceAtWorld P ext w = 0

DKP is determinately false iff prevalence is 0 (no kind member satisfies P).

theorem Guerrini2026.dkp_true_implies_generic_true_all_thresholds (θ : TesslerGoodman2019.GenThreshold) : TesslerGoodman2019.genericMeaning θ (Degree.deg 20 ⋯) = true

DKP-true entails the BFG (threshold) reading at every threshold: prevalence 100% exceeds them all.

theorem Guerrini2026.dkp_gap_is_threshold_sensitive : TesslerGoodman2019.genericMeaning (Degree.thr 12 ⋯) (Degree.deg 14 ⋯) = true ∧ TesslerGoodman2019.genericMeaning (Degree.thr 16 ⋯) (Degree.deg 14 ⋯) = false

The threshold-sensitive region is where the two parses do real work: at 70% prevalence the generic is true against a 60% threshold, false against 80%.

theorem Guerrini2026.parses_can_disagree : ¬Semantics.Plurality.allSatisfy (fun (a : Fin 10) (x : Fin 1) => ↑a < 7) Finset.univ 0 ∧ ¬Semantics.Plurality.noneSatisfy (fun (a : Fin 10) (x : Fin 1) => ↑a < 7) Finset.univ 0 ∧ TesslerGoodman2019.genericMeaning (Degree.thr 12 ⋯) (Degree.deg 14 ⋯) = true

The parses can disagree: at 7-of-10 the DKP parse is a trivalent gap (not all, not none) while the BFG parse is true at a 60% threshold.

Empirical predictions over the (21)–(136) stimuli

Stimuli are typed LinguisticExample rows in Data/Examples/Guerrini2026.json. featOf/readOf project the paper-specific tags and reading-level judgments.

def Guerrini2026.featOf (r : Data.Examples.LinguisticExample) (k : String) : Option String

A paper-feature value of an example row.

Equations

• Guerrini2026.featOf r k = Option.map (fun (x : String × String) => x.2) (List.find? (fun (x : String × String) => x.1 == k) r.paperFeatures)

def Guerrini2026.readOf (r : Data.Examples.LinguisticExample) (n : String) : Option Features.Judgment

A reading-level judgment of an example row.

Equations

• Guerrini2026.readOf r n = Option.map (fun (x : String × Features.Judgment) => x.2) (List.find? (fun (x : String × Features.Judgment) => x.1 == n) r.readings)

theorem Guerrini2026.genericity_table1_data : ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "genericity" && featOf r "nominalForm" == some "kindDenotingPlural") Examples.all).all fun (x : Data.Examples.LinguisticExample) => x.judgment == Features.Judgment.acceptable) = true ∧ ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "genericity" && featOf r "nominalForm" == some "singularIndefinite" && featOf r "flavor" == some "accidental") Examples.all).all fun (x : Data.Examples.LinguisticExample) => x.judgment == Features.Judgment.unacceptable) = true

Table 1 over the (21)/(22) stimuli: kind-denoting plurals are felicitous in both flavors; singular indefinites are infelicitous in accidental ones.

theorem Guerrini2026.near_universal_tracks_kind : ((List.filter (fun (r : Data.Examples.LinguisticExample) => (featOf r "diagnostic" == some "episodic" || featOf r "diagnostic" == some "epistemic-adj") && (featOf r "nominalForm" == some "kindDenotingPlural" || featOf r "adjReading" == some "local")) Examples.all).all fun (x : Data.Examples.LinguisticExample) => readOf x "near-universal" == some Features.Judgment.acceptable) = true ∧ ((List.filter (fun (r : Data.Examples.LinguisticExample) => (featOf r "diagnostic" == some "episodic" || featOf r "diagnostic" == some "epistemic-adj") && (featOf r "nominalForm" == some "singularIndefinite" || featOf r "adjReading" == some "nonlocal")) Examples.all).all fun (x : Data.Examples.LinguisticExample) => readOf x "near-universal" == some Features.Judgment.unacceptable) = true

Near-universal asymmetry across episodics (§5) and epistemic adjectives (§5.2.2): kind-denoting plurals and local adjectives get the near-universal (DKP) reading; singular indefinites and nonlocal adjectives do not.

theorem Guerrini2026.accidental_tracks_kind : ((List.filter (fun (r : Data.Examples.LinguisticExample) => (featOf r "diagnostic" == some "greenberg" || featOf r "diagnostic" == some "italian-gen") && (featOf r "nominalForm" == some "kindDenotingPlural" || featOf r "nominalExpression" == some "italianDefinitePlural")) Examples.all).all fun (x : Data.Examples.LinguisticExample) => readOf x "accidental" == some Features.Judgment.acceptable) = true ∧ ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "greenberg" && featOf r "nominalForm" == some "singularIndefinite") Examples.all).all fun (x : Data.Examples.LinguisticExample) => readOf x "accidental" == some Features.Judgment.unacceptable) = true

Accidental-reading asymmetry, including the [Gre04]/[Gre07] data reported in §3.7: kind-denoting plurals license accidental readings, singular indefinites do not.

theorem Guerrini2026.singular_kind_divergence_data : ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "singular-kind" && featOf r "kindTermNumber" == some "singular") Examples.all).all fun (r : Data.Examples.LinguisticExample) => readOf r "accidental" == some Features.Judgment.unacceptable && readOf r "cumulative" == some Features.Judgment.unacceptable) = true ∧ ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "singular-kind" && featOf r "kindTermNumber" == some "plural") Examples.all).all fun (x : Data.Examples.LinguisticExample) => readOf x "accidental" == some Features.Judgment.acceptable) = true

Singular vs plural kind terms (§6.2): singular kind terms lack accidental and cumulative readings; plural kind terms have the accidental reading.

theorem Guerrini2026.qadv_and_cumulativity_data : ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "homogeneity-removal" && featOf r "remover" == some "all") Examples.all).all fun (x : Data.Examples.LinguisticExample) => x.judgment == Features.Judgment.acceptable) = true ∧ ((List.filter (fun (r : Data.Examples.LinguisticExample) => featOf r "diagnostic" == some "homogeneity-removal" && featOf r "remover" == some "always") Examples.all).all fun (x : Data.Examples.LinguisticExample) => x.judgment == Features.Judgment.unacceptable) = true ∧ (readOf Examples.ex68a "cumulative" == some Features.Judgment.acceptable) = true ∧ (readOf Examples.ex69 "cumulative" == some Features.Judgment.unacceptable) = true

Q-adverb and cumulativity diagnostics: always/Q-adverbs (overt Gen) strip the DKP/CKP readings while all (the DIST counterpart) does not — no Gen.

Bridge to [Lon01]

theorem Guerrini2026.referential_iff_longobardi_kind : (Longobardi2001.bnCanBeReferential Longobardi2001.english = true ↔ CanDenote NominalExpression.englishBarePlural Semantics.Kinds.NMP.NominalDenotation.kind) ∧ (Longobardi2001.bnCanBeReferential Longobardi2001.romance = false ↔ ¬CanDenote NominalExpression.italianBarePlural Semantics.Kinds.NMP.NominalDenotation.kind)

[Lon01]'s referential bare nominal = Guerrini's kind denotation; both bottom out in Chierchia's CanDenoteKind. English BPs can be referential/denote kinds; Italian (Romance) bare nominals cannot.

theorem Guerrini2026.strongd_to_table1 : Longobardi2001.romance.strongD = true ∧ Longobardi2001.toNominalMapping Longobardi2001.romance = Semantics.Kinds.NMP.NominalMapping.predOnly ∧ ¬Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.predOnly False ∧ ¬CanDenote NominalExpression.italianBarePlural Semantics.Kinds.NMP.NominalDenotation.kind ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ table1 NominalForm.singularIndefinite false = false

End-to-end chain from [Lon01]'s strongD to Table 1: Romance strongD ⇒ predOnly ⇒ no kind ⇒ no DKP ⇒ no accidental flavor.

Cross-framework divergences: DKP/CKP are non-quantificational

Guerrini's "not a complex semantics for Gen" makes the accidental and cumulative readings non-quantificational, against the rivals [Coh99] (majority/proportional Gen) and [Nic09] (ways-of-normality Gen), which treat the same data as a quantifier. These theorems put the analyses on shared models and show they disagree on truth value and ontology.

theorem Guerrini2026.dkp_vs_cohen_disagree : ¬distributiveKindPred (fun (x : Fin 1) => Finset.univ) (fun (a : Fin 10) (x : Fin 1) => ↑a < 7) 0 ∧ ¬Semantics.Plurality.noneSatisfy (fun (a : Fin 10) (x : Fin 1) => ↑a < 7) Finset.univ 0 ∧ (Cohen1999.cohenGEN Finset.univ (fun (x : Fin 10) => True) fun (a : Fin 10) => ↑a < 7) ∧ involvesGen GeneralizationLF.distributiveKindPred = false

DKP vs [Coh99], one shared 7-of-10 model. Cohen's majority Gen judges it true (7/10 > 1/2) as a proportional quantifier (cohen_proportional); the DKP parse is a trivalent gap with no Gen. Same datum, opposite ontology.

inductive Guerrini2026.Habitat : Type

Habitat of an elephant in [Nic09]'s shared model (6 African, 4 Asian).

• africa : Habitat
• asia : Habitat

@[implicit_reducible]

instance Guerrini2026.instDecidableEqHabitat : DecidableEq Habitat

Equations

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

def Guerrini2026.instReprHabitat.repr : Habitat → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Guerrini2026.instReprHabitat.repr Guerrini2026.Habitat.asia prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Guerrini2026.Habitat.asia")).group prec✝

@[implicit_reducible]

instance Guerrini2026.instReprHabitat : Repr Habitat

Equations

• Guerrini2026.instReprHabitat = { reprPrec := Guerrini2026.instReprHabitat.repr }

def Guerrini2026.elephantLives : Nickel2009.Entity → Habitat → Prop

Which habitat each elephant lives in.

Equations

• Guerrini2026.elephantLives x✝ Guerrini2026.Habitat.africa = (x✝.id < 6)
• Guerrini2026.elephantLives x✝ Guerrini2026.Habitat.asia = (x✝.id ≥ 6)

@[implicit_reducible]

instance Guerrini2026.instDecidableElephantLives (e : Nickel2009.Entity) (h : Habitat) : Decidable (elephantLives e h)

Equations

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

theorem Guerrini2026.ckp_vs_gen_on_elephants : cumulativeKindPred elephantLives Nickel2009.elephants {Habitat.africa, Habitat.asia} ∧ involvesGen GeneralizationLF.cumulativeKindPred = false ∧ Nickel2009.nickelConjunctiveGEN Nickel2009.elephants Nickel2009.elephantNormalIn Nickel2009.ways Nickel2009.isElephant Nickel2009.livesInAfrica Nickel2009.livesInAsia ∧ ¬Cohen1999.cohenGEN Nickel2009.elephants Nickel2009.isElephant Nickel2009.livesInAsia

CKP vs [Nic09]/[Coh99] on "Elephants live in Africa and Asia". Cumulative kind predication succeeds with no Gen; Nickel's conjunctive Gen succeeds as a quantifier; Cohen's majority Gen fails on the Asia conjunct (4/10 < 1/2). One datum, three analyses; only Guerrini's is non-quantificational.