Carlson's Foundational Insights

@cite{carlson-1977}

@cite{carlson-1977} established the key ideas that all subsequent theories build on:

1. Bare plurals are proper names of kinds (type e, not quantifiers)
2. Kinds are spatially unbounded (can be "here and there")
3. The Realization relation R(y,x) connects stages to individuals/kinds
4. Predicate level determines reading: Stage-level → ∃, Individual-level → generic
5. The ∃ comes from the predicate, not the NP

How Subsequent Theories Relate

@cite{chierchia-1998} formalizes Carlson's R relation as the ∪ operator:

• Carlson: R y k means "y is a stage/realization of k"
• Chierchia: x ∈ ∪k(w) means "x is in the extension of kind k at world w"

Chierchia's DKP is Carlson's stage-level predication:

• Carlson: stageLevelPred R P k = ∃y[R(y,k) ∧ P(y)]
• Chierchia: DKP P k w = ∃x[x ∈ ∪k(w) ∧ P(x)]

@cite{krifka-2004} departs from Carlson:

• Rejects kinds as basic; bare NPs are properties
• But keeps the insight: ∃ is introduced locally, yielding narrow scope

theorem Phenomena.Generics.Compare.carlson_chierchia_structural_equivalence : (∀ (Entity : Type) (R : Semantics.Lexical.Noun.Kind.Carlson1977.RealizationRel Entity) (P : Entity → Bool) (k : Entity), Semantics.Lexical.Noun.Kind.Carlson1977.stageLevelPred Entity R P k = ∃ (y : Entity), R y k ∧ P y = true) ∧ True

Structural equivalence: Carlson's stage-level predication and Chierchia's DKP have the same logical form.

Both introduce existential quantification over instances/stages of the kind, then apply the object-level predicate to those instances.

Carlson: λk. ∃y[R(y,k) ∧ P(y)]
Chierchia: λk. ∃x[x ∈ ∪k(w) ∧ P(x)]

The only difference is the formalization of "instance-of":

• Carlson uses a primitive R relation
• Chierchia uses the ∪ operator derived from kind semantics

theorem Phenomena.Generics.Compare.predicate_classification_equivalence : Semantics.Lexical.Noun.Kind.Carlson1977.PredicateLevel.stageLevel ≠ Semantics.Lexical.Noun.Kind.Carlson1977.PredicateLevel.individualLevel ∧ True

Predicate classification equivalence:

@cite{carlson-1977}	@cite{chierchia-1998}	Effect
Stage-level (states)	Object-level	Triggers DKP / R-predication
Individual-level (properties)	Kind-level	Direct predication of kind

Both classify predicates the same way; they just use different terminology.

theorem Phenomena.Generics.Compare.carlson_explains_scopelessness : (∀ (Entity : Type) (R : Semantics.Lexical.Noun.Kind.Carlson1977.RealizationRel Entity) (P : Entity → Bool) (k : Entity), Semantics.Lexical.Noun.Kind.Carlson1977.stageLevelPred Entity R P k = ∃ (y : Entity), R y k ∧ P y = true) ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true

Both Carlson and Chierchia explain narrow scope the same way: the ∃ is introduced inside the predicate abstract.

• Carlson: "The existential over stages is introduced by the predicate"
• Chierchia: "DKP introduces a LOCAL existential"

Since the ∃ is inside the predicate, it cannot scope over external operators.

Carlson's Unified Analysis vs Ambiguity Theories

Carlson's key claim: bare plurals are NOT ambiguous between generic and existential readings. The NP always denotes the kind; the predicate determines whether you get a generic or existential interpretation.

This is captured in bare_plural_not_ambiguous in Carlson1977.lean.

theorem Phenomena.Generics.Compare.carlson_unified_analysis : (∀ (Entity : Type) (k : Entity) (P : Semantics.Lexical.Noun.Kind.Carlson1977.IndividualLevelPred Entity), Semantics.Lexical.Noun.Kind.Carlson1977.genericDerivation k P = P k) ∧ ∀ (Entity : Type) (R : Semantics.Lexical.Noun.Kind.Carlson1977.RealizationRel Entity) (k : Entity) (P : Entity → Bool), Semantics.Lexical.Noun.Kind.Carlson1977.existentialDerivation R k P = ∃ (y : Entity), R y k ∧ P y = true

