Anaphora for Concepts, Kinds, and Parts #
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/Kinds/NominalMappingParameter: ⟦it⟧ = λP[MASS] λi.∩P(i),
⟦they⟧ = λP[COUNT] λi.∩⊔P(i) (17a,b). The dynamic layer instantiates the
substrate Update/test/dneg algebra of Semantics/Dynamic/Connectives
at heterogeneous assignments over DRefVal.
Negation here is the paper's VP negation ⟦doesn't⟧ (44b), test (∼φ); 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 absorptionHAssign,entityIntro: heterogeneous assignments and indefinite updateconcept_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)
Kind pronoun and kind-operator selection #
Kind-anaphoric pronouns, selected by the [MASS]/[COUNT] feature.
- it : KindPronoun
- they : KindPronoun
Instances For
Equations
- Krifka2026.instDecidableEqKindPronoun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Krifka2026.instReprKindPronoun = { reprPrec := Krifka2026.instReprKindPronoun.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Select kind-anaphoric pronoun from the count feature.
[Kri26] (17a,b):
- ⟦it⟧ = λP[MASS] λi.∩P(i)
- ⟦they⟧ = λP[COUNT] λi.∩⊔P(i)
Equations
Instances For
The semantic side of (17a,b): it applies ∩ directly, they applies plural closure ⊔ before ∩.
Equations
Instances For
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.
Example (7a): count noun antecedent → plural kind anaphor them. John noticed a spider in the bathroom. He has a phobia against them / *it.
Example (7b): mass noun antecedent → singular kind anaphor it. John noticed mold in the bathroom. He is allergic against it / *them.
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 #
Heterogeneous assignment: drefs valued in entities, concepts, or indices
([Kri26] §4). Partiality is modeled by DRefVal.undef, so this is
Core.Assignment (DRefVal W E) rather than Core.PartialAssign.
Equations
Instances For
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 (Semantics.Dynamic.Core.DRefVal.entity e)) h
Instances For
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.
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).
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.
The concept/entity asymmetry under negation test (∼φ) ((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.
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) #
Concrete entity type for the worked example.
Instances For
Equations
- Krifka2026.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
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✝
Instances For
Equations
- Krifka2026.instReprEnt = { reprPrec := Krifka2026.instReprEnt.repr }
Equations
- Krifka2026.instDecidableEqWld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Krifka2026.instReprWld = { reprPrec := Krifka2026.instReprWld.repr }
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✝
Instances For
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 }
Instances For
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
Instances For
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.
Instances For
"John₁ doesn't own [DP a₃ [NP dog]₂]": the paper's VP negation ⟦doesn't⟧ (44b) is the substrate test of dynamic negation.
Equations
Instances For
The negation is satisfiable in this model (no dogs exist). Output: g₀ = h (test), confirming no entity dref was introduced.
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.
The kind anaphor them selects [COUNT] for dogs, as expected.
Concept vs kind anaphora (19a,b) #
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
Instances For
Equations
- Krifka2026.instDecidableEqAnaphoricConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whether a construction derives a kind individual or reuses the property.
Equations
Instances For
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.