@cite{asher-pelletier-2012} — More Truths about Generic Truth

Nicholas Asher and Francis Jeffry Pelletier, ch. 12 of Genericity (Mari, Beyssade, Del Prete eds.), OUP, Oxford Studies in Theoretical Linguistics 43.

Core Claim

Generics should be analyzed as modal quantifiers — ∀x(φ(x) > ψ(x)), where > is a weak conditional (from Asher & Morreau 1991). The key innovation is per-individual evaluation (§12.3): ψ is evaluated for each individual a only in those worlds where a is a normal φ.

"Birds fly" is true because for each bird a, the most normal a-bird worlds are ones where a flies. For Opus the penguin, the normal Opus-penguin worlds are NOT normal Opus-bird worlds, so "Penguins don't fly" correctly overrides "Birds fly" for penguins (exx. 7–8).

Chapter Sections Covered

• §12.1–12.2: Framework and challenges (exx. 1–5)
• §12.3: Per-individual normality (exx. 6–9)
• §12.4: Arguments against probabilistic alternatives

Connection to Existing Infrastructure

1. NormalityOrder (Core/Order/Normality.lean): preorder structure on worlds. A&P's per-individual normality is a normality ordering per entity and restrictor class.

2. traditionalGEN (Lexical/Noun/Kind/Generics.lean): GEN's normal parameter is the Bool-level projection of a normality ordering.

3. TweetyNixon (Phenomena/DefaultReasoning/TweetyNixon.lean): the Tweety Triangle data — the classic test case for A&P's system.

Refinement vs Specificity

