@cite{krifka-2013}: Definitional Generics

Manfred Krifka, "Definitional Generics", ch. 15 of Genericity (eds. Mari, Beyssade, Del Prete), Oxford University Press, 2013.

Core Claim

IS-generics ("A madrigal is polyphonic") and BP-generics ("Madrigals are popular") correlate with two fundamentally different types of generic meaning:

• Descriptive generics: empirical generalizations about the world. Restrict possible worlds (DES update).
• Definitional generics: restrict admissible interpretations of linguistic expressions (DEF update).

The asymmetry is shown by minimal pairs (exx. 1–2):

• (1) "Madrigals are polyphonic" / "A madrigal is polyphonic" — both OK
• (2) "Madrigals are popular" / "#A madrigal is popular" — IS infelicitous

Being popular is not a defining property of the kind madrigal, so the IS form in (2b) fails as a definitional generic; meanwhile, the syntactic structure of IS blocks existential closure (the default mechanism), leaving only universal closure which requires a rule-like interpretation.

Chapter Sections Covered

• §15.1: IS/BP asymmetry, Lawler (1973a), Leslie et al. (2009)
• §15.2: Previous accounts — Burton-Roberts (1976, 1977), @cite{cohen-1999a}, Greenberg (2003, 2007). Rule types: physical, moral, legal, linguistic (exx. 5–9)
• §15.3.1: Two-index semantics, DES/DEF update operations, descriptive vs definitional readings of "Boys don't cry" (ex. 13), madrigal worked examples (exx. 20–21)
• §15.3.2: Topic-comment structure — definiendum (topic) vs definiens (comment) determines which expression's interpretation gets restricted
• §15.3.3: Definitions and facts — empirical discoveries become definitional via Kripke/Putnam causal theory of reference ("A donkey has 62 chromosomes", ex. 29)
• §15.3.4: IS applies to atomic individuals (suited for definitions checkable on single exemplars), BP to sum individuals (suited for empirical generalizations requiring many observations). But the IS→definitional tendency is not absolute (ex. 44).
• §15.4: Conclusion

Connection to Other Generics Studies

• @cite{cohen-1999a} (Studies/Cohen1999.lean): Cohen's rule-based account of IS generics — Krifka builds on Cohen's insight that IS generics express rules (physical, moral, legal, linguistic) but reanalyzes "rules" as interpretation restrictions rather than ontological entities
• @cite{asher-pelletier-2012} (Studies/AsherPelletier2013.lean): normality orderings — orthogonal to Krifka's theory, which targets the descriptive/definitional distinction rather than default reasoning

structure Krifka2013.Interp : Type

An interpretation index: determines how expressions are interpreted. Different interpretations assign different extensions to predicates. E.g., different height thresholds for "tall" (Barker 2002, exx. 10–11).

• id : ℕ

def Krifka2013.instDecidableEqInterp.decEq (x✝ x✝¹ : Interp) : Decidable (x✝ = x✝¹)

Equations

• Krifka2013.instDecidableEqInterp.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka2013.instDecidableEqInterp : DecidableEq Interp

Equations

• Krifka2013.instDecidableEqInterp = Krifka2013.instDecidableEqInterp.decEq

def Krifka2013.instReprInterp.repr : Interp → ℕ → Std.Format

Equations

• Krifka2013.instReprInterp.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

@[implicit_reducible]

instance Krifka2013.instReprInterp : Repr Interp

Equations

• Krifka2013.instReprInterp = { reprPrec := Krifka2013.instReprInterp.repr }

structure Krifka2013.World : Type

A world index: determines what factual state of affairs obtains.

• id : ℕ

def Krifka2013.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

• Krifka2013.instDecidableEqWorld.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka2013.instDecidableEqWorld : DecidableEq World

Equations

• Krifka2013.instDecidableEqWorld = Krifka2013.instDecidableEqWorld.decEq

@[implicit_reducible]

instance Krifka2013.instReprWorld : Repr World

Equations

• Krifka2013.instReprWorld = { reprPrec := Krifka2013.instReprWorld.repr }

def Krifka2013.instReprWorld.repr : World → ℕ → Std.Format

Equations

• Krifka2013.instReprWorld.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

@[reducible, inline]

abbrev Krifka2013.Denotation : Type

A denotation under two indices: ⟦α⟧^{i,w} in Krifka's notation.

Equations

• Krifka2013.Denotation = (Krifka2013.Interp → Krifka2013.World → Bool)

