@cite{cohen-2013}: No Quantification without Reinterpretation

Ariel Cohen, "No Quantification without Reinterpretation." Chapter 13 in Genericity (ed. Mari, Beyssade, Del Prete), OUP, pp. 334–351.

Thesis

The generic quantifier GEN is not a phonologically null version of an overt quantifier — it is introduced by the hearer through reinterpretation of quantifier-free input. The two reinterpretation mechanisms (Predicate Transfer for generics, type-shifting for habituals) explain the different scopal properties of generics vs habituals.

Empirical Generalizations (§13.2)

Construction	Scope behavior
Overt quantifier (every, ∀)	Full scope ambiguity
Generic (bare plural subject)	Ambiguous, except in opaque contexts
Habitual (no restrictor)	Narrow scope only
Habitual (with restrictor)	Ambiguous (restrictor provides Q site)
Bare plural in habitual	Scope below habitual (DRT constraint)

Core Proposal (§§13.3–13.4)

• Generics arise from Predicate Transfer (T_g, @cite{nunberg-1995}): T_g can apply locally (narrow scope) or globally (wide scope), yielding scope ambiguity. But T_g requires the intension of the transferred property, so it cannot scope out of opaque contexts like believe.

• Habituals arise from type-shifting (γ): Eventive verbs require interval arguments; present tense provides a moment → type mismatch → γ fires at the verb level (locally). Since the shift is local, the resulting GEN takes narrow scope only. With an overt restrictor or contextual restriction, there is no mismatch, so normal scope obtains.

Argumentation Chain (§13.3.1 → §13.4.2)

The paper's key argument flows through the Partee-Rooth SHIFT operator:

1. SHIFT does not commute with negation (shift_neg_noncommutative)
2. Any type-shift shares this non-commutativity property
3. γ is a type-shift, so γ does not commute with ∃ (gamma_noncommutative)
4. Therefore γ must apply at the type-mismatch site (locally)
5. Therefore the existential from the indefinite scopes over γ
6. Therefore habituals take narrow scope (habitual_narrow_scope)

Formalization Strategy

We verify Cohen's scope predictions using finite models, with definitions built directly on transferGen and gamma from PredicateTransfer.lean:

1. Storks / nesting areas: T_g applied locally vs globally gives different truth conditions → generics are scopally ambiguous
2. Mary / cigarettes: γ applied locally gives the implausible narrow- scope reading; the plausible wide-scope reading would require global γ, which is unavailable because the type mismatch is at the verb level
3. Scope hierarchy: overt > predicateTransfer > typeShift

These connect to PredicateTransfer.lean (T_g, γ, SHIFT, QuantifierSource), Generics.lean (traditionalGEN), Habituals.lean (traditionalHAB), CovertQuantifier.lean (shared covertQ), and Scope.lean (ScopeConfig).

structure Cohen2013.ScopeDatum : Type

A datum recording the scope behavior of a construction type with respect to another operator (negation, existential, attitude).

• sentence : String
• constructionType : String
• scopePartner : String
• wideAvailable : Bool
• narrowAvailable : Bool
• source : String

def Cohen2013.genericNegation : ScopeDatum

§13.2.1: Generics interact scopally with negation. "Cows do not eat nettles" — ambiguous between gen > ¬ and ¬ > gen.

Equations

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

def Cohen2013.genericOpaque : ScopeDatum

§13.2.1: Generics cannot scope out of opaque contexts. "The King believes enemy spies are loyal" — only bel > gen.

Equations

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

def Cohen2013.genericTransparent : ScopeDatum

§13.2.1: Generics exhibit scope ambiguity in transparent contexts. "Storks have a favorite nesting area" — gen > ∃ and ∃ > gen.

Equations

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

def Cohen2013.habitualNoRestrictor : ScopeDatum

§13.2.2: Habituals without restrictor take narrow scope only. "#John smokes a cigarette" — only ∃ > hab (implausible).

