Cohen (2013): No quantification without reinterpretation

A generic or habitual sentence contains no audible quantifier, so the hearer must introduce one by reinterpreting the quantifierless input, and the introducing device — not a phonologically null determiner — fixes the quantifier's scope. Generics arise by Nunberg's Predicate Transfer: when predicating a property of a kind makes no pragmatic sense, the predicate is transferred to one true of a kind whose instances generically bear it. Pragmatic triggering leaves the transfer free to apply at any level of composition, after Nunberg and Recanati, so "Storks have a favorite nesting area" is scopally ambiguous — transfer of the verb leaves the generic under the existential, transfer of the whole phrase puts it above (§13.4.1) — though never out of an opaque context, since transfer needs the property's intension. Habituals arise by a type-shift: an eventive verb is evaluated at intervals while the present tense supplies a moment (after Taylor and Dowty), and the shift γ resolves the mismatch at the verb, before the object composes, so "Mary smokes a cigarette" keeps the generic under the existential and is odd, while the brand variant is fine (§13.4.2). That a type-shift applies only at its trigger site is argued from Partee and Rooth's SHIFT: negating a shifted verb differs from shifting a negated one, and only the first order is attested (§13.3.1, after the conjunction needed but didn't buy). Scope alone also does not exhaust the generic–negation interaction: focus fixes the alternative set of Cohen's earlier generic quantifier, so "Cows do not eat [nettles]" generalizes with exceptions while "Cows do [not] eat nettles" denies that any cow eats them (§13.2.1).

We state the two devices with the generic quantifier of Studies/Cohen1999.lean in the transferred and shifted predicates, derive both scopes of the storks sentence from the transfer's freedom of level and the infelicity of the cigarette sentence from the shift's locality, and check the focus readings of the nettles sentence against the two alternative sets.

Implementation notes

The generic quantifier inside the reinterpretation operators is the absolute reading with trivial alternatives, per the chapter's own pointer to Cohen's earlier work for its content. Kinds are Unit, individuals and intervals Fin n; a felicity judgment is derived as the absence of a true reading among the available ones.

TODO

• Bare plurals under habituals ((18): gen above the existential only) follow from bare plurals introducing no discourse referent, a duplex condition under an existential being no well-formed DRS (after Cohen and Erteschik-Shir); this needs the DRT box substrate.
• Predicate Transfer's ban on scoping out of opaque contexts (§13.4.1) rests on its need for the property's intension, which these extensional models cannot state.
• The wide-scope generic objects of (19)–(20), which refute a syntactic account (§13.2.3), presuppose a subject–object asymmetry not encoded here.

References

• A. Cohen, No Quantification without Reinterpretation (2013)
• G. Nunberg, Transfers of Meaning (1995)
• B. Partee and M. Rooth, Generalized Conjunction and Type Ambiguity (1983)
• A. Cohen, Think Generic! The Meaning and Use of Generic Sentences (1999)
• G. N. Carlson, Reference to Kinds in English (1977)
• M. Krifka, F. J. Pelletier, G. N. Carlson, A. ter Meulen, G. Chierchia and G. Link, Genericity: An Introduction (1995)
• A. Cohen and N. Erteschik-Shir, Topic, Focus, and the Interpretation of Bare Plurals (2002)
• F. Recanati, Embedded Implicatures (2003)
• B. Taylor, Tense and Continuity (1977)
• D. R. Dowty, Word Meaning and Montague Grammar (1979)

The two reinterpretation devices (§13.3)

def Cohen2013.SHIFT {E : Type u_1} (V : E → E → Prop) : ((E → Prop) → Prop) → E → Prop

Partee and Rooth's SHIFT, lifting an extensional transitive verb to take a quantifier object.

Equations

• Cohen2013.SHIFT V Q x = Q fun (y : E) => V x y

theorem Cohen2013.not_shift_ne_shift_not : ∃ (V : Bool → Bool → Prop) (Q : (Bool → Prop) → Prop) (x : Bool), ¬(¬SHIFT V Q x ↔ SHIFT (fun (a b : Bool) => ¬V a b) Q x)

Negating a shifted verb differs from shifting the negated verb, and only the first order is attested ((25)): a type-shift applies at its trigger site, before further composition.

def Cohen2013.transfer {Kind : Type u_1} {Ind : Type u_2} [MeasurableSpace Ind] [MeasurableSingletonClass Ind] [Fintype Ind] (instanceOf : Ind → Kind → Prop) [(k : Kind) → DecidablePred fun (y : Ind) => instanceOf y k] (P : Ind → Prop) [DecidablePred P] : Kind → Prop

Predicate Transfer for generics (§13.4.1): a property of individuals becomes the property of a kind whose instances generically bear it.

Equations

• Cohen2013.transfer instanceOf P k = Cohen1999.gen Finset.univ (fun (y : Ind) => instanceOf y k) (fun (x : Ind) => True) P

@[instance_reducible]

instance Cohen2013.instDecidableTransfer {Kind : Type u_1} {Ind : Type u_2} [MeasurableSpace Ind] [MeasurableSingletonClass Ind] [Fintype Ind] (instanceOf : Ind → Kind → Prop) [(k : Kind) → DecidablePred fun (y : Ind) => instanceOf y k] (P : Ind → Prop) [DecidablePred P] (k : Kind) : Decidable (transfer instanceOf P k)

Equations

• Cohen2013.instDecidableTransfer instanceOf P k = id inferInstance

def Cohen2013.gamma {Interval : Type u_1} {Moment : Type u_2} [MeasurableSpace Interval] [MeasurableSingletonClass Interval] [Fintype Interval] (containedIn : Interval → Moment → Prop) [(t : Moment) → DecidablePred fun (e : Interval) => containedIn e t] (P : Interval → Prop) [DecidablePred P] : Moment → Prop

The habitual type-shift γ (§13.4.2): a property of intervals becomes the property of a moment in whose surrounding interval it generically holds.

Equations

• Cohen2013.gamma containedIn P t = Cohen1999.gen Finset.univ (fun (e : Interval) => containedIn e t) (fun (x : Interval) => True) P

@[instance_reducible]

instance Cohen2013.instDecidableGamma {Interval : Type u_1} {Moment : Type u_2} [MeasurableSpace Interval] [MeasurableSingletonClass Interval] [Fintype Interval] (containedIn : Interval → Moment → Prop) [(t : Moment) → DecidablePred fun (e : Interval) => containedIn e t] (P : Interval → Prop) [DecidablePred P] (t : Moment) : Decidable (gamma containedIn P t)

Equations

• Cohen2013.instDecidableGamma containedIn P t = id inferInstance

inductive Cohen2013.Level : Type

A reinterpretation device applies at the mismatching word itself or at the containing phrase.

• word : Level
• phrase : Level

@[instance_reducible]

instance Cohen2013.instDecidableEqLevel : DecidableEq Level

Equations

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

inductive Cohen2013.Device : Type

The two devices that introduce covert quantifiers (§13.3).

• predicateTransfer : Device
• typeShift : Device

@[instance_reducible]

instance Cohen2013.instDecidableEqDevice : DecidableEq Device

Equations

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

def Cohen2013.Device.AppliesAt : Device → Level → Prop

Where a device may apply (§13.3): Predicate Transfer is pragmatically triggered and free to apply at any level; a type-shift fires at the type-mismatch site only.

Equations

• Cohen2013.Device.predicateTransfer.AppliesAt x✝ = True
• Cohen2013.Device.typeShift.AppliesAt x✝ = (x✝ = Cohen2013.Level.word)

Storks have a favorite nesting area (§13.4.1)

Two storks, each nesting in its own area. Transfer at the verb quantifies each area's candidate nesters, transfer at the phrase quantifies the storks' own areas: the readings differ in truth value, and both are available to Predicate Transfer, so the sentence is scopally ambiguous and true on one reading.

@[reducible, inline]

abbrev Cohen2013.nestsIn : Fin 2 → Fin 2 → Prop

Each of two storks nests in its own area.

Equations

• Cohen2013.nestsIn x1✝ x2✝ = (x1✝ = x2✝)

@[reducible, inline]

abbrev Cohen2013.storkOf : Fin 2 → Unit → Prop

Every individual stork instantiates the kind.

Equations

• Cohen2013.storkOf x✝¹ x✝ = True

def Cohen2013.storksReading : Level → Prop

The two logical forms of the storks sentence, by level of transfer.

Equations

• Cohen2013.storksReading Cohen2013.Level.word = ∃ (a : Fin 2), Cohen2013.transfer Cohen2013.storkOf (fun (s : Fin 2) => Cohen2013.nestsIn s a) ()
• Cohen2013.storksReading Cohen2013.Level.phrase = Cohen2013.transfer Cohen2013.storkOf (fun (s : Fin 2) => ∃ (a : Fin 2), Cohen2013.nestsIn s a) ()

@[instance_reducible]

instance Cohen2013.instDecidableStorksReading (l : Level) : Decidable (storksReading l)

Equations

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

theorem Cohen2013.storksReading_word_ne_phrase : ¬storksReading Level.word ∧ storksReading Level.phrase

The two levels yield distinct readings: no single area serves most storks, while every stork has its own.

theorem Cohen2013.storks_true_reading_available : ∃ (l : Level), Device.predicateTransfer.AppliesAt l ∧ storksReading l

Predicate Transfer makes a true reading available: the sentence is felicitous.

Mary smokes a cigarette (§13.4.2)

Three occasions in the interval around the speech moment, a different cigarette each time. The type mismatch sits at the eventive verb, so γ may apply only there, leaving the existential above the generic; that sole available reading is false, which is the oddness of (17a)/(45). The brand variant (17b) is the same shift with a constant witness, so its narrow reading is true and the sentence is fine.

@[reducible, inline]

abbrev Cohen2013.smokes : Fin 3 → Fin 3 → Prop

Mary smokes a different cigarette at each of three occasions.

Equations

• Cohen2013.smokes x1✝ x2✝ = (x1✝ = x2✝)

@[reducible, inline]

abbrev Cohen2013.inSpeechInterval : Fin 3 → Unit → Prop

Every occasion falls in the interval around the speech moment.

Equations

• Cohen2013.inSpeechInterval x✝¹ x✝ = True

def Cohen2013.cigaretteReading : Level → Prop

The two logical forms of the cigarette sentence, by level of the shift.

Equations

• Cohen2013.cigaretteReading Cohen2013.Level.word = ∃ (c : Fin 3), Cohen2013.gamma Cohen2013.inSpeechInterval (fun (e : Fin 3) => Cohen2013.smokes c e) ()
• Cohen2013.cigaretteReading Cohen2013.Level.phrase = Cohen2013.gamma Cohen2013.inSpeechInterval (fun (e : Fin 3) => ∃ (c : Fin 3), Cohen2013.smokes c e) ()

@[instance_reducible]

instance Cohen2013.instDecidableCigaretteReading (l : Level) : Decidable (cigaretteReading l)

Equations

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

theorem Cohen2013.cigaretteReading_word_ne_phrase : ¬cigaretteReading Level.word ∧ cigaretteReading Level.phrase

The two levels yield distinct readings: no one cigarette is smoked at most occasions, while each occasion has its cigarette.

theorem Cohen2013.cigarette_no_true_reading_available (l : Level) : Device.typeShift.AppliesAt l → ¬cigaretteReading l

The shift's locality leaves no true reading available, which is the oddness of the restrictorless habitual.

@[reducible, inline]

abbrev Cohen2013.smokesBrand : Fin 1 → Fin 3 → Prop

One brand, smoked at every occasion.

Equations

• Cohen2013.smokesBrand x✝¹ x✝ = True

theorem Cohen2013.brand_true_reading_available : ∃ (l : Level), Device.typeShift.AppliesAt l ∧ ∃ (b : Fin 1), gamma inSpeechInterval (fun (e : Fin 3) => smokesBrand b e) ()

With a constant witness the same local shift yields a true reading: the brand variant (17b) is fine.

Cows do not eat nettles (§13.2.1)

Five cows, one a nettle-eater. With focus on the object, the alternatives are the ways of eating and the generic scopes over negation: cows in general eat something other than nettles, exceptions tolerated ((9a)). With focus on the auxiliary, the scope is its own sole alternative, the generic is the trivially true refutation reading, and the negated sentence denies that any cow eats nettles — false here ((9b)).

@[reducible, inline]

abbrev Cohen2013.eatsNettles : Fin 5 → Prop

The one nettle-eating cow among five.

Equations

• Cohen2013.eatsNettles x✝ = (↑x✝ = 4)

@[reducible, inline]

abbrev Cohen2013.eatsSomething : Fin 5 → Prop

Every cow eats something, the disjunction of the alternatives under object focus.

Equations

• Cohen2013.eatsSomething x✝ = True

theorem Cohen2013.cows_gen_over_neg : Cohen1999.gen Finset.univ (fun (x : Fin 5) => True) eatsSomething fun (x : Fin 5) => ¬eatsNettles x

With object focus the generic scopes over negation, and most eating cows avoid nettles ((9a)).

theorem Cohen2013.cows_neg_over_gen_false : Cohen1999.gen Finset.univ (fun (x : Fin 5) => True) eatsNettles eatsNettles

With auxiliary focus negation scopes over the generic, whose refutation reading is true as long as one cow eats nettles, so the sentence is false ((9b)).