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 Phenomena.Generics.Studies.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))

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqGeneralizationLF : DecidableEq GeneralizationLF

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprGeneralizationLF : Repr GeneralizationLF

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprGeneralizationLF = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprGeneralizationLF.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprGeneralizationLF.repr : GeneralizationLF → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instBEqGeneralizationLF : BEq GeneralizationLF

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqGeneralizationLF = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqGeneralizationLF.beq }

def Phenomena.Generics.Studies.Guerrini2026.instBEqGeneralizationLF.beq : GeneralizationLF → GeneralizationLF → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqGeneralizationLF.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

noncomputable def Phenomena.Generics.Studies.Guerrini2026.kindExtensionFinset {Atom W : Type} [Fintype Atom] (k : Semantics.Lexical.Noun.Kind.Chierchia1998.Kind W Atom) (w : W) : Finset Atom

Extract a kind's extension at a world as a Finset, bridging Chierchia1998'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

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

def Phenomena.Generics.Studies.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

• Phenomena.Generics.Studies.Guerrini2026.kindExtensionOfBool member w = {w_1 : Atom | member w w_1 = true}

def Phenomena.Generics.Studies.Guerrini2026.distributiveKindPred {Atom W : Type} (kindExtension : W → Finset Atom) (P : Atom → W → Bool) (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 Chierchia1998.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

• Phenomena.Generics.Studies.Guerrini2026.distributiveKindPred kindExtension P s₀ = Semantics.Lexical.Plural.Distributivity.distMaximal P (kindExtension s₀) s₀

def Phenomena.Generics.Studies.Guerrini2026.distributiveKindPredTV {Atom W : Type} (kindExtension : W → Finset Atom) (P : Atom → W → Bool) (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

• Phenomena.Generics.Studies.Guerrini2026.distributiveKindPredTV kindExtension P s₀ = Semantics.Lexical.Plural.Distributivity.pluralTruthValue P (kindExtension s₀) s₀

noncomputable def Phenomena.Generics.Studies.Guerrini2026.distributiveKindPredOfKind {Atom W : Type} [Fintype Atom] (k : Semantics.Lexical.Noun.Kind.Chierchia1998.Kind W Atom) (P : Atom → W → Bool) (s₀ : W) : Bool

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

Equations

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

inductive Phenomena.Generics.Studies.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

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqGenFlavor : DecidableEq GenFlavor

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprGenFlavor : Repr GenFlavor

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprGenFlavor = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprGenFlavor.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprGenFlavor.repr : GenFlavor → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instBEqGenFlavor : BEq GenFlavor

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqGenFlavor = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqGenFlavor.beq }

def Phenomena.Generics.Studies.Guerrini2026.instBEqGenFlavor.beq : GenFlavor → GenFlavor → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqGenFlavor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Phenomena.Generics.Studies.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"

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqNominalForm : DecidableEq NominalForm

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instReprNominalForm.repr : NominalForm → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprNominalForm : Repr NominalForm

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprNominalForm = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprNominalForm.repr }

def Phenomena.Generics.Studies.Guerrini2026.instBEqNominalForm.beq : NominalForm → NominalForm → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqNominalForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqNominalForm : BEq NominalForm

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqNominalForm = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqNominalForm.beq }

def Phenomena.Generics.Studies.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

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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

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

theorem Phenomena.Generics.Studies.Guerrini2026.singular_no_accidental : Semantics.Lexical.Noun.Kind.Chierchia1998.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 Phenomena.Generics.Studies.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

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqHomogeneitySource : DecidableEq HomogeneitySource

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneitySource : Repr HomogeneitySource

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneitySource = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneitySource.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneitySource.repr : HomogeneitySource → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneitySource.beq : HomogeneitySource → HomogeneitySource → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneitySource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneitySource : BEq HomogeneitySource

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneitySource = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneitySource.beq }

inductive Phenomena.Generics.Studies.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 ∀

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqHomogeneityRemover : DecidableEq HomogeneityRemover

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneityRemover.repr : HomogeneityRemover → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneityRemover : Repr HomogeneityRemover

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneityRemover = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprHomogeneityRemover.repr }

def Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneityRemover.beq : HomogeneityRemover → HomogeneityRemover → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneityRemover.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneityRemover : BEq HomogeneityRemover

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneityRemover = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqHomogeneityRemover.beq }

def Phenomena.Generics.Studies.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

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

inductive Phenomena.Generics.Studies.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"

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqSentenceType : DecidableEq SentenceType

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprSentenceType : Repr SentenceType

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprSentenceType = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprSentenceType.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprSentenceType.repr : SentenceType → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instBEqSentenceType : BEq SentenceType

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqSentenceType = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqSentenceType.beq }

def Phenomena.Generics.Studies.Guerrini2026.instBEqSentenceType.beq : SentenceType → SentenceType → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqSentenceType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Generics.Studies.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

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

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

Which removers are available for each sentence type.

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.NominalExpression : Type

Cross-linguistic nominal form.

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

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqNominalExpression : DecidableEq NominalExpression

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprNominalExpression : Repr NominalExpression

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprNominalExpression = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprNominalExpression.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprNominalExpression.repr : NominalExpression → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instBEqNominalExpression.beq : NominalExpression → NominalExpression → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqNominalExpression.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqNominalExpression : BEq NominalExpression

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqNominalExpression = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqNominalExpression.beq }

def Phenomena.Generics.Studies.Guerrini2026.nominalMapping : NominalExpression → Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping

The Nominal Mapping Parameter for each nominal expression.

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.hasD : NominalExpression → Bool

Whether an overt determiner (D) is present.

Equations

• Phenomena.Generics.Studies.Guerrini2026.hasD Phenomena.Generics.Studies.Guerrini2026.NominalExpression.englishBarePlural = false
• Phenomena.Generics.Studies.Guerrini2026.hasD Phenomena.Generics.Studies.Guerrini2026.NominalExpression.italianDefinitePlural = true
• Phenomena.Generics.Studies.Guerrini2026.hasD Phenomena.Generics.Studies.Guerrini2026.NominalExpression.italianBarePlural = false

def Phenomena.Generics.Studies.Guerrini2026.canDenote (ne : NominalExpression) (nd : KindReference.NominalDenotation) : Bool

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.

theorem Phenomena.Generics.Studies.Guerrini2026.english_bp_ambiguous : canDenote NominalExpression.englishBarePlural KindReference.NominalDenotation.kind = true ∧ canDenote NominalExpression.englishBarePlural KindReference.NominalDenotation.property = true

English bare plurals are ambiguous.

theorem Phenomena.Generics.Studies.Guerrini2026.italian_def_pl_kind_only : canDenote NominalExpression.italianDefinitePlural KindReference.NominalDenotation.kind = true ∧ canDenote NominalExpression.italianDefinitePlural KindReference.NominalDenotation.property = false

Italian definite plurals unambiguously denote kinds.

theorem Phenomena.Generics.Studies.Guerrini2026.italian_bare_pl_property_only : canDenote NominalExpression.italianBarePlural KindReference.NominalDenotation.kind = false ∧ canDenote NominalExpression.italianBarePlural KindReference.NominalDenotation.property = true

Italian bare plurals unambiguously denote properties.

def Phenomena.Generics.Studies.Guerrini2026.lfAvailable (ne : NominalExpression) (lf : GeneralizationLF) : Bool

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

• One or more equations did not get rendered due to their size.
• Phenomena.Generics.Studies.Guerrini2026.lfAvailable ne Phenomena.Generics.Studies.Guerrini2026.GeneralizationLF.bonaFideGeneric = true

theorem Phenomena.Generics.Studies.Guerrini2026.english_bp_all_lfs : lfAvailable NominalExpression.englishBarePlural GeneralizationLF.bonaFideGeneric = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.distributiveKindPred = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.cumulativeKindPred = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.existentialDPP = true

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

theorem Phenomena.Generics.Studies.Guerrini2026.italian_def_pl_lfs : lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.bonaFideGeneric = true ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.distributiveKindPred = true ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.cumulativeKindPred = true ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.existentialDPP = false

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

theorem Phenomena.Generics.Studies.Guerrini2026.italian_bare_pl_lfs : lfAvailable NominalExpression.italianBarePlural GeneralizationLF.bonaFideGeneric = true ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.cumulativeKindPred = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.existentialDPP = true

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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.birdsMigrating : EpisodicDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.aBirdMigrating : EpisodicDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.studentsScarred : EpisodicDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.aStudentScared : EpisodicDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.episodicData : List EpisodicDatum