Equations

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

def Cohen2013.habitualWithRestrictor : ScopeDatum

§13.2.2: Habituals WITH restrictor are ambiguous. "John smokes a cigarette when he is nervous" — hab > ∃ and ∃ > hab.

Equations

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

def Cohen2013.barePluralInHabitual : ScopeDatum

§13.2.2: Bare plurals in habituals take scope below the habitual. "John smokes cigarettes" — only hab > gen (not gen > hab).

Equations

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

Storks / Nesting Areas

"Storks have a favorite nesting area"

Initial LF: ∃x(nesting-area(x) ∧ have(∩storks, x))

This is anomalous: kinds don't have nesting areas — individuals do. So Predicate Transfer applies (T_g from PredicateTransfer.lean), with two options depending on the level of application:

• Local T_g (on the verb have): ∃x(area(x) ∧ T_g(λy.have(y,x))(∩storks)) = ∃x(area(x) ∧ gen_y[stork(y)][have(y,x)]) — GEN takes narrow scope

• Global T_g (on the VP have a favorite nesting area): T_g(λy.∃x(area(x) ∧ have(y,x)))(∩storks) = gen_y[stork(y)][∃x(area(x) ∧ have(y,x))] — GEN takes wide scope

The kind ∩storks is modeled as Unit (a single kind-level entity); instances are individual storks. This follows @cite{chierchia-1998}'s ∩ (down) operator, where ∩storks denotes the kind, and ∪(∩storks) gives the extension (the set of individual storks). Here instanceOfStork plays the role of ∪.

inductive Cohen2013.Stork : Type

• s1 : Stork
• s2 : Stork

@[implicit_reducible]

instance Cohen2013.instDecidableEqStork : DecidableEq Stork

Equations

• Cohen2013.instDecidableEqStork x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cohen2013.instReprStork : Repr Stork

Equations

• Cohen2013.instReprStork = { reprPrec := Cohen2013.instReprStork.repr }

def Cohen2013.instReprStork.repr : Stork → ℕ → Std.Format

Equations

• Cohen2013.instReprStork.repr Cohen2013.Stork.s1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Stork.s1")).group prec✝
• Cohen2013.instReprStork.repr Cohen2013.Stork.s2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Stork.s2")).group prec✝

inductive Cohen2013.NestArea : Type

• a1 : NestArea
• a2 : NestArea

@[implicit_reducible]

instance Cohen2013.instDecidableEqNestArea : DecidableEq NestArea

Equations

• Cohen2013.instDecidableEqNestArea x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cohen2013.instReprNestArea : Repr NestArea

Equations

• Cohen2013.instReprNestArea = { reprPrec := Cohen2013.instReprNestArea.repr }

def Cohen2013.instReprNestArea.repr : NestArea → ℕ → Std.Format

Equations

• Cohen2013.instReprNestArea.repr Cohen2013.NestArea.a1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.NestArea.a1")).group prec✝
• Cohen2013.instReprNestArea.repr Cohen2013.NestArea.a2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.NestArea.a2")).group prec✝

def Cohen2013.storks : List Stork

Equations

• Cohen2013.storks = [Cohen2013.Stork.s1, Cohen2013.Stork.s2]

def Cohen2013.areas : List NestArea

Equations

• Cohen2013.areas = [Cohen2013.NestArea.a1, Cohen2013.NestArea.a2]

def Cohen2013.nestsIn : Stork → NestArea → Bool

Each stork nests in a different area: s1→a1, s2→a2

Equations

• Cohen2013.nestsIn Cohen2013.Stork.s1 Cohen2013.NestArea.a1 = true
• Cohen2013.nestsIn Cohen2013.Stork.s2 Cohen2013.NestArea.a2 = true
• Cohen2013.nestsIn x✝¹ x✝ = false

def Cohen2013.genStork (restrictor scope : Stork → Bool) : Bool

