Cohen (1999): Think Generic!

Cohen's inductivist semantics makes a generic sentence a probability judgment: gen(ψ, φ) is true iff the conditional probability of the scope, given the restrictor and the disjunction of a set of alternatives to the scope, exceeds one half (definition 1, p. 37). "Mammals bear live young" is evaluated over the mammals that procreate in some way, so no majority among all mammals is required, and Thomason's "People have a hard time finding CMU" is evaluated over the people who sought it. Generics are further ambiguous between this absolute reading and a relative one whose threshold is the average probability of the scope over the alternatives; the relative reading verifies "Bulgarians are good weightlifters" and, since its threshold depends on individuals outside the restrictor, it is not conservative (definition 3, pp. 55–56). The probability is a relative frequency in the limit, which imposes two constraints. The reference class may not be explicitly bounded (§4.4.2), and it must be homogeneous: unrestricted homogeneity is degenerate, since partitioning by the scope itself separates any mixed reference class (definition 4 and Salmon's argument, pp. 81–82), so the final truth conditions demand the majority within every inhabited cell of every salient partition of the restrictor (definition 5, p. 83). "Mammals are female" then fails under the sex partition however many mammals are female (§4.4.6). Frequency adverbs apply other thresholds to the same conditional probability — always 1, never 0, sometimes non-zero, usually the same one half as gen — and respect only the temporal partition, which is why "Primary school teachers are usually female" is true while the bare generic is not (definition 10, p. 128; §6.2.3).

We state the three definitions over finite models, derive the degeneracy of unrestricted homogeneity, the conservativity of the absolute reading and a non-conservativity witness for the relative one, the recovery of the relativized classical quantifiers at the frequency-adverb thresholds, and the paper's key examples.

Implementation notes

Page and definition numbers follow the CSLI edition, a light revision of the 1996 dissertation that renames its independent and dependent readings absolute and relative. The alternative set enters the truth conditions only through its extensional disjunction and the relative threshold, so it is carried as a single predicate. A conditional probability is the uniform measure on the reference class at the scope; with an empty reference class it is undefined in the paper (p. 37, §5.6) and 0 here, so gen is false there and decidable through its count form, and a salient cell with an empty reference class imposes no condition.

TODO

• The unboundedness constraint (§4.4.2) and lawlikeness (§4.4.3) restrict which sentences express generics at all — a matter of reference classes conceivable as unlimited, with no content over a fixed finite model — and are not stated.
• Chapter 5's calculus of alternatives (absolute determinables, focus, the connectives) and chapter 7's default reasoning are not formalized; the alternative set is taken as given, as in §3.2.

References

• A. Cohen, Think Generic! The Meaning and Use of Generic Sentences (1999)
• W. C. Salmon, Objectively Homogeneous Reference Classes (1977)
• R. Thomason, Theories of Nonmonotonicity and Natural Language Generics (1988)
• G. N. Carlson, Reference to Kinds in English (1977)

def Cohen1999.gen {α : Type u_1} [MeasurableSpace α] (domain : Finset α) (ψ alt φ : α → Prop) [DecidablePred ψ] [DecidablePred alt] : Prop

Cohen's generic quantifier on its absolute reading (definition 1, p. 37) holds when the conditional probability of the scope φ, given the restrictor ψ and the disjunction alt of the alternatives to the scope, exceeds one half.

Equations

• Cohen1999.gen domain ψ alt φ = (2⁻¹ < (ProbabilityTheory.uniformOn ↑({x ∈ domain | ψ x ∧ alt x})) {x : α | φ x})

def Cohen1999.genRelative {α : Type u_1} [MeasurableSpace α] (domain : Finset α) (ψ alt φ : α → Prop) [DecidablePred ψ] [DecidablePred alt] : Prop

The relative reading (definition 3, p. 56) holds when the restrictor raises the probability of the scope above its average over the alternatives.

Equations

• Cohen1999.genRelative domain ψ alt φ = ((ProbabilityTheory.uniformOn ↑(Finset.filter alt domain)) {x : α | φ x} < (ProbabilityTheory.uniformOn ↑({x ∈ domain | ψ x ∧ alt x})) {x : α | φ x})

def Cohen1999.genSalient {α : Type u_1} [MeasurableSpace α] (domain : Finset α) (ψ alt φ : α → Prop) [DecidablePred ψ] [DecidablePred alt] {ι : Type u_2} (cells : ι → α → Prop) [(i : ι) → DecidablePred (cells i)] : Prop

The final truth conditions (definition 5, p. 83) ask for the absolute threshold within every salient cell whose reference class is inhabited.

Equations

• Cohen1999.genSalient domain ψ alt φ cells = ∀ (i : ι), {x ∈ domain | (ψ x ∧ cells i x) ∧ alt x}.Nonempty → Cohen1999.gen domain (fun (x : α) => ψ x ∧ cells i x) alt φ

def Cohen1999.freq {α : Type u_1} [MeasurableSpace α] (domain : Finset α) (ψ alt φ : α → Prop) [DecidablePred ψ] [DecidablePred alt] (R : ENNReal → Prop) : Prop

A frequency adverb applies its lexical requirement to the same conditional probability (definition 10, p. 128); gen carries the requirement (2⁻¹ < ·), synonymous with usually.

Equations

• Cohen1999.freq domain ψ alt φ R = R ((ProbabilityTheory.uniformOn ↑({x ∈ domain | ψ x ∧ alt x})) {x : α | φ x})

def Cohen1999.Homogeneous {α : Type u_1} [MeasurableSpace α] (domain : Finset α) (ψ φ : α → Prop) [DecidablePred ψ] : Prop

Unrestricted homogeneity (definition 4, p. 81, after Salmon) holds when every inhabited sub-reference class preserves the conditional probability of the scope.

Equations

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

Probabilities on a finite reference class

The absolute reading and the majority quantifier

theorem Cohen1999.gen_iff_card {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] [DecidablePred φ] : gen domain ψ alt φ ↔ {x ∈ domain | ψ x ∧ alt x}.card < 2 * (Finset.filter φ ({x ∈ domain | ψ x ∧ alt x})).card

The absolute reading in division-free form, false on an empty reference class.

@[instance_reducible]

instance Cohen1999.instDecidableGen {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] [DecidablePred φ] : Decidable (gen domain ψ alt φ)

Equations

• Cohen1999.instDecidableGen = decidable_of_iff ({x ∈ domain | ψ x ∧ alt x}.card < 2 * (Finset.filter φ ({x ∈ domain | ψ x ∧ alt x})).card) ⋯

theorem Cohen1999.genRelative_iff_card {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] [DecidablePred φ] (hA : (Finset.filter alt domain).Nonempty) (hR : {x ∈ domain | ψ x ∧ alt x}.Nonempty) : genRelative domain ψ alt φ ↔ (Finset.filter φ (Finset.filter alt domain)).card * {x ∈ domain | ψ x ∧ alt x}.card < (Finset.filter φ ({x ∈ domain | ψ x ∧ alt x})).card * (Finset.filter alt domain).card

The relative reading in division-free, kernel-decidable form.

theorem Cohen1999.gen_iff_most {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] [DecidablePred φ] : gen domain ψ alt φ ↔ Quantifier.GQ.most (fun (x : α) => x ∈ domain ∧ ψ x ∧ alt x) φ

The absolute reading is the majority quantifier on the restricted domain.

theorem Cohen1999.gen_iff_freq {α : Type u_1} [MeasurableSpace α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] : gen domain ψ alt φ ↔ freq domain ψ alt φ fun (x : ENNReal) => 2⁻¹ < x

gen is the adverb usually (definition 10, p. 128; p. 131).

theorem Cohen1999.gen_conservativity {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] [DecidablePred φ] : (gen domain ψ alt fun (x : α) => ψ x ∧ φ x) ↔ gen domain ψ alt φ

The absolute reading is conservative: intersecting the scope with the restrictor changes nothing (p. 54, after Wilkinson).

theorem Cohen1999.gen_self {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ φ : α → Prop} [DecidablePred ψ] [DecidablePred φ] (hR : {x ∈ domain | ψ x ∧ φ x}.Nonempty) : gen domain ψ φ φ

A generic whose scope exhausts its alternatives is true on any inhabited reference class, the reading of refutation statements, whose negation denies existence (§5.7).

The generalized-quantifier interface

Over the whole carrier with trivial alternatives the absolute reading is the majority generalized quantifier, hence proportional: its truth depends only on the two cell counts. The relativized readings are exactly what departs from this.

theorem Cohen1999.gen_univ_iff_most {β : Type u_2} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] (R S : β → Prop) [DecidablePred R] [DecidablePred S] : gen Finset.univ R (fun (x : β) => True) S ↔ Quantifier.GQ.most R S

