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

instance Phenomena.Generics.Studies.Krifka2013.instDecidableEqInterp : DecidableEq Interp

Equations

• Phenomena.Generics.Studies.Krifka2013.instDecidableEqInterp = Phenomena.Generics.Studies.Krifka2013.instDecidableEqInterp.decEq

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

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instReprInterp : Repr Interp

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprInterp = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprInterp.repr }

def Phenomena.Generics.Studies.Krifka2013.instReprInterp.repr : Interp → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.Krifka2013.instBEqInterp.beq : Interp → Interp → Bool

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqInterp.beq { id := a } { id := b } = (a == b)
• Phenomena.Generics.Studies.Krifka2013.instBEqInterp.beq x✝¹ x✝ = false

instance Phenomena.Generics.Studies.Krifka2013.instBEqInterp : BEq Interp

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqInterp = { beq := Phenomena.Generics.Studies.Krifka2013.instBEqInterp.beq }

structure Phenomena.Generics.Studies.Krifka2013.World : Type

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

• id : ℕ

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

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instDecidableEqWorld : DecidableEq World

Equations

• Phenomena.Generics.Studies.Krifka2013.instDecidableEqWorld = Phenomena.Generics.Studies.Krifka2013.instDecidableEqWorld.decEq

def Phenomena.Generics.Studies.Krifka2013.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instReprWorld : Repr World

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprWorld = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprWorld.repr }

instance Phenomena.Generics.Studies.Krifka2013.instBEqWorld : BEq World

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqWorld = { beq := Phenomena.Generics.Studies.Krifka2013.instBEqWorld.beq }

def Phenomena.Generics.Studies.Krifka2013.instBEqWorld.beq : World → World → Bool

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqWorld.beq { id := a } { id := b } = (a == b)
• Phenomena.Generics.Studies.Krifka2013.instBEqWorld.beq x✝¹ x✝ = false

@[reducible, inline]

abbrev Phenomena.Generics.Studies.Krifka2013.Denotation : Type

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

Equations

• Phenomena.Generics.Studies.Krifka2013.Denotation = (Phenomena.Generics.Studies.Krifka2013.Interp → Phenomena.Generics.Studies.Krifka2013.World → Bool)

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

def Phenomena.Generics.Studies.Krifka2013.instReprCommonGround.repr : CommonGround → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instReprCommonGround : Repr CommonGround

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprCommonGround = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprCommonGround.repr }

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

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

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

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

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

DES preserves interpretations.

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

DEF preserves worlds.

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

DES restricts worlds (result is a subset).

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

DEF restricts interpretations (result is a subset).

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

• Phenomena.Generics.Studies.Krifka2013.i₁ = { id := 1 }

def Phenomena.Generics.Studies.Krifka2013.i₂ : Interp

Equations

• Phenomena.Generics.Studies.Krifka2013.i₂ = { id := 2 }

def Phenomena.Generics.Studies.Krifka2013.i₃ : Interp

Equations

• Phenomena.Generics.Studies.Krifka2013.i₃ = { id := 3 }

def Phenomena.Generics.Studies.Krifka2013.w₁ : World

Three possible worlds.

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

Equations

• Phenomena.Generics.Studies.Krifka2013.w₁ = { id := 1 }

def Phenomena.Generics.Studies.Krifka2013.w₂ : World

Equations

• Phenomena.Generics.Studies.Krifka2013.w₂ = { id := 2 }

def Phenomena.Generics.Studies.Krifka2013.w₃ : World

Equations

• Phenomena.Generics.Studies.Krifka2013.w₃ = { id := 3 }

def Phenomena.Generics.Studies.Krifka2013.cg₀ : CommonGround

Initial common ground: all interpretations, all worlds.

Equations

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

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

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

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

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

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

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

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

DES preserves all three interpretations.

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

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

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

DEF preserves all three worlds.

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

instance Phenomena.Generics.Studies.Krifka2013.instDecidableEqRuleType : DecidableEq RuleType

Equations

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

def Phenomena.Generics.Studies.Krifka2013.instReprRuleType.repr : RuleType → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instReprRuleType : Repr RuleType

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprRuleType = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprRuleType.repr }

def Phenomena.Generics.Studies.Krifka2013.instBEqRuleType.beq : RuleType → RuleType → Bool

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqRuleType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Generics.Studies.Krifka2013.instBEqRuleType : BEq RuleType

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqRuleType = { beq := Phenomena.Generics.Studies.Krifka2013.instBEqRuleType.beq }