GEN as universal over storks (simplified: all storks are "normal").

Equations

• Cohen2013.genStork restrictor scope = Semantics.Quantification.CovertQuantifier.covertQ Cohen2013.storks restrictor scope

def Cohen2013.instanceOfStork : Stork → Unit → Bool

Chierchia's ∪ applied to ∩storks: every Stork is an instance of the kind.

Equations

• Cohen2013.instanceOfStork x✝¹ x✝ = true

def Cohen2013.storkKind : Unit

The kind ∩storks (a single kind-level entity).

Equations

• Cohen2013.storkKind = ()

def Cohen2013.localTransfer : Bool

Local T_g: ∃area(T_g(λy.nestsIn(y, area))(∩storks)) = ∃area(gen_y[stork(y)][nestsIn(y, area)]) "There is one area that, in general, storks nest in."

Equations

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

def Cohen2013.globalTransfer : Bool

Global T_g: T_g(λy.∃area(nestsIn(y, area)))(∩storks) = gen_y[stork(y)][∃area(nestsIn(y, area))] "In general, storks nest in some area (possibly different)."

Equations

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

theorem Cohen2013.generic_scope_ambiguity : localTransfer = false ∧ globalTransfer = true

Generic scope ambiguity: local and global T_g yield different truth conditions. This is why generics in transparent contexts are scopally ambiguous — Predicate Transfer can apply at either level.

The two readings correspond to ScopeConfig.surface (∃ > gen) and ScopeConfig.inverse (gen > ∃).

theorem Cohen2013.generic_both_scopes : genericTransparent.wideAvailable = true ∧ genericTransparent.narrowAvailable = true

The scope ambiguity matches the empirical datum: both readings available.

From SHIFT Non-Commutativity to γ Locality

Cohen's argument for habitual narrow scope flows through the Partee-Rooth SHIFT operator (@cite{partee-rooth-1983}):

1. shift_neg_noncommutative (in PredicateTransfer.lean) proves that SHIFT does not commute with negation: ¬SHIFT(V) ≠ SHIFT(¬V).

2. γ is a type-shift (it resolves a type mismatch between eventive predicates and moments). Like any type-shift, γ does not commute with other operators.

3. gamma_noncommutative below proves the concrete instance: γ does not commute with the existential quantifier over our finite model.

4. Therefore γ must apply at the type-mismatch site — the verb level — before the existential from the indefinite object is composed in.

5. This forces the existential to scope over the habitual GEN.

Mary / Cigarettes

"Mary smokes a cigarette"

The verb smoke is eventive: λy.λx.λe.smoke(x, y, e). In present tense, it applies to the speech time t₀ (a moment). Since an eventive verb requires an interval but receives a moment, there is a type mismatch. γ fires at the verb level:

γ(λe.smoke(m, c, e))(t₀) — this is what happens. THEN the object composes, yielding: ∃c(cigarette(c) ∧ γ(λe.smoke(m, c, e))(t₀))

The existential (from the indefinite) takes wide scope over γ, giving the implausible reading "there is one cigarette that Mary habitually smokes."

The plausible reading (different cigarettes each time) would require GEN to scope over ∃. But that would need γ to apply globally — after the existential is composed in — which is unavailable because the type mismatch is at the verb level (step 4 of the argumentation chain above).

inductive Cohen2013.Occasion : Type

• e1 : Occasion
• e2 : Occasion
• e3 : Occasion

@[implicit_reducible]

instance Cohen2013.instDecidableEqOccasion : DecidableEq Occasion

Equations

• Cohen2013.instDecidableEqOccasion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Cohen2013.instReprOccasion : Repr Occasion

Equations

• Cohen2013.instReprOccasion = { reprPrec := Cohen2013.instReprOccasion.repr }

def Cohen2013.instReprOccasion.repr : Occasion → ℕ → Std.Format

Equations