Carlson's core thesis: One meaning, two readings.

The bare plural "dogs" always denotes the kind DOGS.

• With "be intelligent" (individual-level): predicate applies to kind directly
• With "be in the yard" (stage-level): predicate introduces ∃ over stages

No ambiguity in the NP — the "ambiguity" is in predicate selection.

theorem Phenomena.Generics.Compare.english_bare_plural_prediction : Semantics.Lexical.Noun.Kind.Dayal2004.englishKindRef.bareKindsOK = KindReference.englishBarePlural.bareKindOK

English parameters predict bare plural licensing.

The theory (englishKindRef) correctly predicts the empirical pattern (englishBarePlural.bareKindOK = true).

theorem Phenomena.Generics.Compare.english_singular_needs_definite : Semantics.Lexical.Noun.Kind.Dayal2004.englishKindRef.hasDefiniteArticle = true ∧ Semantics.Lexical.Noun.Kind.Dayal2004.englishKindRef.definiteSingularKinds = true ∧ KindReference.englishDefiniteSingularKind.defKindOK = true

English parameters predict bare singular restriction.

The theory predicts bare singulars need "the" for kind reference, matching the empirical pattern.

theorem Phenomena.Generics.Compare.french_definite_required : Semantics.Lexical.Noun.Kind.Dayal2004.romanceKindRef.bareKindsOK = false ∧ Semantics.Lexical.Noun.Kind.Dayal2004.romanceKindRef.definitePluralKinds = true ∧ KindReference.frenchPluralKind.bareKindOK = false ∧ KindReference.frenchPluralKind.defKindOK = true

French (Romance) parameters predict definite requirement.

The theory (romanceKindRef) correctly predicts that French requires definite articles for kind reference.

theorem Phenomena.Generics.Compare.hindi_bare_nominals : Semantics.Lexical.Noun.Kind.Dayal2004.determinerlessKindRef.bareKindsOK = true ∧ Semantics.Lexical.Noun.Kind.Dayal2004.determinerlessKindRef.hasDefiniteArticle = false ∧ KindReference.hindiKind.bareKindOK = true

Hindi (determiner-less) parameters predict bare nominal freedom.

The theory (determinerlessKindRef) correctly predicts that Hindi allows bare nominals for kind reference.

theorem Phenomena.Generics.Compare.bare_plural_scopeless_empirically : KindReference.negationBarePlural.ambiguous = false ∧ KindReference.universalBarePlural.ambiguous = false

The phenomena data confirms bare plurals are scopeless.

theorem Phenomena.Generics.Compare.explicit_quantifier_ambiguous : KindReference.negationSomeDogs.ambiguous = true ∧ KindReference.universalSomeBooks.ambiguous = true

Contrast: Explicit quantifiers ARE scopally ambiguous.

theorem Phenomena.Generics.Compare.dkp_locality_predicts_scopelessness : Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true → KindReference.negationBarePlural.ambiguous = false ∧ KindReference.universalBarePlural.ambiguous = false

Theory (DKP locality) correctly predicts empirical scopelessness.

The theoretical claim dkpIsLocal = true from Kinds.lean predicts the empirical pattern of bare plural scopelessness.

theorem Phenomena.Generics.Compare.kind_level_predicates_direct : KindReference.beExtinct.directKindApplication = true ∧ KindReference.beWidespread.directKindApplication = true ∧ KindReference.beRare.directKindApplication = true ∧ KindReference.evolveFrom.directKindApplication = true

Kind-level predicates apply directly to kinds (no DKP needed).

theorem Phenomena.Generics.Compare.object_level_predicates_need_dkp : KindReference.beBarkingInYard.directKindApplication = false ∧ KindReference.beInGarden.directKindApplication = false

Object-level predicates require DKP for kind subjects.

theorem Phenomena.Generics.Compare.predicate_classification_complete : ((List.filter (fun (p : KindReference.PredicateDatum) => p.level == KindReference.PredLevel.kind) KindReference.predicateData).all fun (p : KindReference.PredicateDatum) => p.directKindApplication) = true ∧ ((List.filter (fun (p : KindReference.PredicateDatum) => p.level == KindReference.PredLevel.object) KindReference.predicateData).all fun (p : KindReference.PredicateDatum) => !p.directKindApplication) = true

The predicate classification correctly partitions the data.

