[Nic09]: Generics and the ways of normality

Bernhard Nickel, "Generics and the ways of normality", Linguistics and Philosophy 31 (2009), 629–648.

The Problem: Conjunctive Generics

Nickel criticizes majority-based views of generics (including [Coh99]'s probability-based GEN) by showing they cannot handle conjunctive generics like:

(2b) Elephants live in Africa and Asia.

If (2b) is equivalent to the sentential conjunction:

Elephants live in Africa AND Elephants live in Asia.

then a majority-based view would require both conjuncts to hold with prevalence > 0.5 over the same domain. But African elephants and Asian elephants are disjoint populations — most elephants can't live in BOTH places. So the majority view predicts the conjunction is false, contrary to speaker judgments. (Nickel's running example is the elephants (2b/11); example (2a), "Bears live in North America, South America, Europe, and Asia", is the more dramatic four-continent variant.)

Nickel's Solution: Ways of Being Normal

Nickel proposes that normality is not a single binary predicate but comes in multiple ways. For the elephant case:

• Way w₁: normal w.r.t. habitat → lives in Africa
• Way w₂: normal w.r.t. habitat → lives in Asia

GEN existentially quantifies over ways of being normal, then universally quantifies over the As that are normal in that way (p. 643):

G(A;F) is true iff there is a way w of being an F-normal A such that
all As that are w are F.

i.e. ∃w. ∀x. (A(x) ∧ normalIn(x, w)) → F(x). Conjunctive generics can then use different normality ways for each conjunct.

Nickel notes (p. 643) that these truth-conditions "don't account yet for a situation in which there aren't any F-normal As… we need to introduce a counterfactual element. However, for the purposes of this paper, we can ignore this complication." The formalization below inherits that: nickelGEN holds vacuously when no entity is normal in any way. The way-existential is modeled by its actual-extension proxy (the modal/inductive-target content of "a respect of normality" is abstracted away).

Ways of Being Normal

structure Nickel2009.NormalcyWay : Type

A way of being normal — an index selecting which entities count as "normal" for a given generalization. Different generic claims can appeal to different normality ways.

• id : ℕ

@[implicit_reducible]

instance Nickel2009.instDecidableEqNormalcyWay : DecidableEq NormalcyWay

Equations

• Nickel2009.instDecidableEqNormalcyWay = Nickel2009.instDecidableEqNormalcyWay.decEq

def Nickel2009.instDecidableEqNormalcyWay.decEq (x✝ x✝¹ : NormalcyWay) : Decidable (x✝ = x✝¹)

Equations

• Nickel2009.instDecidableEqNormalcyWay.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Nickel2009.instReprNormalcyWay : Repr NormalcyWay

Equations

• Nickel2009.instReprNormalcyWay = { reprPrec := Nickel2009.instReprNormalcyWay.repr }

def Nickel2009.instReprNormalcyWay.repr : NormalcyWay → ℕ → Std.Format

Equations

• Nickel2009.instReprNormalcyWay.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

structure Nickel2009.Entity : Type

An entity in the domain of a generic.

• id : ℕ

@[implicit_reducible]

instance Nickel2009.instDecidableEqEntity : DecidableEq Entity

Equations

• Nickel2009.instDecidableEqEntity = Nickel2009.instDecidableEqEntity.decEq

def Nickel2009.instDecidableEqEntity.decEq (x✝ x✝¹ : Entity) : Decidable (x✝ = x✝¹)

Equations

• Nickel2009.instDecidableEqEntity.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Nickel2009.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

• Nickel2009.instReprEntity.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

@[implicit_reducible]

instance Nickel2009.instReprEntity : Repr Entity

Equations

• Nickel2009.instReprEntity = { reprPrec := Nickel2009.instReprEntity.repr }

Nickel's GEN

GEN as everyOn (the relativized restricted universal) under an existential over normality ways — Quantification.everyOn is the canonical generalized quantifier, so the only Nickel-specific apparatus is the ∃-over-ways wrapper.

