Asher & Pelletier 2013: generics as modal quantifiers

A characterizing generic φs ψ is ∀x(φ(x) > ψ(x)), with > the weak conditional of commonsense entailment: for each individual, ψ holds throughout the worlds where that individual is a normal φ, the conditional of a normality on worlds (Genericity.Normality.gen). Normality is selected per restrictor, so Birds fly and Penguins don't fly hold together, the normal Opus-penguin worlds not being normal Opus-bird worlds, which a fixed set of normal worlds cannot provide; and it has give: the teleological and the statistical construal disagree on whether turtles live to be a hundred. Against the probabilistic rival, on which a generic is true when the scope is more likely than not given the restrictor, the paper objects that a margin just over half verifies generics that are not true, and that embedded generics trivialize the account: under conditionalization the probability of the conditional collapses to that of the scope. Logical forms are then built by putting the focused material in the nuclear scope and its alternatives in the restrictor, which weakens the restrictor where needed (ducks lay eggs), lets a tautologous restrictor deliver an existential (firemen are available), and, with a further generic over circumstances, gives mosquitoes their disposition to carry the virus.

Item numbers follow the 2012 preprint.

Main definitions

• generic: the generic quantifier over a normality on worlds, whose conditional is the weak conditional.
• generic_disjoint, generic_inter: contrary generics select disjoint worlds; the scope weakens.
• normal_ofAccess_eq_empty, exists_bird_penguin: a fixed set of normal worlds leaves no normal penguin world once birds fly and penguins don't, while a normality from an ordering of worlds has one.
• existentialReading, gen_univ, doubleGeneric: the alternatives-based, the tautologous, and the circumstantial restrictor.
• Conditionalizes, cond_eq_of_conditionalizes: the trivialization of probabilistic generics.

References

• [AP13]
• [AM91], [AM95], [PA97] — the modal account
• [Coh99] — the probabilistic rival
• [Les08] — the counterexamples
• [Lew76], [Mil03] — the triviality argument

The modal quantifier

def AsherPelletier2013.generic {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) (φ ψ : E → Set W) (w : W) : Prop

The generic ∀x(φ(x) > ψ(x)) of (2) holds when each individual satisfies ψ throughout the worlds where it is a normal φ.

Equations

• AsherPelletier2013.generic n φ ψ w = ∀ (a : E), w ∈ n.gen (φ a) (ψ a)

theorem AsherPelletier2013.generic_disjoint {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) {φ φ' ψ : E → Set W} {w : W} (h : generic n φ ψ w) (h' : generic n φ' (fun (a : E) => (ψ a)ᶜ) w) (a : E) : Disjoint (n.normal w (φ a)) (n.normal w (φ' a))

Contrary generics select disjoint normal worlds for each individual: if birds fly and penguins don't, the normal Opus-penguin worlds are not normal Opus-bird worlds.

theorem AsherPelletier2013.generic_inter {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) {φ ψ χ : E → Set W} {w : W} (h : generic n φ (fun (a : E) => ψ a ∩ χ a) w) : generic n φ ψ w

A generic with a conjoined scope entails the generic with either conjunct.

theorem AsherPelletier2013.gen_univ {W : Type u_1} (n : Genericity.Normality W W) {w : W} (h : n.normal w Set.univ = {w}) (q : Set W) : w ∈ n.gen Set.univ q ↔ w ∈ q

With logical truths selecting the world of evaluation itself, a tautologous restrictor makes the conditional its consequent at that world.

theorem AsherPelletier2013.normal_ofAccess_eq_empty {W : Type u_1} {B : W → Set W} {bird penguin fly : Set W} {w : W} (hpb : penguin ⊆ bird) (hb : w ∈ (Genericity.Normality.ofAccess B).gen bird fly) (hp : w ∈ (Genericity.Normality.ofAccess B).gen penguin flyᶜ) : (Genericity.Normality.ofAccess B).normal w penguin = ∅

With a fixed set of normal worlds, Birds fly makes Opus fly in its normal penguin worlds, so with Penguins don't fly it has none ((7), (8)).

theorem AsherPelletier2013.exists_bird_penguin : ∃ (n : Genericity.Normality Bool Bool) (bird : Set Bool) (penguin : Set Bool) (fly : Set Bool), penguin ⊆ bird ∧ true ∈ n.gen bird fly ∧ true ∈ n.gen penguin flyᶜ ∧ (n.normal true penguin).Nonempty

With normality from an ordering of worlds, Birds fly and Penguins don't fly hold together and there is a normal Opus-penguin world, since the more normal world, where Opus is an ordinary bird and flies, is not a penguin world ((7), (8)).

def AsherPelletier2013.teleological : Genericity.Normality Bool Bool

On the teleological construal a turtle's normal worlds are those where it reaches a hundred.

