Anaphora for Concepts, Kinds, and Parts

[Kri26]

Head nouns introduce presupposed concept discourse referents — properties tagged [MASS]/[COUNT] — which project past anaphoric islands (in Krifka's extended sense: negation, modals, conditionals), while entity drefs introduced by indefinites under negation are trapped. Kind anaphors pick up concept drefs and derive kind individuals via [Chi98]'s ∩ from Semantics/Genericity/NominalMappingParameter: ⟦it⟧ = λP[MASS] λi.∩P(i), ⟦they⟧ = λP[COUNT] λi.∩⊔P(i) (17a,b). The dynamic layer instantiates the substrate Update/test/neg algebra of Semantics/Dynamic/Connectives at heterogeneous assignments over DRefVal.

Negation here is the paper's VP negation ⟦doesn't⟧ (44b), test (neg φ); the sentential ⟦NEG⟧ (34) additionally restricts the negated existential to extensions g≤k, and both carry a world-time index — differences orthogonal to projection, which needs only that negation is a test. The paper derives the concept dref's input-presupposition compositionally from the head noun's partial (strong-Kleene) lexical entry (40d); that pipeline is not formalized, so the projection theorems take the input conditions as hypotheses. Cf. [Hof25] (Studies/Hofmann2025.lean) for the neighboring account of entity-dref accessibility under negation via nonveridical continuations.

Main declarations

• selectPronoun, selectKindAnaphor, selectKindAnaphor_count_eq_mass: [MASS]/[COUNT]-driven pronoun and kind-operator selection, with absorption
• HAssign, entityIntro: heterogeneous assignments and indefinite update
• concept_survives_test, entity_trapped_by_test, concept_entity_asymmetry: projection past island operators
• an end-to-end model of John₁ doesn't own [DP a₃ [NP dog]₂] (44–45)

Concept drefs and heterogeneous dref values ([Kri26] §4)

Paper-specific substrate: concept discourse referents (property + count feature), the heterogeneous DRefVal universe, and concept-variable indices.

structure Krifka2026.ConceptDRef (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A concept discourse referent value: a property annotated with a morphosyntactic count feature.

Introduced by the NP of an antecedent DP. For example, dog in John owns a dog introduces a concept dref anchored to the property λi.λx[dog(i)(x)] with feature [COUNT].

Kind anaphors pick up concept drefs and derive kind individuals via Chierchia's ∩ (down) operator:

• ⟦it⟧ = λP[MASS]. λi. ∩P(i)
• ⟦they⟧ = λP[COUNT]. λi. ∩(⊔P)(i)

The ⊔-closure for count nouns introduces pluralization, allowing for the number mismatch between a spider (singular) and they (plural). For mass nouns, ⊔-closure is vacuous (mass predicates are already cumulative), so the singular it is used.

• property : W → E → Bool

  The property this concept is anchored to: λi.λx[P(i)(x)]

• feature : MassCount

  Morphosyntactic count feature

inductive Krifka2026.DRefVal (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Values that discourse referent indices can map to.

Standard dynamic semantics restricts assignments to map indices to entities. [Kri26] §4 extends this: assignments are partial functions from ℕ to a heterogeneous universe including entities, concepts (properties with count features), and world-time indices.

• .entity e: an individual referent (standard entity dref)
• .concept c: a concept dref — the NP property with [MASS]/[COUNT]
• .index w: a world-time index dref
• .undef: index not in the domain (models assignment partiality)

Key property: concept drefs project past operators like negation, disjunction, and modals — they are introduced in the global assignment, not in local sub-assignments. This is what licenses kind anaphora out of anaphoric islands:

John doesn't own a dog. He is afraid of them.

The entity dref for a dog is trapped under negation, but the concept dref for 'dog' projects to the global context.

• entity {W : Type u_1} {E : Type u_2} : E → DRefVal W E
• concept {W : Type u_1} {E : Type u_2} : ConceptDRef W E → DRefVal W E
• index {W : Type u_1} {E : Type u_2} : W → DRefVal W E
• undef {W : Type u_1} {E : Type u_2} : DRefVal W E

def Krifka2026.DRefVal.getEntity {W : Type u_1} {E : Type u_2} : DRefVal W E → Option E

Extract entity value, if present.

Equations

• (Krifka2026.DRefVal.entity e).getEntity = some e
• x✝.getEntity = none

def Krifka2026.DRefVal.getConcept {W : Type u_1} {E : Type u_2} : DRefVal W E → Option (ConceptDRef W E)

Extract concept dref, if present.

Equations

• (Krifka2026.DRefVal.concept c).getConcept = some c
• x✝.getConcept = none

def Krifka2026.DRefVal.getIndex {W : Type u_1} {E : Type u_2} : DRefVal W E → Option W

Extract world-time index, if present.

Equations

• (Krifka2026.DRefVal.index w).getIndex = some w
• x✝.getIndex = none

def Krifka2026.DRefVal.isDefined {W : Type u_1} {E : Type u_2} : DRefVal W E → Prop

Is this index in the domain of the assignment?

Equations

• Krifka2026.DRefVal.undef.isDefined = False
• x✝.isDefined = True

def Krifka2026.DRefVal.liftEntityPred {W : Type u_1} {E : Type u_2} (p : E → Bool) : DRefVal W E → Bool

Lift a predicate on entities to DRefVal (false for non-entities).

Equations

• Krifka2026.DRefVal.liftEntityPred p (Krifka2026.DRefVal.entity e) = p e
• Krifka2026.DRefVal.liftEntityPred p x✝ = false

def Krifka2026.DRefVal.liftConceptPred {W : Type u_1} {E : Type u_2} (p : ConceptDRef W E → Bool) : DRefVal W E → Bool

Lift a predicate on concepts to DRefVal (false for non-concepts).

Equations

• Krifka2026.DRefVal.liftConceptPred p (Krifka2026.DRefVal.concept c) = p c
• Krifka2026.DRefVal.liftConceptPred p x✝ = false

structure Krifka2026.CVar : Type

A concept variable (names a concept dref).

Concept variables are indices into the assignment that map to ConceptDRef values — properties annotated with [MASS]/[COUNT].

• idx : ℕ

@[instance_reducible]

instance Krifka2026.instDecidableEqCVar : DecidableEq CVar

Equations

• Krifka2026.instDecidableEqCVar = Krifka2026.instDecidableEqCVar.decEq

def Krifka2026.instDecidableEqCVar.decEq (x✝ x✝¹ : CVar) : Decidable (x✝ = x✝¹)

Equations

• Krifka2026.instDecidableEqCVar.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Krifka2026.instReprCVar.repr : CVar → ℕ → Std.Format

Equations

• Krifka2026.instReprCVar.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "idx" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.idx)).group) " }"