Equations

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

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 Phenomena.Generics.Studies.Guerrini2026.ItalianEpisodicDatum : Type

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

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

def Phenomena.Generics.Studies.Guerrini2026.itDefPlJournalists : ItalianEpisodicDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.itBarePlJournalists : ItalianEpisodicDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.italianEpisodicData : List ItalianEpisodicDatum

Equations

• Phenomena.Generics.Studies.Guerrini2026.italianEpisodicData = [Phenomena.Generics.Studies.Guerrini2026.itDefPlJournalists, Phenomena.Generics.Studies.Guerrini2026.itBarePlJournalists]

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.itDefPlCandidates : ItalianGenDisambiguationDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.itBarePlCandidates : ItalianGenDisambiguationDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.italianGenDisambiguationData : List ItalianGenDisambiguationDatum

Equations

• Phenomena.Generics.Studies.Guerrini2026.italianGenDisambiguationData = [Phenomena.Generics.Studies.Guerrini2026.itDefPlCandidates, Phenomena.Generics.Studies.Guerrini2026.itBarePlCandidates]

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.italian_disambiguation_from_kind_denotation : canDenote NominalExpression.italianDefinitePlural KindReference.NominalDenotation.kind = true ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.distributiveKindPred = true ∧ canDenote NominalExpression.italianBarePlural KindReference.NominalDenotation.kind = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred = false ∧ canDenote NominalExpression.italianBarePlural KindReference.NominalDenotation.property = true

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 Phenomena.Generics.Studies.Guerrini2026.subjectToGenericInference (lf : GeneralizationLF) : Bool

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

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.prevalenceAtWorld {Atom W : Type} (P : Atom → W → Bool) (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

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

theorem Phenomena.Generics.Studies.Guerrini2026.dkp_true_iff_prevalence_one {Atom W : Type} (P : Atom → W → Bool) (ext : Finset Atom) (w : W) (hne : ext.Nonempty) : Semantics.Lexical.Plural.Distributivity.distMaximal P ext w = true ↔ 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 Phenomena.Generics.Studies.Guerrini2026.dkp_false_iff_prevalence_zero {Atom W : Type} (P : Atom → W → Bool) (ext : Finset Atom) (w : W) : Semantics.Lexical.Plural.Distributivity.noneSatisfy P ext w = true ↔ prevalenceAtWorld P ext w = 0

DKP trivalent-false ↔ prevalence = 0.

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.parses_can_disagree : ∃ (P : Fin 10 → Fin 1 → Bool) (ext : Finset (Fin 10)), ext.Nonempty ∧ Semantics.Lexical.Plural.Distributivity.allSatisfy P ext 0 = false ∧ Semantics.Lexical.Plural.Distributivity.noneSatisfy P ext 0 = false ∧ 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 Phenomena.Generics.Studies.Guerrini2026.ItalianMood : Type

Italian mood in relative clause modifying the subject DP.

• indicative : ItalianMood
• subjunctive : ItalianMood

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqItalianMood : DecidableEq ItalianMood

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprItalianMood : Repr ItalianMood

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprItalianMood = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprItalianMood.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprItalianMood.repr : ItalianMood → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instBEqItalianMood.beq : ItalianMood → ItalianMood → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqItalianMood.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqItalianMood : BEq ItalianMood

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqItalianMood = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqItalianMood.beq }

def Phenomena.Generics.Studies.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

• Phenomena.Generics.Studies.Guerrini2026.subjunctiveForcesLawLike Phenomena.Generics.Studies.Guerrini2026.ItalianMood.indicative = false
• Phenomena.Generics.Studies.Guerrini2026.subjunctiveForcesLawLike Phenomena.Generics.Studies.Guerrini2026.ItalianMood.subjunctive = true

def Phenomena.Generics.Studies.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

• One or more equations did not get rendered due to their size.
• Phenomena.Generics.Studies.Guerrini2026.lfAvailableWithMood Phenomena.Generics.Studies.Guerrini2026.ItalianMood.indicative lf = true

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.GenericityDatum : Type

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

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