structure Krifka2013.CommonGround : Type

A common ground: a set of admissible interpretations paired with a set of possible worlds (§15.3.1, p. 377).

• interps : List Interp
• worlds : List World

@[implicit_reducible]

instance Krifka2013.instReprCommonGround : Repr CommonGround

Equations

• Krifka2013.instReprCommonGround = { reprPrec := Krifka2013.instReprCommonGround.repr }

def Krifka2013.instReprCommonGround.repr : CommonGround → ℕ → Std.Format

Equations

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

def Krifka2013.des (cg : CommonGround) (φ : Denotation) : CommonGround

DES (Descriptive update): restricts worlds, keeps interpretations.

⟨I, W⟩ + DES(⟦Φ⟧) = ⟨I, {w∈W | ∃i∈I. ⟦Φ⟧^{i,w}}⟩

Descriptive assertions inform about the world. The existential reflects that we may not yet know which interpretation to settle on; we keep worlds consistent with at least one admissible reading.

Equations

• Krifka2013.des cg φ = { interps := cg.interps, worlds := List.filter (fun (w : Krifka2013.World) => cg.interps.any fun (i : Krifka2013.Interp) => φ i w) cg.worlds }

def Krifka2013.def_ (cg : CommonGround) (φ : Denotation) : CommonGround

DEF (Definitional update): restricts interpretations, keeps worlds.

⟨I, W⟩ + DEF(⟦Φ⟧) = ⟨{i∈I | ∀w∈W. ⟦Φ⟧^{i,w}}, W⟩

Definitional assertions restrict the language: only interpretations under which the proposition holds in ALL worlds survive. The universal reflects that definitions must hold unconditionally.

Equations

• Krifka2013.def_ cg φ = { interps := List.filter (fun (i : Krifka2013.Interp) => cg.worlds.all fun (w : Krifka2013.World) => φ i w) cg.interps, worlds := cg.worlds }

theorem Krifka2013.des_preserves_interps (cg : CommonGround) (φ : Denotation) : (des cg φ).interps = cg.interps

DES preserves interpretations.

theorem Krifka2013.def_preserves_worlds (cg : CommonGround) (φ : Denotation) : (def_ cg φ).worlds = cg.worlds

DEF preserves worlds.

theorem Krifka2013.des_restricts_worlds (cg : CommonGround) (φ : Denotation) (w : World) : w ∈ (des cg φ).worlds → w ∈ cg.worlds

DES restricts worlds (result is a subset).

theorem Krifka2013.def_restricts_interps (cg : CommonGround) (φ : Denotation) (i : Interp) : i ∈ (def_ cg φ).interps → i ∈ cg.interps

DEF restricts interpretations (result is a subset).

theorem Krifka2013.def_invariant_world_measure {α : Type} (cg : CommonGround) (φ : Denotation) (f : List World → α) : f (def_ cg φ).worlds = f cg.worlds

Any function of worlds alone is invariant under DEF, because DEF only changes interpretations. Since threshold semantics measures world-prevalence, it cannot capture definitional generics that change truth value through DEF.

Since traditional GEN (a descriptive operator) reduces to threshold semantics (CovertQuantifier.reduces_to_threshold), this theorem shows definitional generics escape that reduction entirely.

def Krifka2013.i₁ : Interp

Three interpretations of "madrigal" varying in strictness.

• i₁: strict — only polyphonic pieces count as madrigals
• i₂: medium — mostly polyphonic, some exceptions allowed
• i₃: loose — includes monophonic pieces as madrigals

Equations

• Krifka2013.i₁ = { id := 1 }

def Krifka2013.i₂ : Interp

Equations

• Krifka2013.i₂ = { id := 2 }

def Krifka2013.i₃ : Interp

Equations

• Krifka2013.i₃ = { id := 3 }

def Krifka2013.w₁ : World

Three possible worlds.

• w₁, w₂: madrigals are generally popular
• w₃: madrigals are not popular

Equations

• Krifka2013.w₁ = { id := 1 }

def Krifka2013.w₂ : World

Equations

• Krifka2013.w₂ = { id := 2 }

def Krifka2013.w₃ : World

Equations

• Krifka2013.w₃ = { id := 3 }

def Krifka2013.cg₀ : CommonGround

Initial common ground: all interpretations, all worlds.

Equations

• Krifka2013.cg₀ = { interps := [Krifka2013.i₁, Krifka2013.i₂, Krifka2013.i₃], worlds := [Krifka2013.w₁, Krifka2013.w₂, Krifka2013.w₃] }