processDefault below uses NormalityOrder.refine (@cite{veltman-1996}'s operation), which intersects ordering constraints. For the Tweety Triangle, Veltman's refinement produces incomparability between penguinFlies and penguinNoFly (neither is ≤ the other, since each satisfies one default and violates the other). A&P's per-individual evaluation resolves this via specificity: the more specific "penguins don't fly" overrides "birds fly" for penguins. The tweetyLe ordering encodes this specificity-resolved result directly.

structure AsherPelletier2013.DefaultRule (W : Type u_1) : Type u_1

A default rule: "Normally, if restrictor then scope."

Generic sentences express default rules. "Birds fly" means "Normally, if x is a bird, then x flies."

• restrictor : W → Prop
• scope : W → Prop

def AsherPelletier2013.processDefault {W : Type u_1} (no : Core.Order.NormalityOrder W) (d : DefaultRule W) : Core.Order.NormalityOrder W

Process a default rule as a refinement of a normality ordering.

"Normally, if P then Q" refines the ordering to promote P∧Q worlds over P∧¬Q worlds via NormalityOrder.refine. This is @cite{veltman-1996}'s monotonic (intersection-based) operation.

Note: A&P's actual system uses per-individual evaluation with specificity, which goes beyond simple refinement. See the module docstring caveat about refinement vs specificity.

Equations

• AsherPelletier2013.processDefault no d = no.refine fun (w : W) => d.restrictor w → d.scope w

structure AsherPelletier2013.PerIndividualDatum : Type

Per-individual evaluation data from §12.3.

The chapter's key innovation: for ∀x(φ(x) > ψ(x)), the consequent ψ is evaluated per-individual. For individual a in the domain, we look at normal a-φ worlds — worlds where a is a normal φ.

• sentence : String
• individual : String
• restrictorClass : String
• normalWorldDesc : String
• scopeHolds : Bool
• exNumber : String

def AsherPelletier2013.instReprPerIndividualDatum.repr : PerIndividualDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AsherPelletier2013.instReprPerIndividualDatum : Repr PerIndividualDatum

Equations

• AsherPelletier2013.instReprPerIndividualDatum = { reprPrec := AsherPelletier2013.instReprPerIndividualDatum.repr }

def AsherPelletier2013.opusPenguinsDontFly : PerIndividualDatum

Ex. (7): "Penguins don't fly" — evaluated for Opus. Normal Opus-PENGUIN worlds: Opus doesn't fly. Scope (¬fly) holds.

Equations

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

def AsherPelletier2013.opusBirdsFly : PerIndividualDatum

Ex. (8): "Birds fly" — evaluated for Opus. Normal Opus-BIRD worlds: in those worlds, Opus is "definitely not a normal penguin." So Opus flies. Scope (fly) holds.

Key insight: both "Birds fly" and "Penguins don't fly" are true SIMULTANEOUSLY for the same individual — evaluated at different normal worlds (normal-bird vs normal-penguin worlds).

Equations

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

theorem AsherPelletier2013.both_generics_true : opusPenguinsDontFly.scopeHolds = true ∧ opusBirdsFly.scopeHolds = true

Both generics are simultaneously true for penguins. Per-individual evaluation evaluates at DIFFERENT normal worlds for each restrictor, so both can hold without contradiction.

theorem AsherPelletier2013.specificity_selects_penguin_default : opusPenguinsDontFly.scopeHolds = true ∧ Phenomena.DefaultReasoning.tweety_doesnt_fly = true

Specificity determines which default to apply for inference: the more specific "penguins don't fly" overrides "birds fly" for penguins. This is a property of defeasible inference with the > conditional, not of the per-individual evaluation itself.

structure AsherPelletier2013.NormalityConstrual : Type

§12.3, ex. (9): "Turtles live to be 100."

The notion of a "normal φ(a) world" has some "give" to it — different construals of normality yield different truth values. Under an Aristotelian/teleological conception (natural telos of a turtle: if everything goes right), it's true. Under a statistical conception (most turtles die within hours of hatching), it's false.

A&P consider this context-dependence a virtue: discourse and contextual factors fix the normality construal.

• sentence : String
• construal : String
• genericTrue : Bool
• exNumber : String

def AsherPelletier2013.instReprNormalityConstrual.repr : NormalityConstrual → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AsherPelletier2013.instReprNormalityConstrual : Repr NormalityConstrual

Equations

• AsherPelletier2013.instReprNormalityConstrual = { reprPrec := AsherPelletier2013.instReprNormalityConstrual.repr }

def AsherPelletier2013.turtlesTeleological : NormalityConstrual

Equations

• AsherPelletier2013.turtlesTeleological = { sentence := "Turtles live to be 100", construal := "Aristotelian/teleological: natural telos of a turtle", genericTrue := true, exNumber := "(9)" }

def AsherPelletier2013.turtlesStatistical : NormalityConstrual

Equations

• AsherPelletier2013.turtlesStatistical = { sentence := "Turtles live to be 100", construal := "Statistical: most turtles die within hours of hatching", genericTrue := false, exNumber := "(9)" }

theorem AsherPelletier2013.normality_context_dependent : turtlesTeleological.genericTrue ≠ turtlesStatistical.genericTrue

The same generic has different truth values under different normality construals — A&P's "slop" in the normality notion.

def AsherPelletier2013.birdsNormallyFly : DefaultRule Phenomena.DefaultReasoning.TweetyWorld

Default 1: "Birds normally fly."

Equations

• AsherPelletier2013.birdsNormallyFly = { restrictor := Phenomena.DefaultReasoning.isBird, scope := Phenomena.DefaultReasoning.flies }

def AsherPelletier2013.penguinsNormallyDontFly : DefaultRule Phenomena.DefaultReasoning.TweetyWorld

Default 2: "Penguins normally don't fly."

Equations

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

def AsherPelletier2013.tweetyOrdering : Core.Order.NormalityOrder Phenomena.DefaultReasoning.TweetyWorld

Veltman-style refinement of both defaults.

This uses NormalityOrder.refine to process both defaults. The result makes penguinNoFly and penguinFlies incomparable — neither is ≤ the other — because the two defaults create crossing constraints. (penguinFlies satisfies "birds fly" but violates "penguins don't fly"; penguinNoFly does the reverse.)

This matches the Nixon Diamond behavior (conflicting defaults → agnosticism), not the Tweety Triangle (specificity resolution). A&P's per-individual evaluation resolves this via specificity, encoded in tweetyLe below.

The order of processing doesn't matter (NormalityOrder.refine_comm).

Equations

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

theorem AsherPelletier2013.penguin_nofly_more_normal : AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly Phenomena.DefaultReasoning.TweetyWorld.penguinFlies = true ∧ AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.penguinFlies Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly = false

Specificity resolution: penguinNoFly is strictly more normal than penguinFlies (the more specific penguin default wins).

theorem AsherPelletier2013.bird_fly_more_normal : AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.birdFlies Phenomena.DefaultReasoning.TweetyWorld.birdNoFly = true ∧ AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.birdNoFly Phenomena.DefaultReasoning.TweetyWorld.birdFlies = false

The bird default applies for non-penguin birds: birdFlies is strictly more normal than birdNoFly.

theorem AsherPelletier2013.tweety_resolved : Phenomena.DefaultReasoning.robin_flies = true ∧ Phenomena.DefaultReasoning.tweety_doesnt_fly = true

The empirical judgments match: Robin flies, Tweety doesn't.

def AsherPelletier2013.normalFromOrdering {W : Type u_1} (le_dec : W → W → Bool) (domain : List W) : W → Bool

The normal parameter in traditionalGEN is the Bool-level projection of a normality ordering: normal(s) = true iff s is among the most normal elements.

This bridges the abstract ordering theory to the concrete GEN operator. Requires decidable le to compute Bool values.

Equations

• AsherPelletier2013.normalFromOrdering le_dec domain w = domain.all fun (v : W) => le_dec w v

theorem AsherPelletier2013.total_all_normal {W : Type u_1} (domain : List W) (w : W) : w ∈ domain → normalFromOrdering (fun (x x_1 : W) => true) domain w = true

When the ordering is total (initial state), every world is normal.

theorem AsherPelletier2013.tweety_normal_worlds : have domain := [Phenomena.DefaultReasoning.TweetyWorld.birdFlies, Phenomena.DefaultReasoning.TweetyWorld.birdNoFly, Phenomena.DefaultReasoning.TweetyWorld.penguinFlies, Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly]; normalFromOrdering AsherPelletier2013.tweetyLe✝ domain Phenomena.DefaultReasoning.TweetyWorld.birdFlies = true ∧ normalFromOrdering AsherPelletier2013.tweetyLe✝ domain Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly = true ∧ normalFromOrdering AsherPelletier2013.tweetyLe✝ domain Phenomena.DefaultReasoning.TweetyWorld.penguinFlies = false ∧ normalFromOrdering AsherPelletier2013.tweetyLe✝ domain Phenomena.DefaultReasoning.TweetyWorld.birdNoFly = false

Under the specificity-resolved ordering, the normal TweetyWorlds (those in the top tier) are exactly birdFlies and penguinNoFly.

structure AsherPelletier2013.ChallengeDatum : Type

Challenge examples from §12.2 that the simple modal analysis ∀x(φ > ψ) appears to predict wrongly.

• sentence : String
• challenge : String
• exNumber : String

def AsherPelletier2013.instReprChallengeDatum.repr : ChallengeDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AsherPelletier2013.instReprChallengeDatum : Repr ChallengeDatum

Equations

• AsherPelletier2013.instReprChallengeDatum = { reprPrec := AsherPelletier2013.instReprChallengeDatum.repr }

def AsherPelletier2013.ducksLayEggs : ChallengeDatum

Ex. (4a): "Ducks lay eggs" — the basic analysis predicts normal male ducks lay eggs, which is wrong.

Equations

• AsherPelletier2013.ducksLayEggs = { sentence := "Ducks lay eggs", challenge := "Predicts normal male ducks lay eggs", exNumber := "(4a)" }

def AsherPelletier2013.cardinalsRed : ChallengeDatum

Ex. (4b): "Cardinals are bright red" — predicts normal female cardinals are bright red, which is wrong.

Equations

• AsherPelletier2013.cardinalsRed = { sentence := "Cardinals are bright red", challenge := "Predicts normal female cardinals are bright red", exNumber := "(4b)" }

def AsherPelletier2013.mosquitoesWNV : ChallengeDatum

Ex. (5): "Mosquitoes carry the West Nile Virus" — true despite a vanishingly small percentage of normal mosquitoes carrying WNV.

Equations

• AsherPelletier2013.mosquitoesWNV = { sentence := "Mosquitoes carry the West Nile Virus", challenge := "True despite vanishingly small percentage carrying WNV", exNumber := "(5)" }

def AsherPelletier2013.challengeData : List ChallengeDatum

Equations

• AsherPelletier2013.challengeData = [AsherPelletier2013.ducksLayEggs, AsherPelletier2013.cardinalsRed, AsherPelletier2013.mosquitoesWNV]

inductive AsherPelletier2013.AntiProbArgument : Type

A&P's arguments against @cite{cohen-1999a}'s probabilistic semantics for generics.

Cohen proposes generic truth ↔ Pr(B(a)|A(a)) > 0.5 (the "Cohen conditional"). A&P argue this is inadequate for three reasons.

• tooWeak : AntiProbArgument

  Too weak: Pr(tails|coin-flip) ≈ 50.05% → "*This coin normally comes up tails" should NOT be a true generic.

• wrongInference : AntiProbArgument

  Wrong inference pattern: probabilistic semantics validates Modus Ponens (Pr(B|A) > 0.5 and A(a) → B(a) more likely than not) but NOT Defeasible Modus Ponens. Generics support the latter ("Birds fly, Tweety is a bird, so Tweety flies") but the inference is defeasible.

• embeddedGenerics : AntiProbArgument

  Embedded generics ("Dogs chase cats that chase mice") require higher-order probabilities, leading to triviality results.

@[implicit_reducible]

instance AsherPelletier2013.instDecidableEqAntiProbArgument : DecidableEq AntiProbArgument

Equations

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

def AsherPelletier2013.instReprAntiProbArgument.repr : AntiProbArgument → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AsherPelletier2013.instReprAntiProbArgument : Repr AntiProbArgument

Equations

• AsherPelletier2013.instReprAntiProbArgument = { reprPrec := AsherPelletier2013.instReprAntiProbArgument.repr }

theorem AsherPelletier2013.generic_nonmonotonic : AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly Phenomena.DefaultReasoning.TweetyWorld.birdFlies = true ∧ AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.birdFlies Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly = true ∧ AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.penguinFlies Phenomena.DefaultReasoning.TweetyWorld.penguinNoFly = false ∧ AsherPelletier2013.tweetyLe✝ Phenomena.DefaultReasoning.TweetyWorld.penguinFlies Phenomena.DefaultReasoning.TweetyWorld.birdFlies = false

Generic reasoning is non-monotonic: the specificity-resolved ordering makes penguinNoFly top-tier (equally normal as birdFlies), despite penguinNoFly violating the "birds fly" default. The more specific penguin default overrides.

Adding the information "Tweety is a penguin" retracts the conclusion "Tweety flies" and replaces it with "Tweety doesn't fly."