Nickel (2009): Generics and the Ways of Normality

This file formalizes the argument of [Nic09] from conjunctive generics against majority-based accounts of the generic operator. Elephants live in Africa and Asia is sentential conjunction, elephants live in Africa and elephants live in Asia, and is true although no majority of elephants lives in either place, so the probabilistic operator of [Coh99] predicts it false (cohen_fails_elephant_asia). Normality comes in ways: a characterizing sentence is true when there is a way of being normal in the respect the predicate determines such that every individual normal in that way satisfies the predicate (nickelGEN), so each conjunct of a conjunctive generic may draw on its own way (nickelConjunctiveGEN, nickel_handles_elephant_conjunction, bears_nickel_succeeds), and the ways are incompatible without the conjunction entailing that anything lives in both places (ways_incompatible).

Implementation notes

The ways are indices selecting the individuals that count as normal, the actual-extension proxy for the paper's respects of normality and its inductive targets; the counterfactual element the paper notes it needs when no individual is normal in a way is not represented, so the operator holds vacuously in that case. Each toy model is a finite type of entities, over which GEN is the type-level every. The comparison with Cohen's operator runs over one shared toy model, with the habitats as the alternative set.

References

• [Nic09]
• [Coh99]

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 : ℕ

@[instance_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 ⋯

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) " }"

@[instance_reducible]

instance Nickel2009.instReprNormalcyWay : Repr NormalcyWay

Equations

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

Nickel's GEN

GEN is the restricted universal every under an existential over normality ways, so the only apparatus specific to Nickel is the existential over ways.

def Nickel2009.nickelGEN {α : Type u_1} (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope : α → Prop) : Prop

Nickel's GEN with way-indexed normality holds when 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 normalIn ways restrictor scope = ∃ w ∈ ways, Quantifier.GQ.every (fun (e : α) => restrictor e ∧ normalIn e w) scope

def Nickel2009.nickelConjunctiveGEN {α : Type u_1} (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope scope' : α → Prop) : Prop

A conjunctive generic holds when both GEN[A][F₁] and GEN[A][F₂] hold, possibly through different normality ways.

Equations

• Nickel2009.nickelConjunctiveGEN normalIn ways restrictor scope scope' = (Nickel2009.nickelGEN normalIn ways restrictor scope ∧ Nickel2009.nickelGEN normalIn ways restrictor scope')

def Nickel2009.WaysIncompatible {α : Type u_1} (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) : Prop