def Phenomena.Generics.Studies.Guerrini2026.llmsUtilizeDL : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.aLLMUtilizesDL : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.llmsArePopular : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.aLLMIsPopular : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.gliLLMUsanoDL : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.unLLMUsaDL : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.gliLLMSonoPopolari : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.unLLMEPopolari : GenericityDatum

Equations

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

def Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.evalBFG (situations : List Semantics.Lexical.Noun.Kind.Generics.Situation) (normal : Semantics.Lexical.Noun.Kind.Generics.NormalcyPredicate) (kindRestrictor : Semantics.Lexical.Noun.Kind.Generics.Restrictor) (predScope : Semantics.Lexical.Noun.Kind.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

• Phenomena.Generics.Studies.Guerrini2026.evalBFG situations normal kindRestrictor predScope = Semantics.Lexical.Noun.Kind.Generics.traditionalGEN situations normal kindRestrictor predScope

theorem Phenomena.Generics.Studies.Guerrini2026.table1_from_lf_structure : (∃ (lf : GeneralizationLF), lfAvailable NominalExpression.englishBarePlural lf = true ∧ lfFlavor lf = GenFlavor.lawLike) ∧ (∃ (lf : GeneralizationLF), lfAvailable NominalExpression.englishBarePlural lf = true ∧ lfFlavor lf = GenFlavor.accidental) ∧ lfFlavor GeneralizationLF.bonaFideGeneric = GenFlavor.lawLike ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.cumulativeKindPred = false

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 Phenomena.Generics.Studies.Guerrini2026.referential_iff_longobardi_kind : Reference.Studies.Longobardi2001.bnCanBeReferential Reference.Studies.Longobardi2001.english = canDenote NominalExpression.englishBarePlural KindReference.NominalDenotation.kind ∧ Reference.Studies.Longobardi2001.bnCanBeReferential Reference.Studies.Longobardi2001.romance = canDenote NominalExpression.italianBarePlural 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 Phenomena.Generics.Studies.Guerrini2026.quantificational_only_iff_bfg_only : lfAvailable NominalExpression.englishBarePlural GeneralizationLF.distributiveKindPred = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.cumulativeKindPred = true ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.cumulativeKindPred = false

@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 Phenomena.Generics.Studies.Guerrini2026.strongd_to_table1 : Reference.Studies.Longobardi2001.romance.strongD = true ∧ Reference.Studies.Longobardi2001.toNominalMapping Reference.Studies.Longobardi2001.romance = Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.predOnly ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.canDenoteKind Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.predOnly false = false ∧ canDenote NominalExpression.italianBarePlural KindReference.NominalDenotation.kind = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred = false ∧ 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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.cumulativeKindPred {Atom Loc : Type} (R : Atom → Loc → Bool) (kindExtension : Finset Atom) (locations : Finset Loc) : Bool

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

• Phenomena.Generics.Studies.Guerrini2026.cumulativeKindPred R kindExtension locations = Semantics.Lexical.Plural.Cumulativity.cumulativeOp 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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.wugsColors : CumulativityDiagnosticDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.wugsQAdvColors : CumulativityDiagnosticDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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.

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqAdjReading : DecidableEq AdjReading

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprAdjReading : Repr AdjReading

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprAdjReading = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprAdjReading.repr }

def Phenomena.Generics.Studies.Guerrini2026.instReprAdjReading.repr : AdjReading → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instBEqAdjReading.beq : AdjReading → AdjReading → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqAdjReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqAdjReading : BEq AdjReading

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqAdjReading = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqAdjReading.beq }

def Phenomena.Generics.Studies.Guerrini2026.adjReadingSupportsKind : AdjReading → Bool

Kind predication is available only with local adjective readings.

Equations

• Phenomena.Generics.Studies.Guerrini2026.adjReadingSupportsKind Phenomena.Generics.Studies.Guerrini2026.AdjReading.local = true
• Phenomena.Generics.Studies.Guerrini2026.adjReadingSupportsKind Phenomena.Generics.Studies.Guerrini2026.AdjReading.nonlocal = false

structure Phenomena.Generics.Studies.Guerrini2026.EpistemicAdjDatum : Type

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

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