def Krifka2013.madrigalsPopular : Denotation

"Madrigals are popular" — a descriptive claim (ex. 20). True in w₁ and w₂ under all interpretations, false in w₃. Depends only on the world index: popularity is a fact about the world, not about how we interpret "madrigal."

Equations

• Krifka2013.madrigalsPopular _i w = match w.id with | 1 => true | 2 => true | x => false

def Krifka2013.madrigalsPolyphonic : Denotation

"Madrigals are polyphonic" — a definitional claim (ex. 21). True under i₁ and i₂ (in all worlds), false under i₃. Depends only on the interpretation index: whether madrigals are polyphonic is a matter of how "madrigal" is interpreted.

Equations

• Krifka2013.madrigalsPolyphonic i _w = match i.id with | 1 => true | 2 => true | x => false

theorem Krifka2013.des_popular_eliminates_w3 : (des cg₀ madrigalsPopular).worlds = [w₁, w₂]

After DES("Madrigals are popular"), w₃ is eliminated.

theorem Krifka2013.des_popular_keeps_interps : (des cg₀ madrigalsPopular).interps = [i₁, i₂, i₃]

DES preserves all three interpretations.

theorem Krifka2013.def_polyphonic_eliminates_i3 : (def_ cg₀ madrigalsPolyphonic).interps = [i₁, i₂]

After DEF("Madrigals are polyphonic"), i₃ is eliminated.

theorem Krifka2013.def_polyphonic_keeps_worlds : (def_ cg₀ madrigalsPolyphonic).worlds = [w₁, w₂, w₃]

DEF preserves all three worlds.

theorem Krifka2013.des_then_def : have cg := def_ (des cg₀ madrigalsPopular) madrigalsPolyphonic; cg.interps = [i₁, i₂] ∧ cg.worlds = [w₁, w₂]

DES then DEF: 2 interpretations, 2 worlds.

theorem Krifka2013.def_then_des : have cg := des (def_ cg₀ madrigalsPolyphonic) madrigalsPopular; cg.interps = [i₁, i₂] ∧ cg.worlds = [w₁, w₂]

DEF then DES: same result. This holds because madrigalsPopular depends only on w and madrigalsPolyphonic depends only on i, making their filter conditions independent. In general, DES and DEF do NOT commute (each references the other index in its quantifier scope).

theorem Krifka2013.def_not_world_reducible : (def_ cg₀ madrigalsPolyphonic).worlds = cg₀.worlds ∧ (def_ cg₀ madrigalsPolyphonic).interps ≠ cg₀.interps

Definitional generics cannot be reduced to prevalence thresholds because they operate on interpretations, not worlds.

inductive Krifka2013.RuleType : Type

Types of rules that definitional generics can express. Following @cite{cohen-1999a}'s categorization as cited by Krifka §15.2.

• physical : RuleType
• moral : RuleType
• legal : RuleType
• linguistic : RuleType

@[implicit_reducible]

instance Krifka2013.instDecidableEqRuleType : DecidableEq RuleType

Equations

• Krifka2013.instDecidableEqRuleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2013.instReprRuleType.repr : RuleType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2013.instReprRuleType.repr Krifka2013.RuleType.moral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2013.RuleType.moral")).group prec✝
• Krifka2013.instReprRuleType.repr Krifka2013.RuleType.legal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2013.RuleType.legal")).group prec✝

@[implicit_reducible]

instance Krifka2013.instReprRuleType : Repr RuleType

Equations

• Krifka2013.instReprRuleType = { reprPrec := Krifka2013.instReprRuleType.repr }

structure Krifka2013.GenericDatum : Type

Data entry for generics from Krifka's chapter. The felicitous field captures acceptability judgments — critical for encoding the IS/BP asymmetry.

• sentence : String
• subjectForm : Features.Genericity.GenericForm
• preferredReading : Features.Genericity.GenericReading
• felicitous : Bool
• ruleType : Option RuleType
• exNumber : String
• notes : String

def Krifka2013.instReprGenericDatum.repr : GenericDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka2013.instReprGenericDatum : Repr GenericDatum

Equations

• Krifka2013.instReprGenericDatum = { reprPrec := Krifka2013.instReprGenericDatum.repr }

def Krifka2013.madrigalPolyphonicBP : GenericDatum

Equations

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

