Guerrini (2026): Distributive Kind Predication

@cite{guerrini-2026}

Natural Language Semantics. Published online 02 March 2026.

Core Thesis

Generalizations with kind-denoting plurals (English bare plurals, Italian definite plurals) are structurally ambiguous between:

1. Bona Fide Genericity: the kind enters the restrictor of Gen → law-like reading ("Lions hunt" ≈ "Generally, lions hunt")
2. Distributive Kind Predication: the kind is evaluated at the actual world and DIST distributes the predicate over its atomic members → accidental reading ("LLMs are popular" ≈ "The LLMs are popular")

This ambiguity — not a complex semantics for Gen — explains why kind-denoting plurals have wider distribution than singular indefinites. Singular indefinites cannot denote kinds (∩ undefined for singulars), so DIST never applies, and they are limited to Bona Fide Genericity.

Key Predictions

• Table 1: Kind-denoting plurals appear in both law-like and accidental generalizations; singular indefinites appear only in law-like ones.
• Table 3: Homogeneity removal — 'all' removes DIST-homogeneity, 'always' removes Gen-homogeneity. Kind-denoting plurals allow both; singular indefinites allow only 'always'.
• Italian subjunctive: Forces Bona Fide Generic parse (kind must be in Gen restrictor, which licenses subjunctive). Accidental readings disappear under subjunctive-modified restrictors.
• Episodic sentences (§5): Near-universal readings of bare plurals ("Birds are migrating" ≈ ∀) arise via Distributive Kind Predication without Gen. Singular indefinites get only existential readings.

Connection to Tessler & Goodman (2019)

@cite{tessler-goodman-2019}'s threshold semantics for generics (see Phenomena/Generics/Studies/TesslerGoodman2019.lean) applies to the Bona Fide Generic parse: prevalence-based inference determines whether the Gen-quantified generalization is judged true. But on the Distributive Kind Predication parse, there is no Gen — the sentence is non-generic, and its truth conditions are those of a referential definite plural with DIST. Guerrini's ambiguity thus explains why "accidental" generalizations resist Q-adverb modification and don't display quantificational variability effects: they aren't quantified.

Nominal Mapping and Cross-Linguistic Variation

English bare plurals are ambiguous between kind and property denotation:

• Kind → Distributive/cumulative LFs or Bona Fide Generic LFs
• Property → Bona Fide Generic LFs or low-scoped existential LFs

Italian definite plurals unambiguously denote kinds. Italian bare plurals unambiguously denote properties.

This derives from @cite{chierchia-1998}'s Nominal Mapping Parameter: English [+arg, +pred] allows both; Italian [-arg, +pred] forces D.

inductive Guerrini2026.GeneralizationLF : Type

Available LF parses for sentences with kind-denoting plurals.

Guerrini's central claim: English bare plurals are structurally ambiguous between four LF types (diagram (145)). The first three require kind denotation; the fourth requires property denotation.

Kind-denoting plurals can access all four; singular indefinites access only BFG.