def Phenomena.Generics.Studies.Guerrini2026.americanVoters : EpistemicAdjDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.unidentifiedVoters : EpistemicAdjDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.investigativeJournalists : EpistemicAdjDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.unknownJournalists : EpistemicAdjDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.epistemicAdjData : List EpistemicAdjDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.lionsUsuallyExtinct : QAdvDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.llmsUsuallyPopular : QAdvDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.birdsAllMigrating : QAdvDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.birdsAlwaysMigrating : QAdvDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.qAdvData : List QAdvDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Chierchia1998.lean.

theorem Phenomena.Generics.Studies.Guerrini2026.existential_via_dpp : lfAvailable NominalExpression.englishBarePlural GeneralizationLF.existentialDPP = true ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.existentialDPP = true ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.existentialDPP = false

DPP (from Chierchia1998.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 Phenomena.Generics.Studies.Guerrini2026.diagram_145_four_paths : lfAvailable NominalExpression.englishBarePlural GeneralizationLF.distributiveKindPred = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.cumulativeKindPred = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.existentialDPP = true ∧ lfAvailable NominalExpression.englishBarePlural GeneralizationLF.bonaFideGeneric = true ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.existentialDPP = false ∧ lfAvailable NominalExpression.italianDefinitePlural GeneralizationLF.distributiveKindPred = true ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.distributiveKindPred = false ∧ lfAvailable NominalExpression.italianBarePlural GeneralizationLF.existentialDPP = true

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 Phenomena.Generics.Studies.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

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqVPAspect : DecidableEq VPAspect

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instReprVPAspect.repr : VPAspect → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprVPAspect : Repr VPAspect

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprVPAspect = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprVPAspect.repr }

def Phenomena.Generics.Studies.Guerrini2026.instBEqVPAspect.beq : VPAspect → VPAspect → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqVPAspect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Guerrini2026.instBEqVPAspect : BEq VPAspect

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqVPAspect = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqVPAspect.beq }

def Phenomena.Generics.Studies.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

• One or more equations did not get rendered due to their size.
• Phenomena.Generics.Studies.Guerrini2026.lfCompatibleWithAspect Phenomena.Generics.Studies.Guerrini2026.VPAspect.habitual lf = true

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.episodic_kind_plural_advantage : lfCompatibleWithAspect VPAspect.episodic GeneralizationLF.distributiveKindPred = true ∧ canDenote NominalExpression.englishBarePlural KindReference.NominalDenotation.kind = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.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 Phenomena.Generics.Studies.Guerrini2026.KindTermNumber : Type

Number of a kind-denoting term.

• singular : KindTermNumber
• plural : KindTermNumber

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqKindTermNumber : DecidableEq KindTermNumber

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instReprKindTermNumber.repr : KindTermNumber → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprKindTermNumber : Repr KindTermNumber

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprKindTermNumber = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprKindTermNumber.repr }

instance Phenomena.Generics.Studies.Guerrini2026.instBEqKindTermNumber : BEq KindTermNumber

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqKindTermNumber = { beq := Phenomena.Generics.Studies.Guerrini2026.instBEqKindTermNumber.beq }

def Phenomena.Generics.Studies.Guerrini2026.instBEqKindTermNumber.beq : KindTermNumber → KindTermNumber → Bool

Equations

• Phenomena.Generics.Studies.Guerrini2026.instBEqKindTermNumber.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Generics.Studies.Guerrini2026.singularKindLFAvailable (lf : GeneralizationLF) : Bool

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

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.SingularKindDivergenceDatum : Type

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

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

def Phenomena.Generics.Studies.Guerrini2026.madrigalPopularSg : SingularKindDivergenceDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.madrigalPopularPl : SingularKindDivergenceDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.wugColorsSg : SingularKindDivergenceDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.wugColorsPl : SingularKindDivergenceDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.singularKindDivergenceData : List SingularKindDivergenceDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.GreenbergDatum : Type

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

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

def Phenomena.Generics.Studies.Guerrini2026.italianRestaurantsPl : GreenbergDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.italianRestaurantSg : GreenbergDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.norwegianStudentsPl : GreenbergDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.norwegianStudentSg : GreenbergDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.greenbergData : List GreenbergDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.EpisodicHomogeneityDatum : Type