def Krifka2013.madrigalPolyphonicIS : GenericDatum

Equations

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

def Krifka2013.madrigalPopularBP : GenericDatum

Equations

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

def Krifka2013.madrigalPopularIS : GenericDatum

Equations

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

def Krifka2013.kangarooMarsupialIS : GenericDatum

Equations

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

def Krifka2013.tigerClimbsTreesIS : GenericDatum

Bolinger considers (4a) "To be a tiger is to climb trees" analytic (but wrongly so), and (4b) true but not analytic. This shows IS-generics are not uniformly analytic or definitional.

Equations

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

def Krifka2013.electronChargeIS : GenericDatum

Equations

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

def Krifka2013.gentlemanDoorsIS : GenericDatum

Equations

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

def Krifka2013.bishopDiagonalIS : GenericDatum

Equations

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

def Krifka2013.pomegranateAppleCost : GenericDatum

Equations

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

structure Krifka2013.AmbiguousGeneric : Type

"Boys don't cry" (ex. 13) can be read either descriptively or definitionally — the same sentence under two interpretive modes:

Descriptive: the speaker assumes a shared interpretation of "boys" and communicates about the world — boys in fact don't cry.

Definitional: the speaker proposes restricting the admissible interpretations of "boys" to those where entities falling under "boys" don't cry in situations that could lead to crying. This restricts the language, not the world.

• sentence : String
• descriptiveReading : String
• definitionalReading : String
• exNumber : String

def Krifka2013.instReprAmbiguousGeneric.repr : AmbiguousGeneric → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka2013.instReprAmbiguousGeneric : Repr AmbiguousGeneric

Equations

• Krifka2013.instReprAmbiguousGeneric = { reprPrec := Krifka2013.instReprAmbiguousGeneric.repr }

def Krifka2013.boysDontCry : AmbiguousGeneric

Equations

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

def Krifka2013.donkeyChromosomesIS : GenericDatum

§15.3.3, ex. (29): "A donkey has 62 chromosomes."

The chromosome number was an empirical discovery, yet the sentence reads as definitional. Krifka explains this via Kripke (1972, 1980) and Putnam (1975): "donkey" picks out a natural kind via type specimens and the causal theory of reference. Properties that "run in the kind" at the species level (like chromosome number) become definitional properties of the word's meaning. Thus a descriptive discovery (Chiquita has 62 chromosomes, DES update) translates into a definitional property of "donkey" (DEF update, exx. 31–36).

Equations

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

def Krifka2013.animalCageChromosomes : GenericDatum

§15.3.3, ex. (37): "#An animal in this cage has 62 chromosomes."

Deviant because "animal in this cage" does not pick out a natural kind — it's an arbitrary extensional set. Definitional generics require the subject to denote a natural kind so that properties can be understood as "running in" the kind.

Equations

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

def Krifka2013.troutCaughtIS : GenericDatum

§15.3.4 argues that the IS→definitional tendency is NOT absolute. Examples like (44a) show IS-generics with clearly descriptive content: the methods for catching trout are not part of the definition of "trout."

§15.4 concludes: "descriptive generalizations are typically expressed by bare plurals because they tend to rely on observing many instances; definitional statements are typically expressed with indefinite singulars because the decision whether entities fall under a concept can typically be made by looking at single individuals." But these are tendencies, not strict grammatical constraints.

Equations

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

inductive Krifka2013.NumberDomain : Type

§15.3.4 observes a key structural difference:

• IS ("a madrigal"): applies to atomic individuals. One can check whether a single piece of music is polyphonic → suited for definitions
• BP ("madrigals"): applies to sum individuals. Checking popularity requires observing many instances → suited for generalizations

This atomic/sum distinction explains WHY IS-generics tend toward definitional readings and BP-generics toward descriptive ones, even though neither correlation is absolute.

• atomic : NumberDomain
• plural : NumberDomain

@[implicit_reducible]

instance Krifka2013.instDecidableEqNumberDomain : DecidableEq NumberDomain

Equations

• Krifka2013.instDecidableEqNumberDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2013.instReprNumberDomain.repr : NumberDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka2013.instReprNumberDomain : Repr NumberDomain

Equations

• Krifka2013.instReprNumberDomain = { reprPrec := Krifka2013.instReprNumberDomain.repr }

def Krifka2013.isAtomicDomain : Features.Genericity.GenericForm → NumberDomain

Equations