• bonaFideGeneric : GeneralizationLF

  Kind enters restrictor of Gen. World variable bound by Gen. Law-like reading: "Generally, lions hunt." (Guerrini's (29))

• distributiveKindPred : GeneralizationLF

  Kind evaluated at actual world s₀, DIST distributes predicate over atoms. No Gen. Accidental reading: "The lions (of the actual world) hunt." (Guerrini's (30))

• cumulativeKindPred : GeneralizationLF

  Kind evaluated at actual world s₀, ** (cumulative operator) applies. No Gen. "Elephants live in Africa and Asia." (§4)

• existentialDPP : GeneralizationLF

  Property reading: bare plural interpreted as property, composed with predicate via DPP (Derived Property Predication, §5.3). Low-scoped existential: "Bears are destroying my garden" ≈ ∃x[bear(x) ∧ destroying-my-garden(x)]. (Guerrini's (105b))

@[implicit_reducible]

instance Guerrini2026.instDecidableEqGeneralizationLF : DecidableEq GeneralizationLF

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprGeneralizationLF : Repr GeneralizationLF

Equations

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

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

Equations

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

noncomputable def Guerrini2026.kindExtensionFinset {Atom W : Type} [Fintype Atom] (k : Semantics.Kinds.NMP.Kind W Atom) (w : W) : Finset Atom

Extract a kind's extension at a world as a Finset, bridging NMP's Set Atom to Distributivity's Finset Atom.

This is the type-level bridge between the two modules:

• Kind.concept w : Set Atom (mathematical, for proofs)
• Finset Atom (computational, for DIST)

Equations

• Guerrini2026.kindExtensionFinset k w = {x : Atom | x ∈ k.concept w}

def Guerrini2026.kindExtensionOfBool {Atom W : Type} [Fintype Atom] (member : W → Atom → Bool) (w : W) : Finset Atom

Computable kind extension from a Bool-valued membership test. Use this for finite verification instead of the noncomputable kindExtensionFinset, which requires Classical.dec for Set membership.

Example usage:

def lionMember : World → Animal → Bool
  | _, .simba => true | _, .nala => true | _, _ => false
def lionExt := kindExtensionOfBool lionMember

Then pass lionExt directly to distributiveKindPred.

Equations

• Guerrini2026.kindExtensionOfBool member w = {a : Atom | member w a = true}

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

Distributive Kind Predication: evaluate a kind at the actual world to get its maximal sum, then distribute a predicate over its atomic parts.

This is the composition of DIST from Plural/Distributivity.lean with kind extension from NMP.lean. No Gen operator is involved.

Parameterized by kindExtension : W → Finset Atom (the computational representation of the kind's extension). For a Kind value, use kindExtensionFinset to obtain this.

Guerrini (2026), structure (30): ∀y(y ≤ ∩lions_{s₀}) → ⟦hunt⟧_{s₀}(y)

Equations

• Guerrini2026.distributiveKindPred kindExtension P s₀ = decide (Semantics.Plurality.Distributivity.distMaximal P (kindExtension s₀) s₀)

def Guerrini2026.distributiveKindPredTV {Atom W : Type} (kindExtension : W → Finset Atom) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (s₀ : W) : Core.Duality.Truth3

Trivalent truth value for Distributive Kind Predication.

Inherits homogeneity and non-maximality from DIST on referential plurals (Križ & Spector 2021). This predicts that accidental generalizations with bare plurals behave like referential definite plurals w.r.t. polarity reversals and exception tolerance.

Equations

• Guerrini2026.distributiveKindPredTV kindExtension P s₀ = Semantics.Plurality.Distributivity.pluralTruthValue P (kindExtension s₀) s₀

noncomputable def Guerrini2026.distributiveKindPredOfKind {Atom W : Type} [Fintype Atom] (k : Semantics.Kinds.NMP.Kind W Atom) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (s₀ : W) : Bool

Distributive Kind Predication composed directly from a Kind value. Noncomputable because Set.toFinset requires classical decidability.

Equations

• Guerrini2026.distributiveKindPredOfKind k P s₀ = Guerrini2026.distributiveKindPred (Guerrini2026.kindExtensionFinset k) P s₀

inductive Guerrini2026.GenFlavor : Type

Flavor of a generalization.

• lawLike : GenFlavor

  Law-like: "LLMs utilize Deep Learning" — true by necessity/regularity

• accidental : GenFlavor

  Accidental: "LLMs are popular" — contingently true of actual instances

@[implicit_reducible]

instance Guerrini2026.instDecidableEqGenFlavor : DecidableEq GenFlavor

Equations

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

def Guerrini2026.instReprGenFlavor.repr : GenFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprGenFlavor : Repr GenFlavor

Equations

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

inductive Guerrini2026.NominalForm : Type

Nominal form in the generalization.

• kindDenotingPlural : NominalForm

  Kind-denoting plural: English bare plural or Italian definite plural

• singularIndefinite : NominalForm

  Singular indefinite: "A lion hunts" / "Un leone caccia"

@[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 (form : NominalForm) (flavor : GenFlavor) : Bool

Table 1 from Guerrini (2026): distribution of generalizations.

Kind-denoting plurals can appear in both law-like and accidental generalizations. Singular indefinites can appear only in law-like ones. The * for singular indefinite + accidental means the form is possible only with a law-like construal forced.

Equations

• Guerrini2026.table1 Guerrini2026.NominalForm.kindDenotingPlural Guerrini2026.GenFlavor.lawLike = true
• Guerrini2026.table1 Guerrini2026.NominalForm.kindDenotingPlural Guerrini2026.GenFlavor.accidental = true
• Guerrini2026.table1 Guerrini2026.NominalForm.singularIndefinite Guerrini2026.GenFlavor.lawLike = true
• Guerrini2026.table1 Guerrini2026.NominalForm.singularIndefinite Guerrini2026.GenFlavor.accidental = false

theorem Guerrini2026.kind_plural_wider_distribution : (∀ (f : GenFlavor), table1 NominalForm.kindDenotingPlural f = true) ∧ ¬∀ (f : GenFlavor), table1 NominalForm.singularIndefinite f = true

Kind-denoting plurals have wider distribution than singular indefinites.

def Guerrini2026.lfFlavor : GeneralizationLF → GenFlavor

The LF parse determines the generalization flavor.

BFG → law-like (modal generalization, Gen quantifies over situations). DKP/CKP → accidental (no Gen; predicate applies to actual kind instances). DPP → neither law-like nor accidental: it's an existential episodic reading, not a generalization at all. We classify it as accidental (non-generic).

Equations

• Guerrini2026.lfFlavor Guerrini2026.GeneralizationLF.bonaFideGeneric = Guerrini2026.GenFlavor.lawLike
• Guerrini2026.lfFlavor Guerrini2026.GeneralizationLF.distributiveKindPred = Guerrini2026.GenFlavor.accidental
• Guerrini2026.lfFlavor Guerrini2026.GeneralizationLF.cumulativeKindPred = Guerrini2026.GenFlavor.accidental
• Guerrini2026.lfFlavor Guerrini2026.GeneralizationLF.existentialDPP = Guerrini2026.GenFlavor.accidental

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

The accidental flavor is unavailable for singular indefinites.

Full derivation chain from the paper's argument:

1. ∩ is undefined for singular count nouns (@cite{chierchia-1998})
2. Without ∩, no kind denotation is available
3. Without kind denotation, DKP and CKP are unavailable
4. Without DKP/CKP, the only LF is BFG → only law-like readings

This explains why singular indefinites have a narrower distribution than kind-denoting plurals in generalizations.

inductive Guerrini2026.HomogeneitySource : Type

Operator that introduces homogeneity (Guerrini's Table 3).

• dist : HomogeneitySource

  DIST: distributes over individuals; homogeneity from trivalence

• gen : HomogeneitySource

  Gen: modal quantifier; homogeneity from generic quantification

@[implicit_reducible]

instance Guerrini2026.instDecidableEqHomogeneitySource : DecidableEq HomogeneitySource

Equations

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

def Guerrini2026.instReprHomogeneitySource.repr : HomogeneitySource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprHomogeneitySource : Repr HomogeneitySource

Equations

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

inductive Guerrini2026.HomogeneityRemover : Type

Homogeneity remover: the adverb/quantifier that removes homogeneity.

• all : HomogeneityRemover

  'all': replaces DIST with non-homogeneous universal ∀

• always : HomogeneityRemover

  'always': replaces Gen with non-homogeneous universal ∀

@[implicit_reducible]

instance Guerrini2026.instDecidableEqHomogeneityRemover : DecidableEq HomogeneityRemover

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprHomogeneityRemover : Repr HomogeneityRemover

Equations

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

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

Equations

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

def Guerrini2026.removesHomogeneity (r : HomogeneityRemover) (s : HomogeneitySource) : Bool

Table 3: which removers apply to which sources.

'all' removes DIST-homogeneity (it's the non-homogeneous counterpart of DIST). 'always' removes Gen-homogeneity (it's a non-homogeneous Q-adverb replacing Gen).

Equations

• Guerrini2026.removesHomogeneity Guerrini2026.HomogeneityRemover.all Guerrini2026.HomogeneitySource.dist = true
• Guerrini2026.removesHomogeneity Guerrini2026.HomogeneityRemover.always Guerrini2026.HomogeneitySource.gen = true
• Guerrini2026.removesHomogeneity Guerrini2026.HomogeneityRemover.all Guerrini2026.HomogeneitySource.gen = false
• Guerrini2026.removesHomogeneity Guerrini2026.HomogeneityRemover.always Guerrini2026.HomogeneitySource.dist = false

inductive Guerrini2026.SentenceType : Type

Sentence type and its homogeneous LF sources.

• referentialDefinitePlural : SentenceType

  Referential definite plural: "The kids are American"

• singularIndefiniteGeneric : SentenceType

  Singular indefinite generic: "A lion hunts"

• kindDenotingPluralGeneric : SentenceType

  Kind-denoting plural generic: "Lions hunt"

@[implicit_reducible]

instance Guerrini2026.instDecidableEqSentenceType : DecidableEq SentenceType

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprSentenceType : Repr SentenceType

Equations

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

def Guerrini2026.instReprSentenceType.repr : SentenceType → ℕ → Std.Format

Equations

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

def Guerrini2026.hasHomogeneitySource (st : SentenceType) (hs : HomogeneitySource) : Bool

Which homogeneity sources are present in each sentence type.

Referential definite plurals have only DIST. Singular indefinite generics have only Gen. Kind-denoting plural generics have BOTH (due to structural ambiguity).

Equations

• Guerrini2026.hasHomogeneitySource Guerrini2026.SentenceType.referentialDefinitePlural Guerrini2026.HomogeneitySource.dist = true
• Guerrini2026.hasHomogeneitySource Guerrini2026.SentenceType.referentialDefinitePlural Guerrini2026.HomogeneitySource.gen = false
• Guerrini2026.hasHomogeneitySource Guerrini2026.SentenceType.singularIndefiniteGeneric Guerrini2026.HomogeneitySource.dist = false
• Guerrini2026.hasHomogeneitySource Guerrini2026.SentenceType.singularIndefiniteGeneric Guerrini2026.HomogeneitySource.gen = true
• Guerrini2026.hasHomogeneitySource Guerrini2026.SentenceType.kindDenotingPluralGeneric Guerrini2026.HomogeneitySource.dist = true
• Guerrini2026.hasHomogeneitySource Guerrini2026.SentenceType.kindDenotingPluralGeneric Guerrini2026.HomogeneitySource.gen = true

def Guerrini2026.removerAvailable (st : SentenceType) (r : HomogeneityRemover) : Bool

Which removers are available for each sentence type.

Equations

• Guerrini2026.removerAvailable st Guerrini2026.HomogeneityRemover.all = Guerrini2026.hasHomogeneitySource st Guerrini2026.HomogeneitySource.dist
• Guerrini2026.removerAvailable st Guerrini2026.HomogeneityRemover.always = Guerrini2026.hasHomogeneitySource st Guerrini2026.HomogeneitySource.gen

theorem Guerrini2026.refDefPl_removers : removerAvailable SentenceType.referentialDefinitePlural HomogeneityRemover.all = true ∧ removerAvailable SentenceType.referentialDefinitePlural HomogeneityRemover.always = false

Referential definite plurals: 'all' OK, 'always' not. "The bears are all brown" OK vs "#The bears are always brown"

theorem Guerrini2026.singIndef_removers : removerAvailable SentenceType.singularIndefiniteGeneric HomogeneityRemover.all = false ∧ removerAvailable SentenceType.singularIndefiniteGeneric HomogeneityRemover.always = true

Singular indefinite generics: 'always' OK, 'all' not. "A bear is always brown" OK vs "#A bear is all brown"

theorem Guerrini2026.kindPlural_removers : removerAvailable SentenceType.kindDenotingPluralGeneric HomogeneityRemover.all = true ∧ removerAvailable SentenceType.kindDenotingPluralGeneric HomogeneityRemover.always = true

Kind-denoting plural generics: BOTH 'all' and 'always' OK. "Bears are all brown" OK AND "Bears are always brown" OK

inductive Guerrini2026.NominalExpression : Type

Cross-linguistic nominal form.

• 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 for each nominal expression.

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.

Equations

• Guerrini2026.HasD Guerrini2026.NominalExpression.englishBarePlural = False
• Guerrini2026.HasD Guerrini2026.NominalExpression.italianDefinitePlural = True
• Guerrini2026.HasD Guerrini2026.NominalExpression.italianBarePlural = 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) (nd : Phenomena.Generics.KindReference.NominalDenotation) : Prop

Available denotations for each nominal form in argument position.

For kind denotation, derived from CanDenoteKind (Chierchia 1998). For property denotation, derived from the Nominal Mapping Parameter combined with D-status:

• argOnly [+arg, -pred]: nouns are kinds, never properties
• argAndPred [+arg, +pred]: property denotation always available (D gives definiteness, not kind-forcing)
• predOnly [-arg, +pred]: nouns start as predicates; D maps them to kinds (via ∩), blocking the property reading

This yields:

• English BPs [+arg, +pred, -D]: both kind and property ✓
• Italian def pl [-arg, +pred, +D]: kind only (D forces kind) ✓
• Italian bare pl [-arg, +pred, -D]: property only (no ∩) ✓

Equations

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

@[implicit_reducible]

instance Guerrini2026.instDecidableCanDenote (ne : NominalExpression) (nd : Phenomena.Generics.KindReference.NominalDenotation) : Decidable (CanDenote ne nd)

Equations

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

theorem Guerrini2026.english_bp_ambiguous : CanDenote NominalExpression.englishBarePlural Phenomena.Generics.KindReference.NominalDenotation.kind ∧ CanDenote NominalExpression.englishBarePlural Phenomena.Generics.KindReference.NominalDenotation.property

English bare plurals are ambiguous.

theorem Guerrini2026.italian_def_pl_kind_only : CanDenote NominalExpression.italianDefinitePlural Phenomena.Generics.KindReference.NominalDenotation.kind ∧ ¬CanDenote NominalExpression.italianDefinitePlural Phenomena.Generics.KindReference.NominalDenotation.property

Italian definite plurals unambiguously denote kinds.

theorem Guerrini2026.italian_bare_pl_property_only : ¬CanDenote NominalExpression.italianBarePlural Phenomena.Generics.KindReference.NominalDenotation.kind ∧ CanDenote NominalExpression.italianBarePlural Phenomena.Generics.KindReference.NominalDenotation.property

Italian bare plurals unambiguously denote properties.

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

Which LFs are available for a given nominal form.

Kind denotation enables DKP and CKP (kind-level LFs). Property denotation enables BFG (property enters Gen restrictor) and existential DPP (property yields low-scoped ∃). Diagram (145): four paths for English BPs, two via kind, two via property.

Equations

• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.bonaFideGeneric = True
• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.distributiveKindPred = Guerrini2026.CanDenote ne Phenomena.Generics.KindReference.NominalDenotation.kind
• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.cumulativeKindPred = Guerrini2026.CanDenote ne Phenomena.Generics.KindReference.NominalDenotation.kind
• Guerrini2026.LFAvailable ne Guerrini2026.GeneralizationLF.existentialDPP = Guerrini2026.CanDenote ne Phenomena.Generics.KindReference.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.english_bp_all_lfs : LFAvailable NominalExpression.englishBarePlural GeneralizationLF.bonaFideGeneric ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.distributiveKindPred ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.cumulativeKindPred ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.existentialDPP

English bare plurals allow all four LFs (diagram (145)): kind path → BFG, DKP, CKP; property path → BFG, DPP.

theorem Guerrini2026.italian_def_pl_lfs : LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.bonaFideGeneric ∧ LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.distributiveKindPred ∧ LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.cumulativeKindPred ∧ ¬LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.existentialDPP

Italian definite plurals: kind-level LFs only (no property → no DPP). This predicts near-universal but no existential readings in episodics (§5.4).

theorem Guerrini2026.italian_bare_pl_lfs : LFAvailable NominalExpression.italianBarePlural GeneralizationLF.bonaFideGeneric ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.cumulativeKindPred ∧ LFAvailable NominalExpression.italianBarePlural GeneralizationLF.existentialDPP

Italian bare plurals: property-level LFs only (BFG + DPP, no DKP/CKP). This predicts existential but no near-universal readings in episodics (§5.4).

structure Guerrini2026.EpisodicDatum : Type

Episodic reading availability for bare plurals vs singular indefinites.

"Birds are migrating" can mean ≈ all birds are migrating (∀). "A bird is migrating" can only mean ∃ (or *∀ via Gen).

• sentence : String
• nominalForm : NominalForm
• nearUniversalOK : Bool

  Near-universal (∀) reading via DIST on kind extension?

• existentialOK : Bool

  Existential (∃) reading?

• notes : String

def Guerrini2026.birdsMigrating : EpisodicDatum

Equations

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

def Guerrini2026.aBirdMigrating : EpisodicDatum

Equations

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

def Guerrini2026.studentsScarred : EpisodicDatum

Equations

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

def Guerrini2026.aStudentScared : EpisodicDatum

Equations

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

def Guerrini2026.episodicData : List EpisodicDatum

Equations

• Guerrini2026.episodicData = [Guerrini2026.birdsMigrating, Guerrini2026.aBirdMigrating, Guerrini2026.studentsScarred, Guerrini2026.aStudentScared]

Italian as a disambiguator for episodic bare plural readings

@cite{guerrini-2026} §5.4: Italian separates the two LFs that are ambiguous in English bare plurals. English "investigative journalists asked questions" is ambiguous between:

• Kind reading (Italian definite plural): near-universal (DKP) "I giornalisti investigativi hanno posto domande" — all of them asked
• Property reading (Italian bare plural): existential (DPP) "Giornalisti investigativi hanno posto domande" — some of them asked

This is a direct consequence of the unambiguous denotation types in Italian: Italian definite plurals denote kinds → DKP → near-universal Italian bare plurals denote properties → DPP → existential

structure Guerrini2026.ItalianEpisodicDatum : Type

Italian episodic datum (examples (107)-(110), (113)-(114)).

• sentence : String
• gloss : String
• nominalExpression : NominalExpression
• nearUniversalOK : Bool
• existentialOK : Bool
• notes : String

def Guerrini2026.itDefPlJournalists : ItalianEpisodicDatum

Equations

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

def Guerrini2026.itBarePlJournalists : ItalianEpisodicDatum

Equations

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

def Guerrini2026.italianEpisodicData : List ItalianEpisodicDatum

Equations

• Guerrini2026.italianEpisodicData = [Guerrini2026.itDefPlJournalists, Guerrini2026.itBarePlJournalists]

theorem Guerrini2026.italian_episodic_disambiguation : ((List.filter (fun (x : ItalianEpisodicDatum) => x.nominalExpression == NominalExpression.italianDefinitePlural) italianEpisodicData).all fun (x : ItalianEpisodicDatum) => x.nearUniversalOK) = true ∧ ((List.filter (fun (x : ItalianEpisodicDatum) => x.nominalExpression == NominalExpression.italianBarePlural) italianEpisodicData).all fun (x : ItalianEpisodicDatum) => !x.nearUniversalOK) = true

Italian definite plurals get near-universal readings in episodics; Italian bare plurals get only existential readings. (§5.4)

structure Guerrini2026.ItalianGenDisambiguationDatum : Type

Italian generalization datum (§5.4, examples (113)-(114)).

• sentence : String
• gloss : String
• nominalExpression : NominalExpression
• accidentalOK : Bool

  Accidental reading available (via DKP)?

• lawLikeOK : Bool

  Law-like reading available (via BFG)?

• notes : String

def Guerrini2026.itDefPlCandidates : ItalianGenDisambiguationDatum

Equations

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

def Guerrini2026.itBarePlCandidates : ItalianGenDisambiguationDatum

Equations

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

def Guerrini2026.italianGenDisambiguationData : List ItalianGenDisambiguationDatum

Equations

• Guerrini2026.italianGenDisambiguationData = [Guerrini2026.itDefPlCandidates, Guerrini2026.itBarePlCandidates]

theorem Guerrini2026.italian_gen_disambiguation : ((List.filter (fun (x : ItalianGenDisambiguationDatum) => x.nominalExpression == NominalExpression.italianDefinitePlural) italianGenDisambiguationData).all fun (x : ItalianGenDisambiguationDatum) => x.accidentalOK) = true ∧ ((List.filter (fun (x : ItalianGenDisambiguationDatum) => x.nominalExpression == NominalExpression.italianBarePlural) italianGenDisambiguationData).all fun (x : ItalianGenDisambiguationDatum) => !x.accidentalOK) = true

Italian definite plurals support accidental generalizations; Italian bare plurals do not. Derived from kind denotation availability.

theorem Guerrini2026.italian_disambiguation_from_kind_denotation : CanDenote NominalExpression.italianDefinitePlural Phenomena.Generics.KindReference.NominalDenotation.kind ∧ LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.distributiveKindPred ∧ ¬CanDenote NominalExpression.italianBarePlural Phenomena.Generics.KindReference.NominalDenotation.kind ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ CanDenote NominalExpression.italianBarePlural Phenomena.Generics.KindReference.NominalDenotation.property

Both generalization and episodic disambiguation derive from the same kind-denotation chain: def pl can denote kind → DKP available → accidental / near-universal; bare pl cannot → no DKP → no accidental / no near-universal.

Guerrini × Tessler & Goodman: Where Pragmatics Applies

@cite{tessler-goodman-2019}'s threshold semantics and RSA inference apply specifically to the Bona Fide Generic parse. On this parse, a kind enters the restrictor of Gen, which is semantically parallel to a modalized universal quantifier. The threshold θ determines how many exceptions are tolerated, and pragmatic inference (L1 reasoning over priors on prevalence) explains context-sensitivity.

On the Distributive Kind Predication parse, by contrast, there is no Gen at all. The sentence's truth conditions are compositionally determined by DIST applied to the kind's extension at the evaluation world. This is a non-generic, non-quantificational reading. RSA generic inference does not apply here — the sentence is true iff (approximately) all actual members of the kind satisfy the predicate, modulo homogeneity/non-maximality from DIST.

Predictions for RSA

1. Accidental generalizations resist pragmatic threshold adjustment. "LLMs are popular" on the DKP parse is true iff the actual LLMs are popular — no threshold, no prevalence inference. This explains why accidental generalizations feel "factual" rather than "generic."

2. Law-like generalizations show prevalence sensitivity. "Lions hunt" on the BFG parse is judged via prevalence × prior, exactly as @cite{tessler-goodman-2019} predict. The same utterance on its DKP parse is judged as a factual claim about actual lions.

3. Q-adverb diagnostics align. "Lions usually hunt" forces the BFG parse (overt Q-adverb replaces Gen). Since only this parse involves generic quantification, only this parse is subject to Tessler & Goodman's pragmatic inference. The DKP parse is unavailable with overt Q-adverbs — DIST and Q-adverbs compete for the same structural position.

def Guerrini2026.subjectToGenericInference (lf : GeneralizationLF) : Bool

Whether a given LF parse is subject to RSA generic inference (Tessler & Goodman 2019's threshold semantics).

Equations

• Guerrini2026.subjectToGenericInference Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.subjectToGenericInference Guerrini2026.GeneralizationLF.distributiveKindPred = false
• Guerrini2026.subjectToGenericInference Guerrini2026.GeneralizationLF.cumulativeKindPred = false
• Guerrini2026.subjectToGenericInference Guerrini2026.GeneralizationLF.existentialDPP = false

theorem Guerrini2026.only_bfg_has_generic_inference : subjectToGenericInference GeneralizationLF.bonaFideGeneric = true ∧ subjectToGenericInference GeneralizationLF.distributiveKindPred = false ∧ subjectToGenericInference GeneralizationLF.cumulativeKindPred = false ∧ subjectToGenericInference GeneralizationLF.existentialDPP = false

Only the Bona Fide Generic parse is subject to T&G inference.

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 atoms in an extension at world w.

This is the proportion of kind-instances satisfying P: |{a ∈ ext | P(a,w)}| / |ext|. It is the bridge quantity between DKP (which checks ∀ atoms) and T&G (which checks prevalence > θ).

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.Distributivity.distMaximal P ext w ↔ prevalenceAtWorld P ext w = 1

DKP true ↔ prevalence = 1.

When all atoms in the kind's extension satisfy P, prevalence is 100%. This is the extensional, non-generic truth condition of the DKP parse: the generalization is "true" in the same way a referential definite plural statement is true — all actual instances satisfy the predicate.

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.Distributivity.noneSatisfy P ext w ↔ prevalenceAtWorld P ext w = 0

DKP trivalent-false ↔ prevalence = 0.

When no atoms satisfy P, the generalization is determinately false, not merely gapped.

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

DKP true implies T&G generic meaning is true at every threshold.

If DKP gives 'true' (all actual instances of the kind satisfy P), then prevalence = 100%, which exceeds every threshold in T&G's model. The DKP parse is a stronger truth condition than any threshold-based generic: it entails the BFG parse at all thresholds.

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

DKP gap is exactly the domain where T&G does real work.

When prevalence is intermediate (0 < p < 1), the DKP parse gives a trivalent gap (some but not all atoms satisfy P), while the BFG parse's truth depends on whether prevalence exceeds the threshold.

At p = 0.7 and θ = 0.6: generic meaning is true (0.7 > 0.6). At p = 0.7 and θ = 0.8: generic meaning is false (0.7 ≯ 0.8).

This is exactly the region where T&G's pragmatic inference — listener reasoning over priors on prevalence — determines the judgment. Guerrini's contribution is showing this inference applies only to the BFG parse, not the DKP parse.

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

The two parses can disagree: DKP gap with BFG true.

Witness: 10 atoms, 7 satisfy P, 3 don't.

• DKP: trivalent gap (not all satisfy, not none satisfy)
• BFG (at θ = 0.6): true (prevalence 0.7 > 0.6)

This formalizes Guerrini's core explanation: "accidental" generalizations feel factual (DKP requires near-universality) while "law-like" generalizations tolerate exceptions (BFG uses threshold, and pragmatic inference determines what counts as "enough").

inductive Guerrini2026.ItalianMood : Type

Italian mood in 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.subjunctiveForcesLawLike (mood : ItalianMood) : Bool

The Italian subjunctive is licensed inside the restrictor of Gen (a broadly intensional environment). Therefore:

• Subjunctive-modified DP → must be in Gen restrictor → BFG parse only
• Indicative-modified DP → compatible with both BFG and DKP parses

Guerrini (2026), example (44): "I candidati che si {presentano/presentino} con molto anticipo non vengono assunti."

• Indicative: law-like AND accidental readings available
• Subjunctive: only law-like reading available

Equations

• Guerrini2026.subjunctiveForcesLawLike Guerrini2026.ItalianMood.indicative = false
• Guerrini2026.subjunctiveForcesLawLike Guerrini2026.ItalianMood.subjunctive = true

def Guerrini2026.lfAvailableWithMood (mood : ItalianMood) (lf : GeneralizationLF) : Bool

Available LFs given mood on the relative clause.

Subjunctive is licensed inside the restrictor of Gen (an intensional environment). DKP, CKP, and DPP place the DP outside Gen, so the subject DP is not in Gen's restrictor — subjunctive is not licensed.

Equations

• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.indicative lf = true
• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.subjunctive Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.subjunctive Guerrini2026.GeneralizationLF.distributiveKindPred = false
• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.subjunctive Guerrini2026.GeneralizationLF.cumulativeKindPred = false
• Guerrini2026.lfAvailableWithMood Guerrini2026.ItalianMood.subjunctive Guerrini2026.GeneralizationLF.existentialDPP = false

theorem Guerrini2026.subjunctive_disambiguates : lfAvailableWithMood ItalianMood.subjunctive GeneralizationLF.bonaFideGeneric = true ∧ lfAvailableWithMood ItalianMood.subjunctive GeneralizationLF.distributiveKindPred = false ∧ lfAvailableWithMood ItalianMood.subjunctive GeneralizationLF.cumulativeKindPred = false ∧ lfAvailableWithMood ItalianMood.subjunctive GeneralizationLF.existentialDPP = false

Subjunctive disambiguates: only Bona Fide Generic survives.

theorem Guerrini2026.indicative_ambiguous : lfAvailableWithMood ItalianMood.indicative GeneralizationLF.bonaFideGeneric = true ∧ lfAvailableWithMood ItalianMood.indicative GeneralizationLF.distributiveKindPred = true ∧ lfAvailableWithMood ItalianMood.indicative GeneralizationLF.cumulativeKindPred = true ∧ lfAvailableWithMood ItalianMood.indicative GeneralizationLF.existentialDPP = true

Indicative preserves full ambiguity.

structure Guerrini2026.GenericityDatum : Type

Genericity datum from Guerrini (2026), examples (21)–(22).

• sentence : String
• language : String
• nominalForm : NominalForm
• flavor : GenFlavor
• felicitous : Bool
• notes : String

def Guerrini2026.llmsUtilizeDL : GenericityDatum

Equations

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

def Guerrini2026.aLLMUtilizesDL : GenericityDatum

Equations

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

def Guerrini2026.llmsArePopular : GenericityDatum

Equations

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

def Guerrini2026.aLLMIsPopular : GenericityDatum

Equations

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

def Guerrini2026.gliLLMUsanoDL : GenericityDatum

Equations

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

def Guerrini2026.unLLMUsaDL : GenericityDatum

Equations

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

def Guerrini2026.gliLLMSonoPopolari : GenericityDatum

Equations

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

def Guerrini2026.unLLMEPopolari : GenericityDatum

Equations

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

def Guerrini2026.genericityData : List GenericityDatum

Equations

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

BFG as an instance of GEN; DKP as an instance of DIST

The two parses connect to different operators in the theory layer:

• BFG instantiates traditionalGEN from Generics.lean: the kind's extension provides the restrictor, the VP provides the scope, and Gen's normalcy parameter captures the hidden context-dependence that @cite{tessler-goodman-2019}'s RSA model replaces with prevalence priors.

• DKP instantiates distMaximal from Distributivity.lean: no GEN operator is involved — the predicate distributes over the kind's extension at the actual world via DIST.

These are not parallel formalisms applied to the same data — they are structurally different semantic compositions that yield different truth conditions and different pragmatic properties.

def Guerrini2026.evalBFG (situations : List Semantics.Genericity.Generics.Situation) (normal : Semantics.Genericity.Generics.NormalcyPredicate) (kindRestrictor : Semantics.Genericity.Generics.Restrictor) (predScope : Semantics.Genericity.Generics.Scope) : Bool

The Bona Fide Generic parse is compositionally an instance of traditionalGEN: the kind provides the restrictor, the VP the scope, and Gen's normalcy parameter is the hidden contextual factor.

This function makes the compositional content of BFG explicit.

Equations

• Guerrini2026.evalBFG situations normal kindRestrictor predScope = Semantics.Genericity.Generics.traditionalGEN situations normal kindRestrictor predScope

theorem Guerrini2026.table1_from_lf_structure : (∃ (lf : GeneralizationLF), LFAvailable NominalExpression.englishBarePlural lf ∧ lfFlavor lf = GenFlavor.lawLike) ∧ (∃ (lf : GeneralizationLF), LFAvailable NominalExpression.englishBarePlural lf ∧ lfFlavor lf = GenFlavor.accidental) ∧ lfFlavor GeneralizationLF.bonaFideGeneric = GenFlavor.lawLike ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.cumulativeKindPred

Table 1 is derivable from LF availability + LF → flavor mapping.

Kind-denoting plurals support both flavors because they have LFs of both flavor types (BFG for law-like, DKP/CKP for accidental). Singular indefinites support only law-like because all their available LFs (just BFG) map to the law-like flavor.

theorem Guerrini2026.referential_iff_longobardi_kind : (Longobardi2001.bnCanBeReferential Longobardi2001.english = true ↔ CanDenote NominalExpression.englishBarePlural Phenomena.Generics.KindReference.NominalDenotation.kind) ∧ (Longobardi2001.bnCanBeReferential Longobardi2001.romance = false ↔ ¬CanDenote NominalExpression.italianBarePlural Phenomena.Generics.KindReference.NominalDenotation.kind)

@cite{longobardi-2001}'s referential BN reading corresponds to DKP/CKP parses: both require kind denotation. The bridge is through Chierchia's canDenoteKind, which both papers use.

English BPs: canDenote .englishBarePlural .kind = true (Guerrini) ↔ bnCanBeReferential english = true (Longobardi)

Italian bare plurals: canDenote .italianBarePlural .kind = false (Guerrini) ↔ bnCanBeReferential romance = false (Longobardi)

theorem Guerrini2026.quantificational_only_iff_bfg_only : LFAvailable NominalExpression.englishBarePlural GeneralizationLF.distributiveKindPred ∧ LFAvailable NominalExpression.englishBarePlural GeneralizationLF.cumulativeKindPred ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.cumulativeKindPred

@cite{longobardi-2001}'s quantificational-only BN = only BFG parse. DKP/CKP require kind denotation, which strongD blocks for BNs.

English BPs: all three LFs (BFG + DKP + CKP) Italian bare plurals: BFG only

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 Phenomena.Generics.KindReference.NominalDenotation.kind ∧ ¬LFAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred ∧ table1 NominalForm.singularIndefinite GenFlavor.accidental = false

End-to-end chain from @cite{longobardi-2001}'s strongD to Table 1:

1. strongD = true (Romance) → bnCanBeReferential = false
2. → canDenoteKind (.predOnly) false = false (Chierchia)
3. → canDenote .italianBarePlural .kind = false (Guerrini)
4. → lfAvailable .italianBarePlural .distributiveKindPred = false
5. → accidental generalizations unavailable (only BFG → law-like)
6. → table1 .singularIndefinite .accidental = false

theorem Guerrini2026.generic_type_matches_longobardi_flavor : lfFlavor GeneralizationLF.bonaFideGeneric = GenFlavor.lawLike ∧ lfFlavor GeneralizationLF.distributiveKindPred = GenFlavor.accidental

@cite{longobardi-2001}'s GenericType aligns with GenFlavor: indefinite generics are law-like (BFG); definite generics can be accidental (DKP).

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

Cumulative Kind Predication: evaluate a kind at the actual world, then apply the cumulative operator ** to the kind extension and a set of locations/arguments.

@cite{guerrini-2026} §4, structure (62): **(λy.λx.⟦Hab live-in⟧{s₀}(x, y))(Africa ⊕ Asia)(∩elephants{s₀})

This connects GeneralizationLF.cumulativeKindPred to the theory-layer ** operator from Cumulativity.lean.

Equations

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

Cumulativity Comes from ** (CKP), Not from Gen

@cite{guerrini-2026} §4.2: Gen itself does not encode cumulativity. Evidence:

1. Q-adverb test: Adding Q-adverbs (which replace Gen) removes cumulative readings. "Wugs are always/often/typically black, white, green, and red" — only the "all four colors simultaneously" reading survives, not the cumulative "each wug is one color" reading (ex. (69)).

2. Italian subjunctive test: Forcing the BFG parse (kind in Gen's restrictor) removes cumulative readings. "I linguisti che si occupino di semantica..." — only distributive, not cumulative (ex. (71)).

This means cumulative readings must arise from the CKP LF (which uses ** independently of Gen), not from a cumulative BFG LF.

structure Guerrini2026.CumulativityDiagnosticDatum : Type

Q-adverbs remove cumulative readings (§4.2, ex. (68)-(69)): forcing BFG parse eliminates cumulativity.

• sentence : String
• hasCumulative : Bool
• hasDistributive : Bool
• notes : String

def Guerrini2026.wugsColors : CumulativityDiagnosticDatum

Equations

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

def Guerrini2026.wugsQAdvColors : CumulativityDiagnosticDatum

Equations

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

theorem Guerrini2026.qadv_kills_cumulativity : wugsColors.hasCumulative = true ∧ wugsQAdvColors.hasCumulative = false ∧ wugsColors.hasDistributive = true ∧ wugsQAdvColors.hasDistributive = true

Q-adverbs kill cumulative readings, confirming that cumulative readings arise from ** (CKP) and not from Gen.

Epistemic Adjectives Block Kind Predication

@cite{guerrini-2026} §5.2.2: Nonlocal readings of epistemic adjectives like "unknown" and "unidentified" block kind denotation, which in turn blocks the near-universal reading via Distributive Kind Predication.

The argument: "unknown X" under its nonlocal reading ("X whose identity is unknown to the speaker") denotes a property that cannot correspond to a natural kind. Since ∩ is only defined for natural-kind-forming properties, the kind-level LF is unavailable, and so is DKP.

This provides independent evidence that near-universal episodic readings require kind denotation (via DKP), not just universality from context.

inductive Guerrini2026.AdjReading : Type

Whether an adjective reading supports kind predication.

• local : AdjReading

  Local: adjective modifies noun content (descriptive). "American voters" = voters who are American. Supports kind.

• nonlocal : AdjReading

  Nonlocal: adjective contributes propositional content. "Unknown voters" = voters whose identity is unknown to speaker. Does NOT support kind.

@[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.adjReadingSupportsKind : AdjReading → Bool

Kind predication is available only with local adjective readings.

Equations

• Guerrini2026.adjReadingSupportsKind Guerrini2026.AdjReading.local = true
• Guerrini2026.adjReadingSupportsKind Guerrini2026.AdjReading.nonlocal = false

structure Guerrini2026.EpistemicAdjDatum : Type

Epistemic adjective datum from @cite{guerrini-2026}, examples (99)–(104).

• bareNP : String
• adjReading : AdjReading
• nearUniversalOK : Bool
• existentialOK : Bool
• notes : String

def Guerrini2026.americanVoters : EpistemicAdjDatum

Equations

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

def Guerrini2026.unidentifiedVoters : EpistemicAdjDatum

Equations

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

def Guerrini2026.investigativeJournalists : EpistemicAdjDatum

Equations

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

def Guerrini2026.unknownJournalists : EpistemicAdjDatum

Equations

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

def Guerrini2026.epistemicAdjData : List EpistemicAdjDatum

Equations

• Guerrini2026.epistemicAdjData = [Guerrini2026.americanVoters, Guerrini2026.unidentifiedVoters, Guerrini2026.investigativeJournalists, Guerrini2026.unknownJournalists]

theorem Guerrini2026.epistemic_adj_from_kind_denotation : adjReadingSupportsKind AdjReading.local = true ∧ adjReadingSupportsKind AdjReading.nonlocal = false

The epistemic adjective diagnostic derives from the same kind-denotation → DKP chain as Table 1.

Local adj → kind OK → DKP available → near-universal OK Nonlocal adj → no kind → no DKP → near-universal blocked

Q-Adverb Resistance as a DKP Diagnostic

@cite{guerrini-2026} §3.1: Q-adverbs like "usually" and "rarely" are overt counterparts of Gen (Krifka et al. 1995). Since DKP does not involve Gen, Q-adverbs are incompatible with DKP readings. This provides a diagnostic: if a Q-adverb is added, only the BFG parse survives, and accidental readings disappear.

§5.1: Episodic bare plurals with DKP allow 'all' (DIST's non-homogeneous counterpart) but not 'always' (Gen's counterpart), confirming the absence of Gen from the DKP parse.

structure Guerrini2026.QAdvDatum : Type

Q-adverb diagnostic datum (§3.1 examples (25), (49); §5.1 examples (89)-(90)).

• sentence : String
• nominalForm : NominalForm
• qAdvCompatible : Bool

  Does adding a Q-adverb allow the intended reading?

• testedReading : GenFlavor

  What reading is being tested?

• notes : String

def Guerrini2026.lionsUsuallyExtinct : QAdvDatum

Equations

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

def Guerrini2026.llmsUsuallyPopular : QAdvDatum

Equations

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

def Guerrini2026.birdsAllMigrating : QAdvDatum

Equations

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

def Guerrini2026.birdsAlwaysMigrating : QAdvDatum

Equations

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

def Guerrini2026.qAdvData : List QAdvDatum

Equations

• Guerrini2026.qAdvData = [Guerrini2026.lionsUsuallyExtinct, Guerrini2026.llmsUsuallyPopular, Guerrini2026.birdsAllMigrating, Guerrini2026.birdsAlwaysMigrating]

theorem Guerrini2026.qadv_blocks_dkp : birdsAllMigrating.qAdvCompatible = true ∧ birdsAlwaysMigrating.qAdvCompatible = false

Q-adverbs (Gen counterparts) are incompatible with accidental/episodic DKP readings, confirming that DKP does not involve Gen.

theorem Guerrini2026.episodic_qadv_aligns_with_table3 : removerAvailable SentenceType.referentialDefinitePlural HomogeneityRemover.all = true ∧ removerAvailable SentenceType.referentialDefinitePlural HomogeneityRemover.always = false ∧ birdsAllMigrating.qAdvCompatible = true ∧ birdsAlwaysMigrating.qAdvCompatible = false

The Q-adverb asymmetry aligns with Table 3: episodic bare plurals (DKP parse) accept 'all' but not 'always', confirming they have DIST but not Gen in their LF.

QVE Absence as a DKP Diagnostic

@cite{guerrini-2026} §1, §3.1, §5.1: Quantificational Variability Effects (QVEs) are the hallmark of generic quantification. A sentence like "Birds rarely fly" (= QVE with 'rarely') is interpreted as "few birds fly" — the Q-adverb varies the quantificational force. QVEs arise when Gen is present, because Q-adverbs are overt counterparts of Gen.

Key fact: episodic bare plurals lack QVEs (examples (8), (90), (92)):

• "Birds are rarely migrating" ≉ "Few birds are migrating"
• "Birds are always migrating" does NOT yield episodic QVE

This absence is predicted by the DKP analysis: no Gen → no Q-adverb slot → no QVE. On the BFG analysis, QVEs would be expected but don't appear.

def Guerrini2026.supportsQVE (lf : GeneralizationLF) : Bool

Whether a given LF parse supports Quantificational Variability Effects.

QVEs arise only when Gen is present (Gen is the covert Q-adverb that overt Q-adverbs like 'usually', 'rarely' replace).

Equations

• Guerrini2026.supportsQVE Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.supportsQVE Guerrini2026.GeneralizationLF.distributiveKindPred = false
• Guerrini2026.supportsQVE Guerrini2026.GeneralizationLF.cumulativeKindPred = false
• Guerrini2026.supportsQVE Guerrini2026.GeneralizationLF.existentialDPP = false

theorem Guerrini2026.only_bfg_supports_qve : supportsQVE GeneralizationLF.bonaFideGeneric = true ∧ supportsQVE GeneralizationLF.distributiveKindPred = false ∧ supportsQVE GeneralizationLF.cumulativeKindPred = false ∧ supportsQVE GeneralizationLF.existentialDPP = false

Only BFG supports QVEs. DKP's absence of QVEs is a direct consequence of not having Gen in the LF. Examples (8), (90), (92) in the paper.

theorem Guerrini2026.qve_absence_matches_qadv_incompatibility : supportsQVE GeneralizationLF.distributiveKindPred = false ∧ subjectToGenericInference GeneralizationLF.distributiveKindPred = false ∧ lfFlavor GeneralizationLF.distributiveKindPred = GenFlavor.accidental

QVE absence aligns with Q-adverb incompatibility: both are consequences of the same structural fact (no Gen in DKP).

DPP Completes the Four-Way Typology

@cite{guerrini-2026} diagram (145) shows English bare plurals have four LF paths. Two via kind denotation (DKP, CKP), two via property denotation (BFG, DPP). The DPP path yields the existential reading of episodic bare plurals ("Bears are destroying my garden" ≈ ∃x[bear(x) ∧ destroying-my-garden(x)]), grounded via DPP from NMP.lean.

theorem Guerrini2026.existential_via_dpp : LFAvailable NominalExpression.englishBarePlural GeneralizationLF.existentialDPP ∧ LFAvailable NominalExpression.italianBarePlural GeneralizationLF.existentialDPP ∧ ¬LFAvailable NominalExpression.italianDefinitePlural GeneralizationLF.existentialDPP

DPP (from NMP.lean) is the compositional engine behind the .existentialDPP LF parse.

This theorem connects the structural LF typology to the theory-layer definition: existential readings arise exactly when property denotation is available, via DPP.

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

The four-way LF typology from diagram (145), connecting denotation types to available LFs and their truth conditions:

Kind path:

• BFG: Gen(⟦kind⟧, ⟦VP⟧) — law-like, prevalence-sensitive
• DKP: DIST(⟦VP⟧)(∩kind_{s₀}) — near-universal over actual instances
• CKP: **(⟦VP⟧)(locations)(∩kind_{s₀}) — cumulative coverage

Property path:

• BFG: Gen(⟦property⟧, ⟦VP⟧) — law-like, prevalence-sensitive
• DPP: ∃x[property(x) ∧ VP(x)] — low-scoped existential

The Role of Hab in Both LF Structures

@cite{guerrini-2026} §3.4: The VP in habitual sentences involves a habitual aspect operator Hab (formalized in Theories/Semantics/Lexical/Verb/Habituals.lean as traditionalHAB). On the "habituality is genericity" view (@cite{chierchia-1995}, @cite{chierchia-1998}), Hab IS Gen applied to situations involving a single individual. On the Dobrovie-Sorin (2001) view, Hab is a distinct operator below Gen.

Either way, the paper's structural ambiguity holds. The two LF structures (41a) and (41b)/(42b) share the same "low part" (⟦Hab VP⟧) but differ in what appears ABOVE it:

• (41a) BFG: Gen(kind, ⟦Hab VP⟧) — Gen binds the kind's world variable
• (41b) DKP: DIST(⟦Hab VP⟧)(kind_{s₀}) — kind evaluated at actual world

For episodic sentences ("Birds are migrating"), there is no Hab at all — the VP is evaluated directly at s₀. DKP still applies (DIST over kind extension), but BFG requires Hab/Gen to be present. This is why episodic bare plurals get near-universal readings without generic quantification.

inductive Guerrini2026.VPAspect : Type

VP aspect: habitual or episodic.

Habitual VPs involve the Hab operator (see Habituals.lean). Episodic VPs are evaluated directly at the world of evaluation.

• 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 (asp : VPAspect) (lf : GeneralizationLF) : Bool

Which LFs are compatible with which aspect.

BFG requires Gen, which in turn requires either Hab or an overt Q-adverb to provide the quantificational structure. In episodic sentences (no Hab, no Q-adverb), BFG is unavailable — only DKP/CKP/DPP survive.

Equations

• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.habitual lf = true
• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.episodic Guerrini2026.GeneralizationLF.bonaFideGeneric = false
• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.episodic Guerrini2026.GeneralizationLF.distributiveKindPred = true
• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.episodic Guerrini2026.GeneralizationLF.cumulativeKindPred = true
• Guerrini2026.lfCompatibleWithAspect Guerrini2026.VPAspect.episodic Guerrini2026.GeneralizationLF.existentialDPP = true

theorem Guerrini2026.episodic_no_bfg : lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.bonaFideGeneric = false ∧ lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.distributiveKindPred = true ∧ lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.cumulativeKindPred = true ∧ lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.existentialDPP = true

In episodic sentences, BFG is unavailable — only DKP/CKP/DPP.

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

This explains the episodic asymmetry (§5):

• Bare plurals in episodics: DKP available → near-universal ✓
• Singular indefinites in episodics: no DKP, no BFG (episodic) → only ∃

The singular indefinite chain goes through ∩ being undefined for singular count nouns (downDefinedFor), NOT through the Italian bare plural's [-arg] parameter (which is a different mechanism).

Singular Kinds Cannot Support Accidental or Cumulative Readings

@cite{guerrini-2026} §6.2: Singular kind terms ("the dodo", "the madrigal") differ strikingly from plural kind terms ("dodos", "madrigals"):

1. Kind predication OK for both ("The dodo is extinct" / "Dodos are extinct")
2. Genericity + QVE OK for singular kinds ("The lion rarely has a mane")
3. Accidental readings unavailable for singular kinds
4. Cumulative readings unavailable for singular kinds

This follows from treating singular kinds as atomic (following @cite{barker-1992}, @cite{schwarzschild-1996}, @cite{dayal-2004}). DIST does not apply to atoms (only to pluralities), so DKP is unavailable. The cumulative operator ** similarly requires pluralities.

inductive Guerrini2026.KindTermNumber : Type

Number of a kind-denoting term.

• singular : KindTermNumber
• plural : KindTermNumber

@[implicit_reducible]

instance Guerrini2026.instDecidableEqKindTermNumber : DecidableEq KindTermNumber

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprKindTermNumber : Repr KindTermNumber

Equations

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

def Guerrini2026.instReprKindTermNumber.repr : KindTermNumber → ℕ → Std.Format

Equations

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

def Guerrini2026.singularKindLFAvailable (lf : GeneralizationLF) : Bool

Singular kind terms are atomic — DIST and ** do not apply. Only BFG is available (kind enters Gen restrictor).

Equations

• Guerrini2026.singularKindLFAvailable Guerrini2026.GeneralizationLF.bonaFideGeneric = true
• Guerrini2026.singularKindLFAvailable Guerrini2026.GeneralizationLF.distributiveKindPred = false
• Guerrini2026.singularKindLFAvailable Guerrini2026.GeneralizationLF.cumulativeKindPred = false
• Guerrini2026.singularKindLFAvailable Guerrini2026.GeneralizationLF.existentialDPP = false

theorem Guerrini2026.singular_kind_law_like_only : singularKindLFAvailable GeneralizationLF.bonaFideGeneric = true ∧ singularKindLFAvailable GeneralizationLF.distributiveKindPred = false ∧ singularKindLFAvailable GeneralizationLF.cumulativeKindPred = false ∧ singularKindLFAvailable GeneralizationLF.existentialDPP = false

Singular kind terms support only law-like readings.

structure Guerrini2026.SingularKindDivergenceDatum : Type

Singular kind divergence datum from §6.2, examples (133)–(136).

• sentence : String
• kindTermNumber : KindTermNumber
• accidentalOK : Bool
• cumulativeOK : Bool
• notes : String

def Guerrini2026.madrigalPopularSg : SingularKindDivergenceDatum

Equations

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

def Guerrini2026.madrigalPopularPl : SingularKindDivergenceDatum

Equations

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

def Guerrini2026.wugColorsSg : SingularKindDivergenceDatum

Equations

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

def Guerrini2026.wugColorsPl : SingularKindDivergenceDatum

Equations

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

def Guerrini2026.singularKindDivergenceData : List SingularKindDivergenceDatum

Equations

• Guerrini2026.singularKindDivergenceData = [Guerrini2026.madrigalPopularSg, Guerrini2026.madrigalPopularPl, Guerrini2026.wugColorsSg, Guerrini2026.wugColorsPl]

theorem Guerrini2026.singular_plural_divergence : ((List.filter (fun (x : SingularKindDivergenceDatum) => x.kindTermNumber == KindTermNumber.singular) singularKindDivergenceData).all fun (x : SingularKindDivergenceDatum) => !x.accidentalOK) = true ∧ ((List.filter (fun (x : SingularKindDivergenceDatum) => x.kindTermNumber == KindTermNumber.singular) singularKindDivergenceData).all fun (x : SingularKindDivergenceDatum) => !x.cumulativeOK) = true ∧ ((List.filter (fun (x : SingularKindDivergenceDatum) => x.kindTermNumber == KindTermNumber.plural) singularKindDivergenceData).all fun (x : SingularKindDivergenceDatum) => x.accidentalOK) = true

Singular kind terms lack accidental and cumulative readings; plural kind terms support both.

Greenberg (2002, 2004, 2007): Further Evidence for DKP

@cite{guerrini-2026} §3.7: @cite{greenberg-2002} @cite{greenberg-2004} @cite{greenberg-2007} presented data teasing apart bare plurals from singular indefinites in accidentally-flavored generalizations.

Temporally modified sentences (@cite{greenberg-2004}): "Italian restaurants are closed today" can be true accidentally (national holiday). The singular "An Italian restaurant is closed today" requires a law-like link.

"Extremely unnatural kinds" (@cite{greenberg-2007}): "Norwegian students with names ending in 's' wear thick green socks" — true via DKP (actual students happen to), but the singular is infelicitous (no law-like link).

structure Guerrini2026.GreenbergDatum : Type

Greenberg datum from @cite{guerrini-2026} §3.7.

• sentence : String
• nominalForm : NominalForm
• accidentalOK : Bool
• lawLikeOK : Bool
• notes : String

def Guerrini2026.italianRestaurantsPl : GreenbergDatum

Equations

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

def Guerrini2026.italianRestaurantSg : GreenbergDatum

Equations

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

def Guerrini2026.norwegianStudentsPl : GreenbergDatum

Equations

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

def Guerrini2026.norwegianStudentSg : GreenbergDatum

Equations

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

def Guerrini2026.greenbergData : List GreenbergDatum

Equations

• Guerrini2026.greenbergData = [Guerrini2026.italianRestaurantsPl, Guerrini2026.italianRestaurantSg, Guerrini2026.norwegianStudentsPl, Guerrini2026.norwegianStudentSg]

theorem Guerrini2026.greenberg_accidental_asymmetry : ((List.filter (fun (x : GreenbergDatum) => x.nominalForm == NominalForm.kindDenotingPlural) greenbergData).all fun (x : GreenbergDatum) => x.accidentalOK) = true ∧ ((List.filter (fun (x : GreenbergDatum) => x.nominalForm == NominalForm.singularIndefinite) greenbergData).all fun (x : GreenbergDatum) => !x.accidentalOK) = true

Bare plurals support accidental readings; singular indefinites do not.

Homogeneity in Episodic Bare Plurals

@cite{guerrini-2026} §5.1: Near-universal episodic readings ("Birds are migrating") arise from DKP — DIST over the kind extension at s₀. Since there is no Gen in this LF:

• 'all' removes homogeneity (targets DIST): "Birds are all migrating" ✓
• 'always' does NOT apply (no Gen to target): "#Birds are always migrating" forces a habitual/generic reparse, not an episodic reading.

This is a direct consequence of Table 3 (§4): episodic DKP has DIST-homogeneity but no Gen-homogeneity.

structure Guerrini2026.EpisodicHomogeneityDatum : Type

Episodic homogeneity removal datum.

• sentence : String
• remover : HomogeneityRemover
• episodicOK : Bool
• notes : String

def Guerrini2026.birdsAllMigratingEp : EpisodicHomogeneityDatum

Equations

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

def Guerrini2026.birdsAlwaysMigratingEp : EpisodicHomogeneityDatum

Equations

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

def Guerrini2026.studentsAllScaredEp : EpisodicHomogeneityDatum

Equations

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

def Guerrini2026.studentsAlwaysScaredEp : EpisodicHomogeneityDatum

Equations

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

def Guerrini2026.episodicHomogeneityData : List EpisodicHomogeneityDatum

Equations

• Guerrini2026.episodicHomogeneityData = [Guerrini2026.birdsAllMigratingEp, Guerrini2026.birdsAlwaysMigratingEp, Guerrini2026.studentsAllScaredEp, Guerrini2026.studentsAlwaysScaredEp]

theorem Guerrini2026.episodic_all_not_always : ((List.filter (fun (x : EpisodicHomogeneityDatum) => x.remover == HomogeneityRemover.all) episodicHomogeneityData).all fun (x : EpisodicHomogeneityDatum) => x.episodicOK) = true ∧ ((List.filter (fun (x : EpisodicHomogeneityDatum) => x.remover == HomogeneityRemover.always) episodicHomogeneityData).all fun (x : EpisodicHomogeneityDatum) => !x.episodicOK) = true

In episodic DKP, 'all' preserves the episodic reading but 'always' forces a generic reparse. DIST but no Gen → only 'all' applies.

theorem Guerrini2026.episodic_homogeneity_from_table3 : hasHomogeneitySource SentenceType.referentialDefinitePlural HomogeneitySource.dist = true ∧ hasHomogeneitySource SentenceType.referentialDefinitePlural HomogeneitySource.gen = false ∧ removesHomogeneity HomogeneityRemover.all HomogeneitySource.dist = true ∧ removesHomogeneity HomogeneityRemover.always HomogeneitySource.dist = false

Derives from Table 3: episodic DKP has DIST-homogeneity (removable by 'all') but no Gen-homogeneity ('always' vacuous).

DKP Inherits Homogeneity and Non-Maximality from DIST

@cite{guerrini-2026} §5.1, §6.1: The near-universal reading from Distributive Kind Predication is homogeneous and non-maximal, just like referential definite plurals. This follows directly from DKP being compositionally DIST applied to the kind extension — the trivalent truth conditions are inherited, not stipulated.

This connects to the theory-neutral homogeneity data in Phenomena/Plurals/Homogeneity.lean (@cite{kriz-2015} @cite{kriz-spector-2021}) and non-maximality data in Phenomena/Plurals/NonMaximality.lean.

The paper's examples (88)–(90) make this explicit:

• "Birds are migrating" — possibly non-maximal, ∼ ∀ (DKP + homogeneity)
• "Birds are not migrating" — possibly non-maximal, ∼ ¬∃ (negated homogeneity)
• "Birds are all migrating" — maximal, ∼ ∀ ('all' removes DIST homogeneity)
• "#Birds are always migrating" — forces generic reparse (Gen absent)

These are exactly the predictions of distributiveKindPredTV (§2) inheriting pluralTruthValue from Distributivity.lean.

theorem Guerrini2026.dkp_homogeneity_from_dist {Atom W : Type} [DecidableEq Atom] [Fintype Atom] (kindExtension : W → Finset Atom) (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (s₀ : W) : distributiveKindPredTV kindExtension P s₀ = Semantics.Plurality.Distributivity.pluralTruthValue P (kindExtension s₀) s₀

DKP truth value is computed via DIST (pluralTruthValue), so it inherits the homogeneity gap from referential definite plurals.

This is the formal bridge between Guerrini's analysis and the Križ & Spector homogeneity theory: the same trivalent operator that gives definite plurals their characteristic behavior also gives kind-denoting plurals their non-maximal, exception-tolerant readings. The parallel is not stipulated — it's structural.

Compositional Trees: Two LF Parses Evaluated End-to-End

@cite{guerrini-2026} structures (29), (30), (105b)

Demonstrates that the BFG and DKP parses of "Lions hunt" can be represented as Tree Unit String values and evaluated via the existing interp machinery, with covert operators (Gen, DIST, DPP) as lexicon entries.

The scenario

Three lions: Simba (hunts), Nala (hunts), Mufasa (doesn't hunt).

• BFG parse: Gen(lion, hunt) — "generally, lions hunt" → true (2 out of 3 lions hunt; the generic quantifier tolerates exceptions)
• DKP parse: DIST(hunt)(∩lions_{s₀}) — "all actual lions hunt" → false (Mufasa doesn't hunt; DIST requires universality)
• DPP parse: DPP(lion, hunt) — "some lion hunts" → true (existential; at least one lion hunts)

This demonstrates the core of @cite{guerrini-2026}: the same surface sentence "Lions hunt" has two structurally distinct LFs that can disagree in truth value.

inductive Guerrini2026.DemoEntity : Type

Demo entity domain: three individual lions plus the lion-kind (the maximal sum ∩lions_{s₀}, treated as a fourth entity).

• simba : DemoEntity
• nala : DemoEntity
• mufasa : DemoEntity
• lionKind : DemoEntity

@[implicit_reducible]

instance Guerrini2026.instDecidableEqDemoEntity : DecidableEq DemoEntity

Equations

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

def Guerrini2026.instReprDemoEntity.repr : DemoEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Guerrini2026.instReprDemoEntity : Repr DemoEntity

Equations

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

@[implicit_reducible]

instance Guerrini2026.instBEqDemoEntity : BEq DemoEntity

Equations

• Guerrini2026.instBEqDemoEntity = { beq := fun (a b : Guerrini2026.DemoEntity) => decide (a = b) }

theorem Guerrini2026.three_parses_disagree : 3 * [DemoEntity.simba, DemoEntity.nala].length ≥ 2 * [DemoEntity.simba, DemoEntity.nala, DemoEntity.mufasa].length ∧ (¬∀ a ∈ Guerrini2026.atomsOf✝ DemoEntity.lionKind, Guerrini2026.huntPred✝ a) ∧ ∃ x ∈ Guerrini2026.demoAtoms✝, Guerrini2026.lionPred✝ x ∧ Guerrini2026.huntPred✝ x

The three parses disagree: same surface sentence, different truth values.

BFG: true — Gen tolerates exceptions (2/3 lions hunt) DKP: false — DIST requires all atoms (Mufasa doesn't hunt) DPP: true — ∃ requires at least one (Simba hunts)

Proved directly from the semantic operators rather than through tree evaluation (which requires noncomputable Decidable instances).

theorem Guerrini2026.all_hunt_agreement : 3 * [DemoEntity.simba, DemoEntity.nala, DemoEntity.mufasa].length ≥ 2 * [DemoEntity.simba, DemoEntity.nala, DemoEntity.mufasa].length ∧ ∀ a ∈ Guerrini2026.atomsOf✝ DemoEntity.lionKind, Guerrini2026.huntAllPred✝ a

When all lions hunt, BFG and DKP agree: both true.