Kind Anaphora: Static-Dynamic Bridge

@cite{krifka-2026}

Bridges the static kind semantics in @cite{chierchia-1998} (∩, ⊔, IsMass, kindAnaphorMass, kindAnaphorCount) with the dynamic concept discourse referent types in DiscourseRef (ConceptDRef, DRefVal).

Both modules share MassCount from Core.Lexical.Word, which models the morphosyntactic mass/count feature that determines kind-anaphor pronoun selection (it for [MASS], they for [COUNT]).

Core insight

@cite{krifka-2026} proposes that head nouns introduce concept discourse referents — properties annotated with a [MASS]/[COUNT] feature. Kind anaphors pick up these concept drefs and derive kind individuals via Chierchia's ∩ operator:

• it picks up [MASS] concepts: ⟦it⟧ = λP[MASS]. ∩P
• they picks up [COUNT] concepts: ⟦they⟧ = λP[COUNT]. ∩(⊔P)

Concept drefs project past anaphoric islands (negation, modals, conditionals) because they are presupposed in the input assignment, not existentially introduced. This is what licenses:

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

while blocking:

John doesn't own a dog. *It is friendly.

Sections

1. Kind anaphor selection by mass/count feature
2. Concept dref projection past anaphoric islands

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

Select the kind-anaphor operator based on the morphosyntactic mass/count feature.

@cite{krifka-2026} (17a,b):

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

The [MASS]/[COUNT] feature determines the pronoun form and whether plural closure (⊔) applies before nominalization (∩).

Equations

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

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

For mass properties, both anaphor paths yield the same kind.

@cite{krifka-2026} (16): ⊔⊔S = ⊔S for cumulative S (absorption rule). Since mass nouns are cumulative, plural closure is a no-op, so kindAnaphorCount P = kindAnaphorMass P when P is mass.

This means the [MASS]/[COUNT] feature's only role is selecting pronoun morphology — the semantic content of the kind anaphor is identical for mass properties.

@[reducible, inline]