@[instance_reducible]

instance Krifka2026.instReprCVar : Repr CVar

Equations

• Krifka2026.instReprCVar = { reprPrec := Krifka2026.instReprCVar.repr }

def Krifka2026.instHashableCVar.hash : CVar → UInt64

Equations

• Krifka2026.instHashableCVar.hash { idx := a } = mixHash 0 (hash a)

@[instance_reducible]

instance Krifka2026.instHashableCVar : Hashable CVar

Equations

• Krifka2026.instHashableCVar = { hash := Krifka2026.instHashableCVar.hash }

Kind pronoun and kind-operator selection

inductive Krifka2026.KindPronoun : Type

Kind-anaphoric pronouns, selected by the [MASS]/[COUNT] feature.

• it : KindPronoun
• they : KindPronoun

@[instance_reducible]

instance Krifka2026.instDecidableEqKindPronoun : DecidableEq KindPronoun

Equations

• Krifka2026.instDecidableEqKindPronoun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Krifka2026.instReprKindPronoun : Repr KindPronoun

Equations

• Krifka2026.instReprKindPronoun = { reprPrec := Krifka2026.instReprKindPronoun.repr }

def Krifka2026.instReprKindPronoun.repr : KindPronoun → ℕ → Std.Format

Equations

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

def Krifka2026.selectPronoun : MassCount → KindPronoun

Select kind-anaphoric pronoun from the count feature.

[Kri26] (17a,b):

• ⟦it⟧ = λP[MASS] λi.∩P(i)
• ⟦they⟧ = λP[COUNT] λi.∩⊔P(i)

Equations