theorem Phenomena.Generics.Compare.singular_kinds_licensed : KindReference.dodoExtinct.grammatical = true ∧ KindReference.computerRevolutionized.grammatical = true ∧ KindReference.lionPredator.grammatical = true

Singular kinds are licensed by specific conditions (extinct, invention, taxonomic).

theorem Phenomena.Generics.Compare.modification_blocks_singular_kind : KindReference.tallLionOdd.grammatical = false

Modification blocks singular kind reading.

theorem Phenomena.Generics.Compare.theory_phenomena_alignment : Semantics.Lexical.Noun.Kind.Dayal2004.englishKindRef.bareKindsOK = KindReference.englishBarePlural.bareKindOK ∧ Semantics.Lexical.Noun.Kind.Dayal2004.romanceKindRef.bareKindsOK = KindReference.frenchPluralKind.bareKindOK ∧ Semantics.Lexical.Noun.Kind.Dayal2004.determinerlessKindRef.bareKindsOK = KindReference.hindiKind.bareKindOK ∧ KindReference.negationBarePlural.ambiguous = false ∧ KindReference.negationSomeDogs.ambiguous = true ∧ KindReference.beExtinct.directKindApplication = true ∧ KindReference.beBarkingInYard.directKindApplication = false

The Chierchia/Dayal theoretical framework correctly predicts the major empirical patterns in kind reference:

1. Cross-linguistic bare nominal licensing
2. Scopelessness of bare plurals
3. Kind-level vs object-level predicate behavior
4. Singular kind licensing conditions

This demonstrates that the formalization captures genuine linguistic generalizations, not just individual paper implementations.

Alternative Theories: Same Predictions, Different Mechanisms

@cite{chierchia-1998} and @cite{krifka-2004} both correctly predict the empirical patterns but propose different underlying mechanisms:

Phenomenon	Chierchia	Krifka
Basic denotation	Kind (via ∩)	Property
Existential reading	DKP coercion	Direct ∃ type shift
Scopelessness	DKP locality	Local number binding
Bare singular out	∩ undefined	Number param unfilled
Kind reading	Always available	Requires topic position

Below we prove they are observationally equivalent for the core phenomena.

theorem Phenomena.Generics.Compare.both_theories_bare_singular_out : Semantics.Lexical.Noun.Kind.Chierchia1998.downDefinedFor MassCount.count false = false ∧ { }.bareUnfilled = true ∧ KindReference.bareSgSubject.grammatical = false

Both theories predict bare singular restriction.

• Chierchia: ∩ is undefined for singular count nouns
• Krifka: Number parameter is unfilled

Both mechanisms yield the same prediction: bare singulars ungrammatical.

theorem Phenomena.Generics.Compare.both_theories_scopelessness : Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true ∧ KindReference.negationBarePlural.ambiguous = false ∧ KindReference.universalBarePlural.ambiguous = false

Both theories predict scopelessness via locality.

• Chierchia: dkpIsLocal = true — DKP introduces ∃ inside predicate abstract
• Krifka: plural_is_local — ∃ binds number argument inside NP

Both locality mechanisms predict bare plurals cannot take wide scope.

theorem Phenomena.Generics.Compare.both_theories_mass_ok : Semantics.Lexical.Noun.Kind.Chierchia1998.downDefinedFor MassCount.mass true = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.downDefinedFor MassCount.mass false = true ∧ KindReference.englishMassNoun.bareKindOK = true

Both theories predict mass nouns pattern with plurals.

• Chierchia: ∩ is defined for mass nouns (always, regardless of "plural" flag)
• Krifka: Mass nouns have no number parameter to fill

Both predict bare mass nouns are grammatical.

theorem Phenomena.Generics.Compare.chierchia_krifka_observationally_equivalent : KindReference.englishBarePlural.bareKindOK = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.downDefinedFor MassCount.count false = false ∧ { }.bareUnfilled = true ∧ KindReference.bareSgSubject.grammatical = false ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true ∧ KindReference.negationBarePlural.ambiguous = false ∧ KindReference.englishMassNoun.bareKindOK = true

Observational equivalence for core phenomena.

Both Chierchia and Krifka correctly predict all of:

1. Bare plural licensing
2. Bare singular restriction
3. Scopelessness
4. Mass noun patterning
5. Cross-linguistic variation

The theories differ on mechanism, not prediction.

Where the Theories Differ