abbrev Semantics.Kinds.Anaphora.HAssign (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Heterogeneous assignment: maps indices to discourse referent values.

Following @cite{krifka-2026} §4: assignments are partial functions from ℕ to a heterogeneous universe including entities, concepts (properties with mass/count features), and world-time indices. Partiality is modeled by DRefVal.undef, so this is Core.Assignment (DRefVal W E) rather than Core.PartialAssign (DRefVal W E).

Equations

• Semantics.Kinds.Anaphora.HAssign W E = Core.Assignment (Semantics.Dynamic.Core.DRefVal W E)

def Semantics.Kinds.Anaphora.DSent (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Dynamic sentence meaning: relation between input and output assignments.

@cite{krifka-2026} §4: meanings of type aast map input assignment g to output assignment h relative to a world-time index i. We omit the index parameter for the projection theorems since it is orthogonal to the island-escaping behavior.

Equations

• Semantics.Kinds.Anaphora.DSent W E = (Semantics.Kinds.Anaphora.HAssign W E → Semantics.Kinds.Anaphora.HAssign W E → Prop)

def Semantics.Kinds.Anaphora.dNeg {W : Type u_1} {E : Type u_2} (φ : DSent W E) : DSent W E

DPL-style negation: test (output = input) plus denial of body.

@cite{krifka-2026} (34): ⟦NEG⟧ = λp.λghi[g=h, ¬∃k[g≤k, p(gki)]]

Negation is a test: it preserves the input assignment (g = h) and checks that no extension of g satisfies the body. This is why entity drefs introduced under negation are inaccessible — they exist only in the existentially bound extension k.

Equations

• Semantics.Kinds.Anaphora.dNeg φ g h = (g = h ∧ ¬∃ (k : Semantics.Kinds.Anaphora.HAssign W E), φ g k)

def Semantics.Kinds.Anaphora.entityIntro {W : Type u_1} {E : Type u_2} (n : ℕ) (body : DSent W E) : DSent W E

Existential introduction of an entity dref at index n.

Models the indexed determiner a₃ in @cite{krifka-2026} (40c,e): the determiner introduces a new entity dref (index 3) that falls under the concept property (index 2).

Equations

• Semantics.Kinds.Anaphora.entityIntro n body g h = ∃ (e : E), body (fun (m : ℕ) => if m = n then Semantics.Dynamic.Core.DRefVal.entity e else g m) h

def Semantics.Kinds.Anaphora.conceptPresup {W : Type u_1} {E : Type u_2} (n : ℕ) (c : Dynamic.Core.ConceptDRef W E) (body : DSent W E) : DSent W E

Concept presupposition: the input assignment must already contain a concept dref at index n.

Models how head nouns introduce concept drefs presuppositionally in @cite{krifka-2026} §4 — they behave like names. The indexed head noun dog₂ in (40d) is interpreted as a dynamic predicate of type eaast that presupposes dref 2 is anchored to the property 'dog'. Unlike entity drefs (existentially introduced by the determiner), concept drefs are conditions on the INPUT assignment, making them globally accessible.

Equations

• Semantics.Kinds.Anaphora.conceptPresup n c body g h = (g n = Semantics.Dynamic.Core.DRefVal.concept c ∧ body g h)

theorem Semantics.Kinds.Anaphora.dNeg_preserves {W : Type u_1} {E : Type u_2} (φ : DSent W E) {g h : HAssign W E} (hNeg : dNeg φ g h) (n : ℕ) : h n = g n

After negation, every index in the output has the same value as in the input. This is the fundamental property of negation-as-test.

theorem Semantics.Kinds.Anaphora.concept_survives_negation {W : Type u_1} {E : Type u_2} {n : ℕ} {c : Dynamic.Core.ConceptDRef W E} {body : DSent W E} {g h : HAssign W E} (hPresup : g n = Dynamic.Core.DRefVal.concept c) (hNeg : dNeg body g h) : h n = Dynamic.Core.DRefVal.concept c

Concept drefs survive negation.

If a concept dref was presupposed in the input, it remains accessible in the output of a negated sentence.

@cite{krifka-2026} §3, §4: John doesn't own a dog. introduces concept dref x₂ for 'dog' in the main box / input assignment. After negation, x₂ persists, licensing continuations like He is afraid of them₂.

Proof: negation forces h = g (test), so h(n) = g(n) = .concept c.

theorem Semantics.Kinds.Anaphora.entity_trapped_by_negation {W : Type u_1} {E : Type u_2} {n : ℕ} {body : DSent W E} {g h : HAssign W E} (hNeg : dNeg (entityIntro n body) g h) (hNovel : g n = Dynamic.Core.DRefVal.undef) : h n = Dynamic.Core.DRefVal.undef

Entity drefs die under negation.

Entity drefs introduced by indefinites under negation are inaccessible in the output: the existentially introduced entity exists only in the local extension k, which is bound under ¬∃.

@cite{krifka-2026} §4: after John doesn't own [a₃ dog₂], index 3 (the entity dref for the dog John might own) is NOT in the output assignment, because it was introduced by ∃k (the determiner) under ¬ (the negation operator).

Formally: negation forces h = g, and since the entity was NEWLY introduced at n (novelty: g(n) = .undef), the output h(n) = .undef.

theorem Semantics.Kinds.Anaphora.concept_entity_asymmetry {W : Type u_1} {E : Type u_2} {nConcept nEntity : ℕ} {c : Dynamic.Core.ConceptDRef W E} {φ : DSent W E} {g h : HAssign W E} (hPresup : g nConcept = Dynamic.Core.DRefVal.concept c) (hNovel : g nEntity = Dynamic.Core.DRefVal.undef) (hNeg : dNeg φ g h) : h nConcept = Dynamic.Core.DRefVal.concept c ∧ h nEntity = Dynamic.Core.DRefVal.undef

The asymmetry between concept and entity drefs under negation.

In the same sentence John₁ doesn't own [a₃ dog₂], the concept dref at index 2 survives while the entity dref at index 3 does not.

This theorem combines the two projection results.

def Semantics.Kinds.Anaphora.embedAssign {W : Type u_1} {E : Type u_2} (g : Core.Assignment E) : HAssign W E

Embed a homogeneous DPL-style assignment (Assignment E = Nat → E, @cite{groenendijk-stokhof-1991}) into a heterogeneous Krifka-style assignment (Nat → DRefVal W E) by wrapping every value in .entity.

Equations

• Semantics.Kinds.Anaphora.embedAssign g n = Semantics.Dynamic.Core.DRefVal.entity (g n)

def Semantics.Kinds.Anaphora.liftDPL {W : Type u_1} {E : Type u_2} (φ : Dynamic.Core.DynProp.DRS (Core.Assignment E)) : DSent W E

Lift a DPL-style relation (DRS (Assignment E)) to operate on heterogeneous assignments via the entity embedding.

Equations

• Semantics.Kinds.Anaphora.liftDPL φ g h = ∃ (g' : Core.Assignment E) (h' : Core.Assignment E), Semantics.Kinds.Anaphora.embedAssign g' = g ∧ Semantics.Kinds.Anaphora.embedAssign h' = h ∧ φ g' h'

theorem Semantics.Kinds.Anaphora.dNeg_structure {W : Type u_1} {E : Type u_2} (φ : DSent W E) (g h : HAssign W E) : dNeg φ g h ↔ g = h ∧ ¬∃ (k : HAssign W E), φ g k

dNeg and test (dneg φ) (the substrate form of @cite{groenendijk-stokhof-1991}'s DPL negation) have identical structure.

Both are: λ g h => g = h ∧ ¬∃ k, φ g k. @cite{krifka-2026}'s negation (34) generalizes DPL negation from homogeneous (Nat → E) to heterogeneous (Nat → DRefVal W E) assignments. The structure is preserved because the projection mechanism depends only on g = h.

theorem Semantics.Kinds.Anaphora.dplNeg_structure {E : Type u_2} (φ : Dynamic.Core.DynProp.DRS (Core.Assignment E)) (g h : Core.Assignment E) : [∼φ] g h ↔ g = h ∧ ¬∃ (k : Core.Assignment E), φ g k

theorem Semantics.Kinds.Anaphora.liftDPL_neg {W : Type u_1} {E : Type u_2} (φ : Dynamic.Core.DynProp.DRS (Core.Assignment E)) (g h : HAssign W E) : liftDPL [∼φ] g h → dNeg (liftDPL φ) g h

Negation commutes with the DPL→heterogeneous embedding.

Lifting a DPL-style negation produces the same result as negating the lifted relation, modulo the entity-only constraint on assignments.