• Krifka2026.selectPronoun MassCount.mass = Krifka2026.KindPronoun.it
• Krifka2026.selectPronoun MassCount.count = Krifka2026.KindPronoun.they

def Krifka2026.selectKindAnaphor {World Atom : Type} (feature : MassCount) (P : Semantics.Kinds.NMP.Property World Atom) : Semantics.Kinds.NMP.Kind World Atom

The semantic side of (17a,b): it applies ∩ directly, they applies plural closure ⊔ before ∩.

Equations

• Krifka2026.selectKindAnaphor MassCount.mass P = Semantics.Kinds.NMP.kindAnaphorMass World Atom P
• Krifka2026.selectKindAnaphor MassCount.count P = Semantics.Kinds.NMP.kindAnaphorCount World Atom P

theorem Krifka2026.selectKindAnaphor_count_eq_mass {World Atom : Type} (P : Semantics.Kinds.NMP.Property World Atom) (hMass : Semantics.Kinds.NMP.IsMass World Atom P) : selectKindAnaphor MassCount.count P = selectKindAnaphor MassCount.mass P

For mass properties both anaphor paths yield the same kind, by [Kri26]'s absorption rule ⊔⊔S = ⊔S: plural closure is a no-op on cumulative properties, so for mass concepts the [MASS]/[COUNT] feature's only role is selecting pronoun morphology.

theorem Krifka2026.ex7a_count_them : selectPronoun MassCount.count = KindPronoun.they

Example (7a): count noun antecedent → plural kind anaphor them. John noticed a spider in the bathroom. He has a phobia against them / *it.

theorem Krifka2026.ex7b_mass_it : selectPronoun MassCount.mass = KindPronoun.it

Example (7b): mass noun antecedent → singular kind anaphor it. John noticed mold in the bathroom. He is allergic against it / *them.

theorem Krifka2026.ex8_feature_determines_pronoun : selectPronoun MassCount.mass ≠ selectPronoun MassCount.count

Examples (8a,b): the same individuals (pollen[MASS] vs pollen grains[COUNT]) select different pronouns based purely on the morphosyntactic feature. (8a) There is a lot of pollen in the air. I am allergic against it / *them. (8b) There are a lot of pollen grains in the air. I am allergic against them / ??it.

Concept dref projection past anaphoric islands

@[reducible, inline]