structure Phenomena.Generics.Studies.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 : Core.Genericity.GenericForm
• preferredReading : Core.Genericity.GenericReading
• felicitous : Bool
• ruleType : Option RuleType
• exNumber : String
• notes : String

def Phenomena.Generics.Studies.Krifka2013.instReprGenericDatum.repr : GenericDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instReprGenericDatum : Repr GenericDatum

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprGenericDatum = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprGenericDatum.repr }

def Phenomena.Generics.Studies.Krifka2013.madrigalPolyphonicBP : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.madrigalPolyphonicIS : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.madrigalPopularBP : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.madrigalPopularIS : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.kangarooMarsupialIS : GenericDatum

Equations

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

def Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Krifka2013.electronChargeIS : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.gentlemanDoorsIS : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.bishopDiagonalIS : GenericDatum

Equations

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

def Phenomena.Generics.Studies.Krifka2013.pomegranateAppleCost : GenericDatum

Equations

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

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

instance Phenomena.Generics.Studies.Krifka2013.instReprAmbiguousGeneric : Repr AmbiguousGeneric

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprAmbiguousGeneric = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprAmbiguousGeneric.repr }

def Phenomena.Generics.Studies.Krifka2013.instReprAmbiguousGeneric.repr : AmbiguousGeneric → ℕ → Std.Format

Equations

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

def Phenomena.Generics.Studies.Krifka2013.boysDontCry : AmbiguousGeneric

Equations

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

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

instance Phenomena.Generics.Studies.Krifka2013.instDecidableEqNumberDomain : DecidableEq NumberDomain

Equations

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

def Phenomena.Generics.Studies.Krifka2013.instReprNumberDomain.repr : NumberDomain → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.Studies.Krifka2013.instReprNumberDomain : Repr NumberDomain

Equations

• Phenomena.Generics.Studies.Krifka2013.instReprNumberDomain = { reprPrec := Phenomena.Generics.Studies.Krifka2013.instReprNumberDomain.repr }

instance Phenomena.Generics.Studies.Krifka2013.instBEqNumberDomain : BEq NumberDomain

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqNumberDomain = { beq := Phenomena.Generics.Studies.Krifka2013.instBEqNumberDomain.beq }

def Phenomena.Generics.Studies.Krifka2013.instBEqNumberDomain.beq : NumberDomain → NumberDomain → Bool

Equations

• Phenomena.Generics.Studies.Krifka2013.instBEqNumberDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Generics.Studies.Krifka2013.isAtomicDomain : Core.Genericity.GenericForm → NumberDomain

Equations

• Phenomena.Generics.Studies.Krifka2013.isAtomicDomain Core.Genericity.GenericForm.indefiniteSingular = Phenomena.Generics.Studies.Krifka2013.NumberDomain.atomic
• Phenomena.Generics.Studies.Krifka2013.isAtomicDomain Core.Genericity.GenericForm.barePlural = Phenomena.Generics.Studies.Krifka2013.NumberDomain.plural
• Phenomena.Generics.Studies.Krifka2013.isAtomicDomain Core.Genericity.GenericForm.definiteSingular = Phenomena.Generics.Studies.Krifka2013.NumberDomain.atomic
• Phenomena.Generics.Studies.Krifka2013.isAtomicDomain Core.Genericity.GenericForm.definitePlural = Phenomena.Generics.Studies.Krifka2013.NumberDomain.plural

def Phenomena.Generics.Studies.Krifka2013.exampleData : List GenericDatum

Equations

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

theorem Phenomena.Generics.Studies.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 Phenomena.Generics.Studies.Krifka2013.bp_always_felicitous : ((List.filter (fun (d : GenericDatum) => d.subjectForm == Core.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 Phenomena.Generics.Studies.Krifka2013.infelicitous_is_lacks_rule_type : ((List.filter (fun (d : GenericDatum) => d.subjectForm == Core.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 Phenomena.Generics.Studies.Krifka2013.rule_typed_is_felicitous : ((List.filter (fun (d : GenericDatum) => d.subjectForm == Core.Genericity.GenericForm.indefiniteSingular && d.ruleType.isSome) exampleData).all fun (d : GenericDatum) => d.felicitous) = true

IS-generics with a rule type are all felicitous.

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