The theories make different predictions for:

1. Scrambling and scope: See below. This is where Krifka is correct and Chierchia fails.

2. Information structure effects: Krifka predicts kind readings require topic position; Chierchia does not distinguish.

3. Non-cumulative properties: Krifka's ∩ is unrestricted; Chierchia's requires cumulativity.

The Scrambling Test Case

In Dutch and German, objects can "scramble" to precede negation/adverbs. This affects bare plural scope:

• Unscrambled: narrow scope only (both theories predict this)
• Scrambled: wide scope (Krifka predicts this, Chierchia does not)

Chierchia's problem:

• BPs denote kinds via ∩
• DKP introduces LOCAL existential quantification
• Locality predicts narrow scope always, regardless of surface position
• But scrambled BPs take wide scope.

Krifka's solution:

• BPs undergo ∃-shift at their surface position
• Scrambling moves the BP, so ∃ scopes from the higher position
• Correctly predicts: unscrambled = narrow, scrambled = wide

Scrambled BPs can still be kind-referring with appropriate predicates like "haten" (hate). This shows scrambling does not force an indefinite reading; it just affects scope when ∃-shift applies.

theorem Phenomena.Generics.Compare.chierchia_predicts_narrow_scope_always : Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true

Chierchia predicts narrow scope for all bare plurals.

DKP locality means the existential is introduced inside the predicate, so it cannot scope over external operators like negation.

theorem Phenomena.Generics.Compare.krifka_scope_follows_position : Semantics.Lexical.Noun.Kind.Krifka2004.existentialShiftPositionSensitive = true

Krifka predicts scope follows surface position.

The ∃-shift applies at the surface position of the BP, so:

• Unscrambled (below negation) → narrow scope
• Scrambled (above negation) → wide scope

theorem Phenomena.Generics.Compare.dutch_unscrambled_narrow : KindReference.dutchUnscrambledNeg.position = KindReference.ScramblingPosition.unscrambled ∧ KindReference.dutchUnscrambledNeg.narrowOK = true ∧ KindReference.dutchUnscrambledNeg.wideOK = false

Dutch unscrambled BPs are narrow scope only.

Both theories correctly predict this.

theorem Phenomena.Generics.Compare.dutch_scrambled_wide : KindReference.dutchScrambledBoeken.position = KindReference.ScramblingPosition.scrambled ∧ KindReference.dutchScrambledBoeken.narrowOK = false ∧ KindReference.dutchScrambledBoeken.wideOK = true

Dutch scrambled BPs take wide scope.

This is where Krifka succeeds and Chierchia fails.

theorem Phenomena.Generics.Compare.scrambled_allows_kind_reference : KindReference.dutchScrambledKindBoeken.position = KindReference.ScramblingPosition.scrambled ∧ KindReference.dutchScrambledKindBoeken.kindReferenceOK = true

Scrambled BPs can still be kind-referring.

With kind-level predicates like "hate", scrambled BPs get kind readings. This shows scrambling doesn't force indefinite interpretation.

theorem Phenomena.Generics.Compare.krifka_handles_scrambling_chierchia_doesnt : KindReference.dutchScrambledBoeken.wideOK = true ∧ KindReference.dutchScrambledMensen.wideOK = true ∧ Semantics.Lexical.Noun.Kind.Krifka2004.existentialShiftPositionSensitive = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true ∧ KindReference.dutchScrambledBoeken.wideOK = true

Krifka correctly predicts scrambling scope; Chierchia does not.

This breaks observational equivalence for the scrambling data:

• Chierchia: narrow scope always (incorrect for scrambled BPs)
• Krifka: scope follows position (correct)

Compositional Derivations

The derivation machinery lives in the theory files:

• Chierchia1998.lean: chierchiaDerivUnscrambled, chierchiaDerivScrambled, chierchia_position_invariant
• Krifka2004.lean: krifkaDerivUnscrambled, krifkaDerivScrambled, krifka_position_sensitive

Here we instantiate them with a concrete example to demonstrate the divergence.

The Key Difference

Chierchia: DKP is position-invariant (proved in chierchia_position_invariant)

• scrambled = unscrambled = ¬∃x[P(x) ∧ V(x)]

Krifka: ∃-shift is position-sensitive (definition of krifkaDerivScrambled)