abbrev Krifka2026.HAssign (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Heterogeneous assignment: drefs valued in entities, concepts, or indices ([Kri26] §4). Partiality is modeled by DRefVal.undef, so this is Assignment (DRefVal W E) rather than PartialAssign.

Equations

• Krifka2026.HAssign W E = Assignment (Krifka2026.DRefVal W E)

def Krifka2026.entityIntro {W : Type u_1} {E : Type u_2} (n : ℕ) (body : DynamicSemantics.Update (HAssign W E)) : DynamicSemantics.Update (HAssign W E)

Existential introduction of an entity dref at index n, as by the indexed determiner a₃ in (40c) — minus the falls-under-the-concept condition, which is delegated to body, and with novelty (g n = .undef) as an external hypothesis rather than built into the extension relation g<₃k.

Equations

• Krifka2026.entityIntro n body g h = ∃ (e : E), body (Function.update g n (Krifka2026.DRefVal.entity e)) h

theorem Krifka2026.test_apply_eq {W : Type u_1} {E : Type u_2} {C : DynamicSemantics.Condition (HAssign W E)} {g h : HAssign W E} (hTest : DynamicSemantics.Update.test C g h) (n : ℕ) : h n = g n

Island operators are tests, and tests preserve every dref of the input assignment. Negation, implication, and disjunction all return a Condition re-entering the update algebra via test, so this single fact covers [Kri26]'s whole island list at once.

theorem Krifka2026.concept_survives_test {W : Type u_1} {E : Type u_2} {n : ℕ} {c : ConceptDRef W E} {C : DynamicSemantics.Condition (HAssign W E)} {g h : HAssign W E} (hPresup : g n = DRefVal.concept c) (hTest : DynamicSemantics.Update.test C g h) : h n = DRefVal.concept c

Concept drefs survive islands ((5a), (25), (44–45)): a concept dref presupposed in the input is still anchored in the output of any test. The presupposition is a hypothesis here; the paper derives it from the head noun's partial lexical entry (40d).

theorem Krifka2026.entity_trapped_by_test {W : Type u_1} {E : Type u_2} {n : ℕ} {C : DynamicSemantics.Condition (HAssign W E)} {g h : HAssign W E} (hNovel : g n = DRefVal.undef) (hTest : DynamicSemantics.Update.test C g h) : h n = DRefVal.undef

Entity drefs are trapped by islands ((5c)): a dref novel in the input (introduced only inside the island's ¬∃k) is still undefined in the output.

theorem Krifka2026.concept_entity_asymmetry {W : Type u_1} {E : Type u_2} {nC nE : ℕ} {c : ConceptDRef W E} {φ : DynamicSemantics.Update (HAssign W E)} {g h : HAssign W E} (hPresup : g nC = DRefVal.concept c) (hNovel : g nE = DRefVal.undef) (hNeg : DynamicSemantics.Update.test φ.neg g h) : h nC = DRefVal.concept c ∧ h nE = DRefVal.undef

The concept/entity asymmetry under negation test (neg φ) ((44e)): the concept dref persists, the entity dref does not. Both conjuncts are instances of test_apply_eq — the asymmetry is carried entirely by where the hypotheses place the two conditions (input presupposition vs input novelty), which is [Kri26]'s point.

theorem Krifka2026.dog_concept_survives_negation {W : Type u_1} {E : Type u_2} {dogConcept : ConceptDRef W E} {φ : DynamicSemantics.Update (HAssign W E)} {g h : HAssign W E} (hDog : g 2 = DRefVal.concept dogConcept) (hNovel : g 3 = DRefVal.undef) (hNeg : DynamicSemantics.Update.test φ.neg g h) : h 2 = DRefVal.concept dogConcept ∧ h 3 = DRefVal.undef

Examples (5a,c), (25), (44–45): concept drefs project past negation.

(5a) John doesn't own a dog. He is afraid of them. But Mary owns one. (5c) John doesn't own a dog. *It is friendly.

In the DRT representation (25) and dynamic semantics (44–45), the concept dref x₂ for 'dog' is in the main box / presupposed in the input. After negation, x₂ persists (licensing them₂, one₂), but the entity dref x₃ is trapped under ¬∃ (blocking *it₃).

End-to-end: John doesn't own a dog (44–45)

inductive Krifka2026.Ent : Type

Concrete entity type for the worked example.

• john : Ent
• mary : Ent

@[instance_reducible]

instance Krifka2026.instDecidableEqEnt : DecidableEq Ent

Equations

• Krifka2026.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2026.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

• Krifka2026.instReprEnt.repr Krifka2026.Ent.john prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2026.Ent.john")).group prec✝
• Krifka2026.instReprEnt.repr Krifka2026.Ent.mary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2026.Ent.mary")).group prec✝

@[instance_reducible]

instance Krifka2026.instReprEnt : Repr Ent

Equations

• Krifka2026.instReprEnt = { reprPrec := Krifka2026.instReprEnt.repr }

inductive Krifka2026.Wld : Type

Concrete world type. A world where John doesn't own a dog.

• w₀ : Wld

@[instance_reducible]

instance Krifka2026.instDecidableEqWld : DecidableEq Wld

Equations

• Krifka2026.instDecidableEqWld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Krifka2026.instReprWld : Repr Wld

Equations

• Krifka2026.instReprWld = { reprPrec := Krifka2026.instReprWld.repr }

def Krifka2026.instReprWld.repr : Wld → ℕ → Std.Format

Equations

• Krifka2026.instReprWld.repr Krifka2026.Wld.w₀ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2026.Wld.w₀")).group prec✝

def Krifka2026.dogConcept : ConceptDRef Wld Ent

The concept 'dog' as a concept dref with [COUNT] feature. In this model, no entity satisfies the dog predicate (John doesn't own one).

Equations

• Krifka2026.dogConcept = { property := fun (x : Krifka2026.Wld) (x_1 : Krifka2026.Ent) => false, feature := MassCount.count }

def Krifka2026.g₀ : HAssign Wld Ent

Initial assignment for (44e): g₁=F(John), g₂=F(dog), F(C)(g₂). Following [Kri26] (40g)/(44e): John's name presupposes dref 1 is anchored to John; the head noun dog₂ presupposes dref 2 is anchored to the 'dog' concept with [COUNT] feature.

Equations

• Krifka2026.g₀ 1 = Krifka2026.DRefVal.entity Krifka2026.Ent.john
• Krifka2026.g₀ 2 = Krifka2026.DRefVal.concept Krifka2026.dogConcept
• Krifka2026.g₀ n = Krifka2026.DRefVal.undef

def Krifka2026.ownADog : DynamicSemantics.Update (HAssign Wld Ent)

Sentence meaning for "own [DP a₃ [NP dog]₂]": introduces entity dref at index 3, constrained to satisfy the concept property at index 2.

Equations

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

def Krifka2026.doesntOwnADog : DynamicSemantics.Update (HAssign Wld Ent)

"John₁ doesn't own [DP a₃ [NP dog]₂]": the paper's VP negation ⟦doesn't⟧ (44b) is the substrate test of dynamic negation.

Equations

• Krifka2026.doesntOwnADog = DynamicSemantics.Update.test Krifka2026.ownADog.neg

theorem Krifka2026.negation_satisfiable : doesntOwnADog g₀ g₀

The negation is satisfiable in this model (no dogs exist). Output: g₀ = h (test), confirming no entity dref was introduced.

theorem Krifka2026.concrete_concept_entity_asymmetry (h : HAssign Wld Ent) : doesntOwnADog g₀ h → h 2 = DRefVal.concept dogConcept ∧ h 3 = DRefVal.undef

Main result: after "John doesn't own a dog", the concept dref for 'dog' at index 2 is accessible while the entity dref at index 3 remains undefined. This is the concrete instantiation of the asymmetry predicted by [Kri26] §4.

theorem Krifka2026.dog_kind_pronoun : selectPronoun dogConcept.feature = KindPronoun.they

The kind anaphor them selects [COUNT] for dogs, as expected.

Concept vs kind anaphora (19a,b)

inductive Krifka2026.AnaphoricConstruction : Type

Anaphoric constructions that pick up concept drefs.

[Kri26] §3 distinguishes concept anaphors (which reuse the property directly) from kind anaphors (which derive kind individuals via ∩). Both pick up concept drefs, but they do different things.

The distinction is testable via examples like (19a,b): (19a) John didn't get a dog from the animal shelter downtown. He is afraid of them. — kind anaphora (OK: dogs-as-kind) (19b) John didn't get a dog from the animal shelter downtown. But Mary got one. — concept anaphora (OK: a dog-from-the-shelter)

• emptyNP : AnaphoricConstruction
• emptyPP : AnaphoricConstruction
• kindPron : AnaphoricConstruction

@[instance_reducible]

instance Krifka2026.instDecidableEqAnaphoricConstruction : DecidableEq AnaphoricConstruction

Equations

• Krifka2026.instDecidableEqAnaphoricConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2026.instReprAnaphoricConstruction.repr : AnaphoricConstruction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Krifka2026.instReprAnaphoricConstruction : Repr AnaphoricConstruction

Equations

• Krifka2026.instReprAnaphoricConstruction = { reprPrec := Krifka2026.instReprAnaphoricConstruction.repr }

def Krifka2026.derivesKind : AnaphoricConstruction → Bool

Whether a construction derives a kind individual or reuses the property.

Equations

• Krifka2026.derivesKind Krifka2026.AnaphoricConstruction.kindPron = true
• Krifka2026.derivesKind Krifka2026.AnaphoricConstruction.emptyNP = false
• Krifka2026.derivesKind Krifka2026.AnaphoricConstruction.emptyPP = false

theorem Krifka2026.kind_vs_concept_distinction : derivesKind AnaphoricConstruction.kindPron = true ∧ derivesKind AnaphoricConstruction.emptyNP = false ∧ derivesKind AnaphoricConstruction.emptyPP = false

Kind pronouns derive kinds; concept anaphors (one, empty NP/PP) don't. This distinction explains (19a) vs (19b): "dogs from the animal shelter" doesn't name a kind (cf. [Car77]), so kind anaphora yields the general dog-kind, while concept anaphora preserves the full NP property.