def Nickel2009.nickelGEN {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope : α → Prop) [DecidablePred restrictor] [DecidablePred scope] [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : Prop

Nickel's GEN with way-indexed normality: there is a way of being normal such that every entity normal in that way (and satisfying the restrictor) satisfies the scope. The existential over ways lets different conjuncts of a conjunctive generic use different ways.

Equations

• Nickel2009.nickelGEN entities normalIn ways restrictor scope = ∃ w ∈ ways, Quantification.everyOn entities (fun (e : α) => restrictor e ∧ normalIn e w) scope

@[implicit_reducible]

instance Nickel2009.instDecidableNickelGEN {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope : α → Prop) [DecidablePred restrictor] [DecidablePred scope] [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : Decidable (nickelGEN entities normalIn ways restrictor scope)

Equations

• Nickel2009.instDecidableNickelGEN entities normalIn ways restrictor scope = id inferInstance

def Nickel2009.nickelConjunctiveGEN {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope1 scope2 : α → Prop) [DecidablePred restrictor] [DecidablePred scope1] [DecidablePred scope2] [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : Prop

Conjunctive generic: both GEN[A][F₁] and GEN[A][F₂] hold, potentially via different normality ways.

Equations

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

@[implicit_reducible]

instance Nickel2009.instDecidableNickelConjunctiveGEN {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope1 scope2 : α → Prop) [DecidablePred restrictor] [DecidablePred scope1] [DecidablePred scope2] [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : Decidable (nickelConjunctiveGEN entities normalIn ways restrictor scope1 scope2)

Equations

• Nickel2009.instDecidableNickelConjunctiveGEN entities normalIn ways restrictor scope1 scope2 = id inferInstance

def Nickel2009.waysIncompatible {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : Prop

Normality ways are pairwise incompatible: no entity is normal in two distinct ways. The paper (p. 643) states this holds "usually (perhaps always)"; here it is a property of the toy model, not a commitment of the account.

Equations

• Nickel2009.waysIncompatible entities normalIn ways = ∀ e ∈ entities, ∀ w₁ ∈ ways, ∀ w₂ ∈ ways, w₁ ≠ w₂ → ¬(normalIn e w₁ ∧ normalIn e w₂)

@[implicit_reducible]

instance Nickel2009.instDecidableWaysIncompatible {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : Decidable (waysIncompatible entities normalIn ways)

Equations

• Nickel2009.instDecidableWaysIncompatible entities normalIn ways = id inferInstance

The Elephant Example (2b/11)

def Nickel2009.elephants : Finset Entity

10 elephants: 6 African (ids 0–5), 4 Asian (ids 6–9).

Equations

• Nickel2009.elephants = (List.map (fun (n : ℕ) => { id := n }) (List.range 10)).toFinset

@[reducible, inline]

abbrev Nickel2009.isElephant : Entity → Prop

Equations

• Nickel2009.isElephant x✝ = True

@[reducible, inline]

abbrev Nickel2009.livesInAfrica : Entity → Prop

Equations

• Nickel2009.livesInAfrica e = (e.id < 6)

@[reducible, inline]

abbrev Nickel2009.livesInAsia : Entity → Prop

Equations

• Nickel2009.livesInAsia e = (e.id ≥ 6)

def Nickel2009.africanWay : NormalcyWay

Equations

• Nickel2009.africanWay = { id := 1 }

def Nickel2009.asianWay : NormalcyWay

Equations

• Nickel2009.asianWay = { id := 2 }

def Nickel2009.ways : Finset NormalcyWay

Equations

• Nickel2009.ways = {Nickel2009.africanWay, Nickel2009.asianWay}

@[reducible, inline]

abbrev Nickel2009.elephantNormalIn : Entity → NormalcyWay → Prop

Normal in the African way = African elephants; in the Asian way = Asian.

Equations

• Nickel2009.elephantNormalIn e w = (w.id = 1 ∧ e.id < 6 ∨ w.id = 2 ∧ e.id ≥ 6)

The Bears Example (2a)

def Nickel2009.bears : Finset Entity

20 bears across 4 continents (5 each): NA 0–4, SA 5–9, EU 10–14, AS 15–19. The majority view fails for ALL four habitat conjuncts (each is 5/20 = 25%).

Equations

• Nickel2009.bears = (List.map (fun (n : ℕ) => { id := n }) (List.range 20)).toFinset

@[reducible, inline]

abbrev Nickel2009.isBear : Entity → Prop

Equations

• Nickel2009.isBear x✝ = True

@[reducible, inline]

abbrev Nickel2009.bearNA : Entity → Prop

Equations

• Nickel2009.bearNA e = (e.id < 5)

@[reducible, inline]

abbrev Nickel2009.bearSA : Entity → Prop

Equations

• Nickel2009.bearSA e = (e.id ≥ 5 ∧ e.id < 10)

@[reducible, inline]

abbrev Nickel2009.bearEU : Entity → Prop

Equations

• Nickel2009.bearEU e = (e.id ≥ 10 ∧ e.id < 15)

@[reducible, inline]

abbrev Nickel2009.bearAS : Entity → Prop

Equations

• Nickel2009.bearAS e = (e.id ≥ 15)

def Nickel2009.bearWays : Finset NormalcyWay

Equations

• Nickel2009.bearWays = {{ id := 1 }, { id := 2 }, { id := 3 }, { id := 4 }}

@[reducible, inline]

abbrev Nickel2009.bearNormalIn : Entity → NormalcyWay → Prop

Equations

• Nickel2009.bearNormalIn e w = (w.id = 1 ∧ e.id < 5 ∨ w.id = 2 ∧ e.id ≥ 5 ∧ e.id < 10 ∨ w.id = 3 ∧ e.id ≥ 10 ∧ e.id < 15 ∨ w.id = 4 ∧ e.id ≥ 15)

Key Theorems

theorem Nickel2009.nickel_handles_elephant_conjunction : nickelConjunctiveGEN elephants elephantNormalIn ways isElephant livesInAfrica livesInAsia

Nickel's view succeeds for the elephant conjunction: Africa is witnessed by the African way, Asia by the Asian way.

theorem Nickel2009.bears_nickel_succeeds : nickelGEN bears bearNormalIn bearWays isBear bearNA ∧ nickelGEN bears bearNormalIn bearWays isBear bearSA ∧ nickelGEN bears bearNormalIn bearWays isBear bearEU ∧ nickelGEN bears bearNormalIn bearWays isBear bearAS

The bears example (2a): Nickel's view succeeds for all four habitat conjuncts.

theorem Nickel2009.ways_incompatible : waysIncompatible elephants elephantNormalIn ways ∧ waysIncompatible bears bearNormalIn bearWays

Normality ways are pairwise incompatible in both toy models.

The majority view fails where Nickel's succeeds

The headline contrast, now a theorem over a shared model citing [Coh99]'s cohenGEN directly (not a local re-implementation). The majority view fails on the conjunction because the Asia conjunct has prevalence 4/10 < 1/2; Nickel's view succeeds. Per the chronology rule this comparison lives in the later paper (Nickel 2009 > Cohen 1999), which is the one that draws it.

theorem Nickel2009.cohen_fails_elephant_asia : ¬Cohen1999.cohenGEN elephants isElephant livesInAsia

Cohen's majority GEN is false for "Elephants live in Asia" (prevalence 4/10).

theorem Nickel2009.cohen_fails_nickel_succeeds_on_conjunction : ¬Cohen1999.cohenGEN elephants isElephant livesInAsia ∧ nickelConjunctiveGEN elephants elephantNormalIn ways isElephant livesInAfrica livesInAsia

Cohen vs Nickel on the conjunctive generic, over one shared model. The majority view fails (Asia is a minority habitat) while Nickel's way-indexed view succeeds — exactly the divergence Nickel's paper draws against Cohen.

theorem Nickel2009.cohen_fails_all_bear_habitats : ¬Cohen1999.cohenGEN bears isBear bearNA ∧ ¬Cohen1999.cohenGEN bears isBear bearSA ∧ ¬Cohen1999.cohenGEN bears isBear bearEU ∧ ¬Cohen1999.cohenGEN bears isBear bearAS

The bears conjunction (2a) fails even harder for the majority view: every one of the four habitats is a 25% minority.

Connection to Traditional GEN

theorem Nickel2009.nickel_single_way_is_everyOn {α : Type u_1} (entities : Finset α) (normalIn : α → NormalcyWay → Prop) (w : NormalcyWay) (restrictor scope : α → Prop) [DecidablePred restrictor] [DecidablePred scope] [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : nickelGEN entities normalIn {w} restrictor scope ↔ Quantification.everyOn entities (fun (e : α) => restrictor e ∧ normalIn e w) scope

Nickel's GEN with a single normality way reduces to the relativized restricted universal everyOn (traditional GEN): the way-existential is trivial, leaving ∀ x. (restrictor(x) ∧ normalIn(x, w)) → scope(x).

Generic-quantifier interface

theorem Nickel2009.nickelGEN_univ_eq_genWays {α : Type u_1} [Fintype α] (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (R S : α → Prop) [DecidablePred R] [DecidablePred S] [(w : NormalcyWay) → DecidablePred fun (e : α) => normalIn e w] : nickelGEN Finset.univ normalIn ways R S ↔ Quantification.genWays normalIn ways R S

Nickel's nickelGEN over the whole carrier is exactly the ways-of-normality generalized quantifier Quantification.genWays — its GQ-interface form, the [Nic09] instance of the shared schema in Quantification.Generic.

Summary: Three Views of Normality

View	Normality	GEN formula	Handles elephants?
[Coh99]	Probability > 0.5	P(Q|P) > 0.5	No
[Nic09]	Ways of being normal	∃w. ∀x. (A(x) ∧ normal(x,w)) → Q(x)	Yes

Cohen's probability view is formalized in Studies/Cohen1999.lean; the divergence on conjunctive generics is cohen_fails_nickel_succeeds_on_conjunction above.