• unscrambled = ¬∃x[P(x) ∧ V(x)]
• scrambled = ∃x[P(x) ∧ ¬V(x)]

Concrete Example: Two Books

World with two books: b1, b2

• I finished b1: V(b1) = true
• I didn't finish b2: V(b2) = false

Chierchia (both positions): ¬∃x[book(x) ∧ finished(x)] = ¬(finished(b1) ∨ finished(b2)) = ¬true = FALSE

Krifka unscrambled: ¬∃x[book(x) ∧ finished(x)] = FALSE (same as Chierchia)

Krifka scrambled: ∃x[book(x) ∧ ¬finished(x)] = ¬finished(b1) ∨ ¬finished(b2) = false ∨ true = TRUE

The scrambled sentence is TRUE: "There are books I didn't finish" ✓ The unscrambled sentence is FALSE: "I didn't finish books" (= I finished no books) ✓

inductive Phenomena.Generics.Compare.Book : Type

• b1 : Book
• b2 : Book

instance Phenomena.Generics.Compare.instDecidableEqBook : DecidableEq Book

Equations

• Phenomena.Generics.Compare.instDecidableEqBook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Generics.Compare.instReprBook : Repr Book

Equations

• Phenomena.Generics.Compare.instReprBook = { reprPrec := Phenomena.Generics.Compare.instReprBook.repr }

def Phenomena.Generics.Compare.instReprBook.repr : Book → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Compare.bookDomain : List Book

Equations

• Phenomena.Generics.Compare.bookDomain = [Phenomena.Generics.Compare.Book.b1, Phenomena.Generics.Compare.Book.b2]

def Phenomena.Generics.Compare.isBook : Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaProp Book Unit

Equations

• Phenomena.Generics.Compare.isBook x✝¹ x✝ = true

def Phenomena.Generics.Compare.finishedVP : Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaVP Book Unit

Equations

• Phenomena.Generics.Compare.finishedVP Phenomena.Generics.Compare.Book.b1 x✝ = true
• Phenomena.Generics.Compare.finishedVP Phenomena.Generics.Compare.Book.b2 x✝ = false

def Phenomena.Generics.Compare.bookKind : Semantics.Lexical.Noun.Kind.Chierchia1998.KindExtension Book Unit

Equations

• Phenomena.Generics.Compare.bookKind x✝ = Phenomena.Generics.Compare.bookDomain

def Phenomena.Generics.Compare.finishedChierchia : Semantics.Lexical.Noun.Kind.Chierchia1998.ChierchiaVP Book Unit

Equations

• Phenomena.Generics.Compare.finishedChierchia = Phenomena.Generics.Compare.finishedVP

theorem Phenomena.Generics.Compare.scrambling_main_result : Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivScrambled bookDomain isBook finishedVP () = true ∧ Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivUnscrambled bookDomain isBook finishedVP () = false ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivScrambled bookKind finishedChierchia () = false ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivUnscrambled bookKind finishedChierchia () = false ∧ Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivScrambled bookDomain isBook finishedVP () = KindReference.dutchScrambledBoeken.wideOK

Krifka correctly distinguishes scrambled/unscrambled; Chierchia incorrectly predicts they are the same.

This theorem combines:

1. The position-invariance of Chierchia (chierchia_position_invariant)
2. The position-sensitivity of Krifka (krifka_position_sensitive)
3. Concrete verification that Krifka matches the empirical data

theorem Phenomena.Generics.Compare.theories_diverge_on_scrambling : Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivUnscrambled bookKind finishedChierchia () = Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivUnscrambled bookDomain isBook finishedVP () ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivScrambled bookKind finishedChierchia () ≠ Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivScrambled bookDomain isBook finishedVP ()

The theories agree on unscrambled but diverge on scrambled.

Theoretical Implications

@cite{le-bruyn-de-swart-2022} conclude:

1. @cite{krifka-2004} is empirically superior for scrambling languages
2. @cite{chierchia-1998} needs modification to handle position-sensitive scope
3. Kind reference ≠ narrow scope: Scrambled BPs can be kind-referring while taking wide scope, showing these are orthogonal properties

The key theorems from the theory files:

• chierchia_position_invariant: Proves Chierchia's DKP gives same meaning regardless of position
• krifka_position_sensitive: Shows Krifka's ∃-shift respects surface position

See Phenomena/Generics/KindReference.lean for the full scrambling dataset.