With trivial alternatives over the whole carrier, gen is most.

theorem Cohen1999.gen_proportional {β : Type u_2} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] : Quantifier.GQ.Proportional fun (R S : β → Prop) => gen Finset.univ R (fun (x : β) => True) S

With trivial alternatives over the whole carrier, gen is proportional ([PW06]), a property of this operator that the genericity literature's counterexamples to majority accounts target.

Homogeneity is degenerate unrestricted (definition 4, p. 82)

theorem Cohen1999.homogeneous_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ φ : α → Prop} [DecidablePred ψ] [DecidablePred φ] (hR : (Finset.filter ψ domain).Nonempty) : Homogeneous domain ψ φ ↔ Quantifier.GQ.no (fun (x : α) => x ∈ domain ∧ ψ x) φ ∨ Quantifier.GQ.every (fun (x : α) => x ∈ domain ∧ ψ x) φ

Salmon's two trivial cases are the only homogeneous reference classes: partitioning by the scope itself separates any mixed one (p. 82). Hence definition 5 restricts the partitions to the salient ones.

Frequency adverbs (definition 10, p. 128)

At the extreme thresholds the restricted classical quantifiers reappear; sometimes is the existential, so a generic over an empty reference class entails nothing (§5.6).

theorem Cohen1999.freq_eq_one_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] (hR : {x ∈ domain | ψ x ∧ alt x}.Nonempty) : (freq domain ψ alt φ fun (x : ENNReal) => x = 1) ↔ Quantifier.GQ.every (fun (x : α) => x ∈ domain ∧ ψ x ∧ alt x) φ