Equations

• AsherPelletier2013.teleological = Genericity.Normality.ofAccess fun (x : Bool) => {true}

def AsherPelletier2013.statistical : Genericity.Normality Bool Bool

On the statistical construal a turtle's normal worlds are those where it dies young.

Equations

• AsherPelletier2013.statistical = Genericity.Normality.ofAccess fun (x : Bool) => {false}

theorem AsherPelletier2013.turtles (w : Bool) : w ∈ teleological.gen Set.univ {true} ∧ w ∉ statistical.gen Set.univ {true}

Turtles live to be 100 is true under the teleological construal and false under the statistical one.

Restrictors

def AsherPelletier2013.existentialReading {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) (Alt : Set (E → Set W)) (T : E → Set W) (c : E) (w : W) : Prop

The existential reading of Typhoons arise in this part of the Pacific: for every alternative property P of the place, normally P is the property that typhoons arise there.

Equations

• AsherPelletier2013.existentialReading n Alt T c w = ∀ P ∈ Alt, w ∈ n.gen (P c) {_v : W | P = T}

theorem AsherPelletier2013.existentialReading.normal_subset {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) {Alt : Set (E → Set W)} {T : E → Set W} {c : E} {w : W} (h : existentialReading n Alt T c w) {P : E → Set W} (hP : P ∈ Alt) : n.normal w (P c) ⊆ T c

An alternative that applies makes the reading defeasibly entail that typhoons arise there: throughout that alternative's normal worlds.

def AsherPelletier2013.doubleGeneric {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) {Ev : Type u_3} (φ : E → Set W) (C : Ev → Set W) (ψ : E → Ev → Set W) (w : W) : Prop

A double generic holds when for each individual, in its normal worlds, every appropriate circumstance normally has it carry the virus, a disposition rather than a frequency.

Equations

• AsherPelletier2013.doubleGeneric n φ C ψ w = AsherPelletier2013.generic n φ (fun (a : E) => {v : W | ∀ (e : Ev), v ∈ n.gen (C e) (ψ a e)}) w

theorem AsherPelletier2013.doubleGeneric_univ {W : Type u_1} {E : Type u_2} (n : Genericity.Normality W W) {Ev : Type u_3} (h : ∀ (v : W), n.normal v Set.univ = {v}) (φ : E → Set W) (ψ : E → Ev → Set W) (w : W) : doubleGeneric n φ (fun (x : Ev) => Set.univ) ψ w ↔ generic n φ (fun (a : E) => {v : W | ∀ (e : Ev), v ∈ ψ a e}) w

Without a circumstance restriction, and with logical truths selecting the world of evaluation, double genericity is ordinary genericity over every circumstance.

Against the probabilistic account

def AsherPelletier2013.tailed : Fin 20 → Prop

A cat has a tail in 11 of 20 equally normal cases, just over half.

Equations

• AsherPelletier2013.tailed w = (↑w < 11)

@[instance_reducible]

instance AsherPelletier2013.instDecidablePredFinOfNatNatTailed : DecidablePred tailed

Equations

• AsherPelletier2013.instDecidablePredFinOfNatNatTailed w = (↑w).decLt 11

theorem AsherPelletier2013.cohen_too_weak : Cohen1999.gen Finset.univ (fun (x : Fin 20) => True) (fun (x : Fin 20) => True) tailed ∧ 0 ∉ ⊤.gen Set.univ {w : Fin 20 | tailed w}

The majority account verifies Cats have tails on a margin just over half; the modal account with every case equally normal does not, since a normal case lacks a tail.

def AsherPelletier2013.Conditionalizes {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (a b c : Set Ω) : Prop

A proposition c for the conditional a > b conditionalizes when its probability given any d is that of b given a and d.

Equations

• AsherPelletier2013.Conditionalizes μ a b c = ∀ (d : Set Ω), MeasurableSet d → μ[c | d] = μ[b | a ∩ d]

theorem AsherPelletier2013.cond_eq_of_conditionalizes {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {a b c : Set Ω} (ha : MeasurableSet a) (hb : MeasurableSet b) (h : Conditionalizes μ a b c) (h₁ : μ (a ∩ b) ≠ 0) : μ[b | a] = μ b

Under conditionalization the probability of the scope given the restrictor is the probability of the scope, whenever the restrictor is compatible with the scope.

theorem AsherPelletier2013.cohen_iff_scope {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {a b c : Set Ω} (ha : MeasurableSet a) (hb : MeasurableSet b) (h : Conditionalizes μ a b c) (h₁ : μ (a ∩ b) ≠ 0) : 1 / 2 < μ[b | a] ↔ 1 / 2 < μ b

The probabilistic generic, under conditionalization, says only that the scope is more likely than not.