Asher & Pelletier (2013): More Truths about Generic Truth

[AP13] (ch. 12 of Genericity, Mari, Beyssade & Del Prete eds., OUP) defends the modal-quantifier analysis of generics of [AM95] and [PA97] — "φs ψ" is ∀x(φ(x) > ψ(x)), with > the weak conditional of [AM91]'s commonsense entailment — refined so that the consequent is evaluated per individual: for each a, in the worlds where a is a normal φ. Here that is rendered as restrictor-indexed normality orderings — each restrictor class carries its own Preorder, and a generic holds iff its scope holds throughout Normality.optimal of its restrictor's ordering. Covers §12.3–12.4; the chapter's accommodation and double-genericity machinery (§12.6, §12.8) is not formalized.

Per-individual evaluation (§12.3, exx. 7–8)

For ∀x(φ(x) > ψ(x)), the consequent ψ is evaluated for each individual a at the worlds where a is a normal φ — under the normality ordering of a's restrictor class.

def AsherPelletier2013.birdDomain : Set TweetyNixon.TweetyWorld

Worlds in which Opus is a bird (all of them, by taxonomy).

Equations

• AsherPelletier2013.birdDomain = {w : TweetyNixon.TweetyWorld | TweetyNixon.isBird w}

def AsherPelletier2013.penguinDomain : Set TweetyNixon.TweetyWorld

Worlds in which Opus is a penguin.

Equations

• AsherPelletier2013.penguinDomain = {w : TweetyNixon.TweetyWorld | TweetyNixon.isPenguin w}

@[reducible]

def AsherPelletier2013.birdNormality : Preorder TweetyNixon.TweetyWorld

Bird-normality: the bird default "birds fly" processed into the ordering.

Equations

• AsherPelletier2013.birdNormality = Core.Order.Normality.refine Core.Order.Normality.total TweetyNixon.flies

@[reducible]

def AsherPelletier2013.penguinNormality : Preorder TweetyNixon.TweetyWorld

Penguin-normality: the penguin default "penguins don't fly" processed into the ordering.

Equations

• AsherPelletier2013.penguinNormality = Core.Order.Normality.refine Core.Order.Normality.total fun (x : TweetyNixon.TweetyWorld) => ¬TweetyNixon.flies x

theorem AsherPelletier2013.birds_fly (w : TweetyNixon.TweetyWorld) : w ∈ Core.Order.Normality.optimal birdNormality birdDomain → TweetyNixon.flies w

Ex. (8): "Birds fly" — Opus flies throughout the normal Opus-bird worlds.

theorem AsherPelletier2013.penguins_dont_fly (w : TweetyNixon.TweetyWorld) : w ∈ Core.Order.Normality.optimal penguinNormality penguinDomain → ¬TweetyNixon.flies w

Ex. (7): "Penguins don't fly" — Opus is grounded throughout the normal Opus-penguin worlds. With birds_fly, both generics hold simultaneously: they are evaluated at different normal-world sets.

theorem AsherPelletier2013.normal_penguin_not_normal_bird : Disjoint (Core.Order.Normality.optimal penguinNormality penguinDomain) (Core.Order.Normality.optimal birdNormality birdDomain)

"The normal Opus-penguin worlds are not normal Opus-bird worlds": the two evaluation sets are disjoint, so neither generic disturbs the other.

Contextual construals of normality (§12.3, ex. 9)

"Turtles live to be 100" is true under the Aristotelian/teleological construal and false under the statistical one: the "give" in what counts as a normal world sits in the choice of ordering, fixed by context and discourse.

inductive AsherPelletier2013.TurtleWorld : Type

Tim the turtle's possible fates.

• reachesCentury : TurtleWorld
• diesYoung : TurtleWorld

@[instance_reducible]

instance AsherPelletier2013.instDecidableEqTurtleWorld : DecidableEq TurtleWorld

Equations

• AsherPelletier2013.instDecidableEqTurtleWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AsherPelletier2013.livesTo100 : TurtleWorld → Prop

Tim lives to be 100 in this world.

Equations

• AsherPelletier2013.livesTo100 AsherPelletier2013.TurtleWorld.reachesCentury = True
• AsherPelletier2013.livesTo100 AsherPelletier2013.TurtleWorld.diesYoung = False

@[reducible]

def AsherPelletier2013.teleological : Preorder TurtleWorld

Teleological construal: promotes telos-fulfilling worlds.

Equations

• AsherPelletier2013.teleological = Core.Order.Normality.refine Core.Order.Normality.total AsherPelletier2013.livesTo100

@[reducible]

def AsherPelletier2013.statistical : Preorder TurtleWorld

Statistical construal: promotes the statistically typical early death.

Equations

• AsherPelletier2013.statistical = Core.Order.Normality.refine Core.Order.Normality.total fun (x : AsherPelletier2013.TurtleWorld) => ¬AsherPelletier2013.livesTo100 x

theorem AsherPelletier2013.turtles_teleological_true (w : TurtleWorld) : w ∈ Core.Order.Normality.optimal teleological Set.univ → livesTo100 w

Under the teleological construal the generic is true.

theorem AsherPelletier2013.turtles_statistical_false : ¬∀ w ∈ Core.Order.Normality.optimal statistical Set.univ, livesTo100 w

Under the statistical construal the same generic is false.

Against the probabilistic account (§12.4)

The "too weak" argument against [Coh99]'s Pr(ψ | φ) > 1/2 semantics: a margin just over half — the chapter's cats have tails in 50.05% of the normal cases, its coin comes up heads 50.000000001% of the time — verifies a generic the modal account rejects, since the normal cases do not settle the scope.

def AsherPelletier2013.tailed : Fin 20 → Prop

Tails in 11 of the 20 equally normal cat-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.cohenGEN Finset.univ (fun (x : Fin 20) => True) tailed ∧ ¬∀ w ∈ Core.Order.Normality.optimal Core.Order.Normality.total Set.univ, tailed w

Cohen's majority GEN verifies "Cats have tails", but the generic fails on the modal account: some normal case lacks tails.