@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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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

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

structure Phenomena.Generics.Studies.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

instance Phenomena.Generics.Studies.AsherPelletier2013.instReprPerIndividualDatum : Repr PerIndividualDatum

Equations

• Phenomena.Generics.Studies.AsherPelletier2013.instReprPerIndividualDatum = { reprPrec := Phenomena.Generics.Studies.AsherPelletier2013.instReprPerIndividualDatum.repr }

def Phenomena.Generics.Studies.AsherPelletier2013.instReprPerIndividualDatum.repr : PerIndividualDatum → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.AsherPelletier2013.specificity_selects_penguin_default : opusPenguinsDontFly.scopeHolds = true ∧ 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 Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.AsherPelletier2013.instReprNormalityConstrual.repr : NormalityConstrual → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.AsherPelletier2013.instReprNormalityConstrual : Repr NormalityConstrual

Equations

• Phenomena.Generics.Studies.AsherPelletier2013.instReprNormalityConstrual = { reprPrec := Phenomena.Generics.Studies.AsherPelletier2013.instReprNormalityConstrual.repr }

def Phenomena.Generics.Studies.AsherPelletier2013.turtlesTeleological : NormalityConstrual

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.turtlesStatistical : NormalityConstrual

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.AsherPelletier2013.birdsNormallyFly : DefaultRule DefaultReasoning.TweetyWorld

Default 1: "Birds normally fly."

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.penguinsNormallyDontFly : DefaultRule DefaultReasoning.TweetyWorld

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

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.tweetyOrdering : Core.Order.NormalityOrder 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 Phenomena.Generics.Studies.AsherPelletier2013.penguin_nofly_more_normal : Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝ DefaultReasoning.TweetyWorld.penguinNoFly DefaultReasoning.TweetyWorld.penguinFlies = true ∧ Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝¹ DefaultReasoning.TweetyWorld.penguinFlies DefaultReasoning.TweetyWorld.penguinNoFly = false

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

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

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

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

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

def Phenomena.Generics.Studies.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

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.AsherPelletier2013.tweety_normal_worlds : have domain := [DefaultReasoning.TweetyWorld.birdFlies, DefaultReasoning.TweetyWorld.birdNoFly, DefaultReasoning.TweetyWorld.penguinFlies, DefaultReasoning.TweetyWorld.penguinNoFly]; normalFromOrdering Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝ domain DefaultReasoning.TweetyWorld.birdFlies = true ∧ normalFromOrdering Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝¹ domain DefaultReasoning.TweetyWorld.penguinNoFly = true ∧ normalFromOrdering Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝² domain DefaultReasoning.TweetyWorld.penguinFlies = false ∧ normalFromOrdering Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝³ domain DefaultReasoning.TweetyWorld.birdNoFly = false

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

structure Phenomena.Generics.Studies.AsherPelletier2013.ChallengeDatum : Type

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

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

instance Phenomena.Generics.Studies.AsherPelletier2013.instReprChallengeDatum : Repr ChallengeDatum

Equations

• Phenomena.Generics.Studies.AsherPelletier2013.instReprChallengeDatum = { reprPrec := Phenomena.Generics.Studies.AsherPelletier2013.instReprChallengeDatum.repr }

def Phenomena.Generics.Studies.AsherPelletier2013.instReprChallengeDatum.repr : ChallengeDatum → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.ducksLayEggs : ChallengeDatum

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

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.cardinalsRed : ChallengeDatum

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

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.mosquitoesWNV : ChallengeDatum

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

Equations

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

def Phenomena.Generics.Studies.AsherPelletier2013.challengeData : List ChallengeDatum

Equations

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

inductive Phenomena.Generics.Studies.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.

instance Phenomena.Generics.Studies.AsherPelletier2013.instDecidableEqAntiProbArgument : DecidableEq AntiProbArgument

Equations

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

instance Phenomena.Generics.Studies.AsherPelletier2013.instReprAntiProbArgument : Repr AntiProbArgument

Equations

• Phenomena.Generics.Studies.AsherPelletier2013.instReprAntiProbArgument = { reprPrec := Phenomena.Generics.Studies.AsherPelletier2013.instReprAntiProbArgument.repr }

def Phenomena.Generics.Studies.AsherPelletier2013.instReprAntiProbArgument.repr : AntiProbArgument → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.AsherPelletier2013.instBEqAntiProbArgument : BEq AntiProbArgument

Equations

• Phenomena.Generics.Studies.AsherPelletier2013.instBEqAntiProbArgument = { beq := Phenomena.Generics.Studies.AsherPelletier2013.instBEqAntiProbArgument.beq }

def Phenomena.Generics.Studies.AsherPelletier2013.instBEqAntiProbArgument.beq : AntiProbArgument → AntiProbArgument → Bool

Equations

• Phenomena.Generics.Studies.AsherPelletier2013.instBEqAntiProbArgument.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

theorem Phenomena.Generics.Studies.AsherPelletier2013.generic_nonmonotonic : Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝ DefaultReasoning.TweetyWorld.penguinNoFly DefaultReasoning.TweetyWorld.birdFlies = true ∧ Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝¹ DefaultReasoning.TweetyWorld.birdFlies DefaultReasoning.TweetyWorld.penguinNoFly = true ∧ Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝² DefaultReasoning.TweetyWorld.penguinFlies DefaultReasoning.TweetyWorld.penguinNoFly = false ∧ Phenomena.Generics.Studies.AsherPelletier2013.tweetyLe✝³ DefaultReasoning.TweetyWorld.penguinFlies 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."