Episodic homogeneity removal datum.

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

def Phenomena.Generics.Studies.Guerrini2026.birdsAllMigratingEp : EpisodicHomogeneityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.birdsAlwaysMigratingEp : EpisodicHomogeneityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.studentsAllScaredEp : EpisodicHomogeneityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.studentsAlwaysScaredEp : EpisodicHomogeneityDatum

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.episodicHomogeneityData : List EpisodicHomogeneityDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Guerrini2026.dkp_homogeneity_from_dist {Atom W : Type} [DecidableEq Atom] [Fintype Atom] (kindExtension : W → Finset Atom) (P : Atom → W → Bool) (s₀ : W) : distributiveKindPredTV kindExtension P s₀ = Semantics.Lexical.Plural.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 Phenomena.Generics.Studies.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

instance Phenomena.Generics.Studies.Guerrini2026.instDecidableEqDemoEntity : DecidableEq DemoEntity

Equations

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

def Phenomena.Generics.Studies.Guerrini2026.instReprDemoEntity.repr : DemoEntity → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Guerrini2026.instReprDemoEntity : Repr DemoEntity

Equations

• Phenomena.Generics.Studies.Guerrini2026.instReprDemoEntity = { reprPrec := Phenomena.Generics.Studies.Guerrini2026.instReprDemoEntity.repr }

instance Phenomena.Generics.Studies.Guerrini2026.instBEqDemoEntity : BEq DemoEntity

Equations

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

theorem Phenomena.Generics.Studies.Guerrini2026.three_parses_disagree : Semantics.Composition.Tree.evalTree Phenomena.Generics.Studies.Guerrini2026.guerriniLex✝ Phenomena.Generics.Studies.Guerrini2026.g₀✝ Phenomena.Generics.Studies.Guerrini2026.bfgTree✝ = some true ∧ Semantics.Composition.Tree.evalTree Phenomena.Generics.Studies.Guerrini2026.guerriniLex✝¹ Phenomena.Generics.Studies.Guerrini2026.g₀✝¹ Phenomena.Generics.Studies.Guerrini2026.dkpTree✝ = some false ∧ Semantics.Composition.Tree.evalTree Phenomena.Generics.Studies.Guerrini2026.guerriniLex✝² Phenomena.Generics.Studies.Guerrini2026.g₀✝² Phenomena.Generics.Studies.Guerrini2026.dppTree✝ = some true

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)

theorem Phenomena.Generics.Studies.Guerrini2026.all_hunt_agreement : have lexAll := fun (s : String) => match s with | "lion" => some { ty := Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := fun (x : Phenomena.Generics.Studies.Guerrini2026.demoModel✝.interpTy Semantics.Montague.Ty.e) => match x with | DemoEntity.simba => true | DemoEntity.nala => true | DemoEntity.mufasa => true | DemoEntity.lionKind => false } | "hunt" => some { ty := Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := fun (x : Phenomena.Generics.Studies.Guerrini2026.demoModel✝¹.interpTy Semantics.Montague.Ty.e) => match x with | DemoEntity.simba => true | DemoEntity.nala => true | DemoEntity.mufasa => true | DemoEntity.lionKind => false } | "∩lions" => some { ty := Semantics.Montague.Ty.e, denot := DemoEntity.lionKind } | "Gen" => some (Semantics.Lexical.CovertQuantifier.genThreshold Phenomena.Generics.Studies.Guerrini2026.demoModel✝² Phenomena.Generics.Studies.Guerrini2026.demoAtoms✝ 2 3) | "DIST" => some (Semantics.Lexical.CovertQuantifier.dist Phenomena.Generics.Studies.Guerrini2026.demoModel✝³ Phenomena.Generics.Studies.Guerrini2026.atomsOf✝) | x => none; Semantics.Composition.Tree.evalTree lexAll Phenomena.Generics.Studies.Guerrini2026.g₀✝ Phenomena.Generics.Studies.Guerrini2026.bfgTree✝ = some true ∧ Semantics.Composition.Tree.evalTree lexAll Phenomena.Generics.Studies.Guerrini2026.g₀✝¹ Phenomena.Generics.Studies.Guerrini2026.dkpTree✝ = some true

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