• Cohen2013.instReprOccasion.repr Cohen2013.Occasion.e1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Occasion.e1")).group prec✝
• Cohen2013.instReprOccasion.repr Cohen2013.Occasion.e2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Occasion.e2")).group prec✝
• Cohen2013.instReprOccasion.repr Cohen2013.Occasion.e3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Occasion.e3")).group prec✝

inductive Cohen2013.Cigarette : Type

• c1 : Cigarette
• c2 : Cigarette
• c3 : Cigarette

@[implicit_reducible]

instance Cohen2013.instDecidableEqCigarette : DecidableEq Cigarette

Equations

• Cohen2013.instDecidableEqCigarette x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cohen2013.instReprCigarette.repr : Cigarette → ℕ → Std.Format

Equations

• Cohen2013.instReprCigarette.repr Cohen2013.Cigarette.c1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Cigarette.c1")).group prec✝
• Cohen2013.instReprCigarette.repr Cohen2013.Cigarette.c2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Cigarette.c2")).group prec✝
• Cohen2013.instReprCigarette.repr Cohen2013.Cigarette.c3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cohen2013.Cigarette.c3")).group prec✝

@[implicit_reducible]

instance Cohen2013.instReprCigarette : Repr Cigarette

Equations

• Cohen2013.instReprCigarette = { reprPrec := Cohen2013.instReprCigarette.repr }

def Cohen2013.occasions : List Occasion

Equations

• Cohen2013.occasions = [Cohen2013.Occasion.e1, Cohen2013.Occasion.e2, Cohen2013.Occasion.e3]

def Cohen2013.cigarettes : List Cigarette

Equations

• Cohen2013.cigarettes = [Cohen2013.Cigarette.c1, Cohen2013.Cigarette.c2, Cohen2013.Cigarette.c3]

def Cohen2013.smokes : Cigarette → Occasion → Bool

Mary smokes a different cigarette each time.

Equations

• Cohen2013.smokes Cohen2013.Cigarette.c1 Cohen2013.Occasion.e1 = true
• Cohen2013.smokes Cohen2013.Cigarette.c2 Cohen2013.Occasion.e2 = true
• Cohen2013.smokes Cohen2013.Cigarette.c3 Cohen2013.Occasion.e3 = true
• Cohen2013.smokes x✝¹ x✝ = false

def Cohen2013.genHab (restrictor scope : Occasion → Bool) : Bool

GEN over occasions (simplified: all occasions are relevant).

Equations

• Cohen2013.genHab restrictor scope = Semantics.Quantification.CovertQuantifier.covertQ Cohen2013.occasions restrictor scope

def Cohen2013.containedInSpeech : Occasion → Unit → Bool

All occasions are contained in the relevant interval of speech time t₀.

Equations

• Cohen2013.containedInSpeech x✝¹ x✝ = true

def Cohen2013.speechTime : Unit

The speech time (a moment).

Equations

• Cohen2013.speechTime = ()

def Cohen2013.localGamma : Bool

Local γ (γ at verb, then object composes): ∃c(cigarette(c) ∧ γ(λe.smoke(m,c,e))(t₀)) "There is one cigarette that Mary habitually smokes."

Equations

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

def Cohen2013.globalGamma : Bool

Global γ (hypothetical — if γ could apply to the whole VP): γ(λe.∃c(cigarette(c) ∧ smoke(m,c,e)))(t₀) "Mary is habitually in a situation where she smokes some cigarette."

Equations

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

theorem Cohen2013.habitual_narrow_scope : localGamma = false ∧ globalGamma = true

Habitual narrow scope: local and global γ differ, but only local is available. The plausible wide-scope reading is blocked because γ must apply at the type-mismatch site (the verb level).

This explains why "#John smokes a cigarette" is odd: the only available reading (∃ > hab) is implausible.

theorem Cohen2013.habitual_matches_datum : habitualNoRestrictor.wideAvailable = false