Always, probability 1, is the restricted universal.

theorem Cohen1999.freq_eq_zero_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] : (freq domain ψ alt φ fun (x : ENNReal) => x = 0) ↔ Quantifier.GQ.no (fun (x : α) => x ∈ domain ∧ ψ x ∧ alt x) φ

Never, probability 0, is the restricted no.

theorem Cohen1999.freq_pos_iff {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {domain : Finset α} {ψ alt φ : α → Prop} [DecidablePred ψ] [DecidablePred alt] : (freq domain ψ alt φ fun (x : ENNReal) => 0 < x) ↔ Quantifier.GQ.some (fun (x : α) => x ∈ domain ∧ ψ x ∧ alt x) φ

Sometimes, positive probability, is the restricted existential.

People have a hard time finding CMU (§3.2.1, after Thomason)

Twenty people, five of whom sought the university: four found it with difficulty, one with ease. The alternatives — the levels of difficulty of the search — restrict the reference class to the seekers, so the generic holds with no majority among people.

@[reducible, inline]

abbrev Cohen1999.soughtCMU : Fin 20 → Prop

Equations

• Cohen1999.soughtCMU x✝ = (↑x✝ < 5)

@[reducible, inline]

abbrev Cohen1999.hardTime : Fin 20 → Prop

Equations

• Cohen1999.hardTime x✝ = (↑x✝ < 4)

theorem Cohen1999.cmu_gen : gen Finset.univ (fun (x : Fin 20) => True) soughtCMU hardTime

theorem Cohen1999.cmu_no_majority : ¬gen Finset.univ (fun (x : Fin 20) => True) (fun (x : Fin 20) => True) hardTime

Mammals bear live young; mammals are not female (§3.2.1 p. 33, §4.4.6 p. 91)

Twenty mammals, eight of which procreate: six bear live young, two lay eggs. Eleven are female, among them every procreator. Relativized to the forms of procreation, the first generic is true though bearers are a minority of all mammals, and the male cell of the sex partition is empty of procreators, so definition 5 agrees. The second clears definition 1 on the female majority alone but fails definition 5, since the male cell is inhabited and contains no female — the paper's resolution of the contrast with different alternatives and the sex partition. By definition 10 the same threshold read as the adverb usually ignores the non-temporal partition (§6.2.3), so "usually female" stays true.

@[reducible, inline]

abbrev Cohen1999.procreates : Fin 20 → Prop

Equations

• Cohen1999.procreates x✝ = (↑x✝ < 8)

@[reducible, inline]

abbrev Cohen1999.bearsLive : Fin 20 → Prop

Equations

• Cohen1999.bearsLive x✝ = (↑x✝ < 6)

@[reducible, inline]

abbrev Cohen1999.female : Fin 20 → Prop

Equations

• Cohen1999.female x✝ = (↑x✝ < 11)

@[reducible, inline]

abbrev Cohen1999.sexCell : Bool → Fin 20 → Prop

The sex partition divides the females from the males.

Equations

• Cohen1999.sexCell b x = if b = true then Cohen1999.female x else ¬Cohen1999.female x

theorem Cohen1999.bearsLive_gen : gen Finset.univ (fun (x : Fin 20) => True) procreates bearsLive

theorem Cohen1999.bearsLive_no_majority : ¬gen Finset.univ (fun (x : Fin 20) => True) (fun (x : Fin 20) => True) bearsLive

theorem Cohen1999.bearsLive_genSalient : genSalient Finset.univ (fun (x : Fin 20) => True) procreates bearsLive sexCell

theorem Cohen1999.female_gen : gen Finset.univ (fun (x : Fin 20) => True) (fun (x : Fin 20) => True) female

theorem Cohen1999.female_not_genSalient : ¬genSalient Finset.univ (fun (x : Fin 20) => True) (fun (x : Fin 20) => True) female sexCell

Relative readings (§3.4.3–3.4.4, pp. 54–56)

Twenty people, fifteen of them weightlifters: the five Bulgarians all lift, two of them well; one of the ten other lifters is good. A Bulgarian lifter is likelier than an arbitrary one to be good, though no majority of Bulgarian lifters is. In the soccer variant, where the lousy players concentrate outside Brazil, the relative reading correctly rejects "Brazilians are lousy soccer players" yet accepts the sentence with its scope intersected with the restrictor, whose average is lower — so the reading is not conservative.

@[reducible, inline]

abbrev Cohen1999.bulgarian : Fin 20 → Prop

Equations

• Cohen1999.bulgarian x✝ = (↑x✝ < 5)

@[reducible, inline]

abbrev Cohen1999.lifter : Fin 20 → Prop

Equations

• Cohen1999.lifter x✝ = (↑x✝ < 15)

@[reducible, inline]

abbrev Cohen1999.goodLifter : Fin 20 → Prop

Equations

• Cohen1999.goodLifter x = (↑x < 2 ∨ ↑x = 5)

theorem Cohen1999.bulgarians_relative : genRelative Finset.univ bulgarian lifter goodLifter

theorem Cohen1999.bulgarians_not_absolute : ¬gen Finset.univ bulgarian lifter goodLifter

@[reducible, inline]

abbrev Cohen1999.brazilian : Fin 20 → Prop

Equations

• Cohen1999.brazilian x✝ = (↑x✝ < 5)

@[reducible, inline]

abbrev Cohen1999.soccerPlayer : Fin 20 → Prop

Equations

• Cohen1999.soccerPlayer x✝ = (↑x✝ < 15)

@[reducible, inline]

abbrev Cohen1999.lousy : Fin 20 → Prop

Equations

• Cohen1999.lousy x = (↑x = 0 ∨ 5 ≤ ↑x ∧ ↑x < 13)

theorem Cohen1999.brazilians_relative_rejected : ¬genRelative Finset.univ brazilian soccerPlayer lousy

theorem Cohen1999.genRelative_not_conservative : ¬((genRelative Finset.univ brazilian soccerPlayer fun (x : Fin 20) => brazilian x ∧ lousy x) ↔ genRelative Finset.univ brazilian soccerPlayer lousy)

The relative reading is not conservative (p. 55): intersecting the scope with the restrictor flips the verdict.