Normality ways are pairwise incompatible when 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 normalIn ways = ∀ (e : α), ∀ w₁ ∈ ways, ∀ w₂ ∈ ways, w₁ ≠ w₂ → ¬(normalIn e w₁ ∧ normalIn e w₂)

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Nickel2009.instDecidableNickelConjunctiveGEN {α : Type u_1} (normalIn : α → NormalcyWay → Prop) (ways : Finset NormalcyWay) (restrictor scope scope' : α → Prop) [Fintype α] [DecidablePred restrictor] [DecidablePred scope] [DecidablePred scope'] [(w : NormalcyWay) → DecidablePred fun (x : α) => normalIn x w] : Decidable (nickelConjunctiveGEN normalIn ways restrictor scope scope')

Equations

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

@[instance_reducible]

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

Equations

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

The Elephant Example (2b/11)

@[reducible, inline]

abbrev Nickel2009.Elephant : Type

Ten elephants, six African (0–5) and four Asian (6–9).

Equations

• Nickel2009.Elephant = Fin 10

@[reducible, inline]

abbrev Nickel2009.isElephant : Elephant → Prop

Equations

• Nickel2009.isElephant x✝ = True

@[reducible, inline]

abbrev Nickel2009.livesInAfrica : Elephant → Prop

Equations

• Nickel2009.livesInAfrica x✝ = (x✝ < 6)

@[reducible, inline]

abbrev Nickel2009.livesInAsia : Elephant → Prop

Equations

• Nickel2009.livesInAsia x✝ = (6 ≤ x✝)

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 : Elephant → NormalcyWay → Prop

Normal in the African way are the African elephants, in the Asian way the Asian ones.

Equations

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

The Bears Example (2a)

@[reducible, inline]

abbrev Nickel2009.Bear : Type

Twenty bears across four continents, five each, with NA 0–4, SA 5–9, EU 10–14 and AS 15–19, so that each habitat is a quarter of the bears.

Equations

• Nickel2009.Bear = Fin 20

@[reducible, inline]

abbrev Nickel2009.isBear : Bear → Prop

Equations

• Nickel2009.isBear x✝ = True

@[reducible, inline]

abbrev Nickel2009.bearNA : Bear → Prop

Equations

• Nickel2009.bearNA x✝ = (x✝ < 5)

@[reducible, inline]

abbrev Nickel2009.bearSA : Bear → Prop

Equations

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

@[reducible, inline]

abbrev Nickel2009.bearEU : Bear → Prop

Equations

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

@[reducible, inline]

abbrev Nickel2009.bearAS : Bear → Prop

Equations

• Nickel2009.bearAS x✝ = (15 ≤ x✝)

@[reducible, inline]

abbrev Nickel2009.bearHabitat : Bear → Prop

The disjunction of the habitat alternatives, which every bear satisfies.

Equations

• Nickel2009.bearHabitat e = (Nickel2009.bearNA e ∨ Nickel2009.bearSA e ∨ Nickel2009.bearEU e ∨ Nickel2009.bearAS e)

def Nickel2009.bearWays : Finset NormalcyWay

Equations

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

@[reducible, inline]

abbrev Nickel2009.bearNormalIn : Bear → NormalcyWay → Prop

Equations

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

Key Theorems

theorem Nickel2009.nickel_handles_elephant_conjunction : nickelConjunctiveGEN elephantNormalIn ways isElephant livesInAfrica livesInAsia

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

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

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

theorem Nickel2009.ways_incompatible : WaysIncompatible elephantNormalIn ways ∧ WaysIncompatible bearNormalIn bearWays

Normality ways are pairwise incompatible in both toy models.

The majority view fails where Nickel's succeeds

The headline contrast is a theorem over a shared model citing the gen of [Coh99] directly, with the habitats as the alternative set. The majority view fails on the conjunction because the Asia conjunct has prevalence 4/10 < 1/2, while Nickel's view succeeds.

theorem Nickel2009.cohen_fails_elephant_asia : ¬Cohen1999.gen Finset.univ isElephant (fun (e : Elephant) => livesInAfrica e ∨ livesInAsia e) livesInAsia

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

theorem Nickel2009.cohen_fails_nickel_succeeds_on_conjunction : ¬Cohen1999.gen Finset.univ isElephant (fun (e : Elephant) => livesInAfrica e ∨ livesInAsia e) livesInAsia ∧ nickelConjunctiveGEN elephantNormalIn ways isElephant livesInAfrica livesInAsia

On the conjunctive generic over one shared model the majority view fails, Asia being a minority habitat, while Nickel's way-indexed view succeeds.

theorem Nickel2009.cohen_fails_all_bear_habitats : ¬Cohen1999.gen Finset.univ isBear bearHabitat bearNA ∧ ¬Cohen1999.gen Finset.univ isBear bearHabitat bearSA ∧ ¬Cohen1999.gen Finset.univ isBear bearHabitat bearEU ∧ ¬Cohen1999.gen Finset.univ isBear bearHabitat bearAS

The bears conjunction (2a) fails for the majority view on every conjunct, since each of the four habitats is a minority.

Connection to Traditional GEN

theorem Nickel2009.nickelGEN_singleton_iff {α : Type u_1} (normalIn : α → NormalcyWay → Prop) (w : NormalcyWay) (restrictor scope : α → Prop) : nickelGEN normalIn {w} restrictor scope ↔ Quantifier.GQ.every (fun (e : α) => restrictor e ∧ normalIn e w) scope

Nickel's GEN with a single normality way is the restricted universal of traditional GEN, ∀ x, restrictor x ∧ normalIn x w → scope x.