• Krifka2013.isAtomicDomain Features.Genericity.GenericForm.indefiniteSingular = Krifka2013.NumberDomain.atomic
• Krifka2013.isAtomicDomain Features.Genericity.GenericForm.barePlural = Krifka2013.NumberDomain.plural
• Krifka2013.isAtomicDomain Features.Genericity.GenericForm.definiteSingular = Krifka2013.NumberDomain.atomic
• Krifka2013.isAtomicDomain Features.Genericity.GenericForm.definitePlural = Krifka2013.NumberDomain.plural

def Krifka2013.exampleData : List GenericDatum

Equations

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

theorem Krifka2013.is_bp_asymmetry : madrigalPolyphonicBP.felicitous = true ∧ madrigalPolyphonicIS.felicitous = true ∧ madrigalPopularBP.felicitous = true ∧ madrigalPopularIS.felicitous = false

The central IS/BP asymmetry: both forms are fine for the definitional "polyphonic" predicate, but only BP is fine for the descriptive "popular" predicate.

theorem Krifka2013.bp_always_felicitous : ((List.filter (fun (d : GenericDatum) => d.subjectForm == Features.Genericity.GenericForm.barePlural) exampleData).all fun (d : GenericDatum) => d.felicitous) = true

All BP-generics in the data are felicitous — BPs are the unmarked form for both descriptive and definitional content.

theorem Krifka2013.infelicitous_is_lacks_rule_type : ((List.filter (fun (d : GenericDatum) => d.subjectForm == Features.Genericity.GenericForm.indefiniteSingular && !d.felicitous) exampleData).all fun (d : GenericDatum) => d.ruleType.isNone) = true

Infelicitous IS-generics have no rule type — the infelicity arises when IS is used for content that cannot serve as a definition.

theorem Krifka2013.rule_typed_is_felicitous : ((List.filter (fun (d : GenericDatum) => d.subjectForm == Features.Genericity.GenericForm.indefiniteSingular && d.ruleType.isSome) exampleData).all fun (d : GenericDatum) => d.felicitous) = true

IS-generics with a rule type are all felicitous.

theorem Krifka2013.natural_kind_required : donkeyChromosomesIS.felicitous = true ∧ animalCageChromosomes.felicitous = false

Natural-kind subjects with definitional readings are felicitous; non-natural-kind subjects (like "animal in this cage") fail even with definitional intent (ex. 37).

§15.3.2 observes that definitional generics have topic-comment structure where the definiendum (the term being defined) is the topic, and the definiens (the defining property) is the comment. "A madrigal is polyphonic" defines madrigal (topic), not polyphonic (comment).

The formal DEF rule (ex. 25) restricts interpretations of the topic expression α to those where the comment β holds for the topic's extension:

⟨I, W⟩ + DEF(⟦α⟧, ⟦β⟧) = ⟨{i∈I | ∀w∈W ∀X [⟦α⟧^{i,w}(X) → ∀i'∈I ⟦β⟧^{i',w}(X)]}, W⟩

This formalizes the intuition that "A madrigal is polyphonic" defines madrigal rather than polyphonic: the definiendum occupies the topic position and is the expression whose interpretation gets restricted.

The distinction matters for examples like the Greenhorn definition (ex. 28, from Karl May's Winnetou I, 1892): a series of predicational definitional sentences successively fix the meaning of a new word.

theorem Krifka2013.orthogonal_to_normality : (def_ cg₀ madrigalsPolyphonic).worlds = cg₀.worlds

Krifka's definitional generics are orthogonal to the default reasoning framework of @cite{asher-pelletier-2012}: normality orderings target descriptive generics (which worlds are normal), while Krifka's DEF targets the interpretation index. The two theories operate on different components of the common ground.

theorem Krifka2013.cohen_krifka_felicity_agreement : electronChargeIS.felicitous = true ∧ gentlemanDoorsIS.felicitous = true ∧ bishopDiagonalIS.felicitous = true ∧ madrigalPopularIS.felicitous = false

@cite{cohen-1999a}'s rule types (physical, moral, legal, linguistic) provide the content classification for what Krifka formalizes as interpretation restrictions. Cohen claims IS-generics EXPRESS rules; Krifka claims IS-generics are INTERPRETED as universal quantification (via UC) when the IS form blocks existential closure.

Both accounts predict the same felicity pattern: IS is natural for rule-like content. The difference is architectural — Cohen posits "rules" as ontological entities; Krifka derives the rule-like flavor from the interaction of IS syntax with closure mechanisms.