The narrow-scope-only prediction matches the empirical datum.

theorem Cohen2013.gamma_noncommutative : localGamma ≠ globalGamma

γ does not commute with ∃ on our model.

This is the concrete instance of the general non-commutativity argument from §13.3.1 (proved abstractly for SHIFT in shift_neg_noncommutative). The non-commutativity is what forces γ to apply locally.

theorem Cohen2013.scope_hierarchy : Semantics.Composition.PredicateTransfer.QuantifierSource.overt.canTakeWideScope = true ∧ Semantics.Composition.PredicateTransfer.QuantifierSource.overt.canScopeOutOfOpaque = true ∧ Semantics.Composition.PredicateTransfer.QuantifierSource.predicateTransfer.canTakeWideScope = true ∧ Semantics.Composition.PredicateTransfer.QuantifierSource.predicateTransfer.canScopeOutOfOpaque = false ∧ Semantics.Composition.PredicateTransfer.QuantifierSource.typeShift.canTakeWideScope = false ∧ Semantics.Composition.PredicateTransfer.QuantifierSource.typeShift.canScopeOutOfOpaque = false

Cohen's core thesis: the mechanism that introduces GEN determines its scope behavior. The three sources form a strict hierarchy:

overt > predicateTransfer > typeShift

in scope freedom. QuantifierSource in PredicateTransfer.lean encodes this hierarchy.

theorem Cohen2013.predictions_match_data : genericTransparent.wideAvailable = Semantics.Composition.PredicateTransfer.QuantifierSource.predicateTransfer.canTakeWideScope ∧ genericOpaque.wideAvailable = Semantics.Composition.PredicateTransfer.QuantifierSource.predicateTransfer.canScopeOutOfOpaque ∧ habitualNoRestrictor.wideAvailable = Semantics.Composition.PredicateTransfer.QuantifierSource.typeShift.canTakeWideScope

The scope behavior of each construction type matches its QuantifierSource prediction.

theorem Cohen2013.both_reduce_to_covertQ : (Semantics.Composition.PredicateTransfer.transferGen genStork instanceOfStork (fun (y : Stork) => nestsIn y NestArea.a1) storkKind = Semantics.Quantification.CovertQuantifier.covertQ storks (fun (x : Stork) => true) fun (y : Stork) => nestsIn y NestArea.a1) ∧ Semantics.Composition.PredicateTransfer.gamma genHab containedInSpeech (fun (e : Occasion) => smokes Cigarette.c1 e) speechTime = Semantics.Quantification.CovertQuantifier.covertQ occasions (fun (x : Occasion) => true) fun (e : Occasion) => smokes Cigarette.c1 e

Both T_g and γ produce instances of covertQ, confirming that CovertQuantifier.lean's shared infrastructure correctly captures the common logical form. The difference is upstream (how the quantifier is introduced), not downstream (what it evaluates to).

T_g with our stork model reduces to covertQ storks because instanceOfStork y () = true for all y, making the restrictor equivalent to fun y => true — i.e., all storks are in the domain.

γ with our model reduces to covertQ occasions because containedInSpeech e () = true for all e, making the restrictor equivalent to fun e => true — i.e., all occasions are relevant.

theorem Cohen2013.generic_scope_configs : [Semantics.Scope.ScopeConfig.surface, Semantics.Scope.ScopeConfig.inverse] = Semantics.Scope.allScopeConfigs

The available scope configurations for generics: both surface and inverse scope (matching Scope.allScopeConfigs).

def Cohen2013.habitualScopeConfigs : List Semantics.Scope.ScopeConfig

The available scope configuration for unrestricted habituals: surface scope only (the covert Q takes narrow scope).

Equations

• Cohen2013.habitualScopeConfigs = [Semantics.Scope.ScopeConfig.surface]

theorem Cohen2013.habitual_scope_restricted : habitualScopeConfigs.length < Semantics.Scope.allScopeConfigs.length