|
| 1 | +import Linglib.Theories.Semantics.Dynamic.Core.KindAnaphora |
| 2 | + |
| 3 | +/-! |
| 4 | +# Anaphora for Concepts, Kinds, and Parts |
| 5 | +@cite{krifka-2026} |
| 6 | +
|
| 7 | +Empirical data and verification theorems for @cite{krifka-2026}'s theory |
| 8 | +of concept discourse referents. Three types of anaphora are distinguished: |
| 9 | +
|
| 10 | +| Type | Pronoun | Picks up | Example | |
| 11 | +|------|---------|----------|---------| |
| 12 | +| Entity | *he/she/it* | individual dref | *A dog₃ came in. It₃ barked.* | |
| 13 | +| Concept | *one*, empty NP | concept dref | *John has a big dog₂. Mary has a small one₂.* | |
| 14 | +| Kind | *it*[MASS], *they*[COUNT] | concept dref → kind | *John owns a dog₂. They₂ are loyal.* | |
| 15 | +
|
| 16 | +## Key empirical claims |
| 17 | +
|
| 18 | +1. **Concept drefs project past anaphoric islands** — negation, modals, |
| 19 | + conditionals cannot trap concept drefs (unlike entity drefs) |
| 20 | +2. **Mass/count feature determines kind pronoun** — *it* for [MASS], |
| 21 | + *they* for [COUNT], independent of ontology |
| 22 | +3. **Kind anaphora ≠ concept anaphora** — kind anaphors derive kind |
| 23 | + individuals via ∩ (and ⊔ for count), concept anaphors reuse the property |
| 24 | +
|
| 25 | +## End-to-End Example |
| 26 | +
|
| 27 | +Section 3 constructs a concrete model of examples (44)–(45): |
| 28 | +
|
| 29 | +``` |
| 30 | +John₁ doesn't own [DP a₃ [NP dog]₂]. |
| 31 | + → concept dref x₂ ('dog'[COUNT]) persists in output |
| 32 | + → entity dref x₃ (the dog) is trapped under ¬∃ |
| 33 | +He₁ is afraid of them₂,₄. |
| 34 | + → kind anaphor picks up concept x₂ (accessible!) |
| 35 | + → derives kind individual via ∩(⊔⟦dog⟧) |
| 36 | +``` |
| 37 | +-/ |
| 38 | + |
| 39 | +namespace Phenomena.Reference.Studies.Krifka2026 |
| 40 | + |
| 41 | +open Semantics.Dynamic.Core (ConceptDRef DRefVal) |
| 42 | +open Semantics.Dynamic.Core.KindAnaphora |
| 43 | + |
| 44 | +-- ════════════════════════════════════════════════════ |
| 45 | +-- § 1. Kind Pronoun Selection |
| 46 | +-- ════════════════════════════════════════════════════ |
| 47 | + |
| 48 | +/-- Kind-anaphoric pronouns, selected by the [MASS]/[COUNT] feature. -/ |
| 49 | +inductive KindPronoun where |
| 50 | + | it -- singular, selects [MASS] concepts |
| 51 | + | they -- plural, selects [COUNT] concepts |
| 52 | + deriving DecidableEq, Repr |
| 53 | + |
| 54 | +/-- Select kind-anaphoric pronoun from the count feature. |
| 55 | +
|
| 56 | + @cite{krifka-2026} (17a,b): |
| 57 | + - ⟦it⟧ = λP[MASS] λi.∩P(i) |
| 58 | + - ⟦they⟧ = λP[COUNT] λi.∩⊔P(i) -/ |
| 59 | +def selectPronoun : MassCount → KindPronoun |
| 60 | + | .mass => .it |
| 61 | + | .count => .they |
| 62 | + |
| 63 | +/-- Example (7a): count noun antecedent → plural kind anaphor *them*. |
| 64 | + *John noticed a spider in the bathroom. He has a phobia against them / \*it.* -/ |
| 65 | +theorem ex7a_count_them : selectPronoun .count = .they := rfl |
| 66 | + |
| 67 | +/-- Example (7b): mass noun antecedent → singular kind anaphor *it*. |
| 68 | + *John noticed mold in the bathroom. He is allergic against it / \*them.* -/ |
| 69 | +theorem ex7b_mass_it : selectPronoun .mass = .it := rfl |
| 70 | + |
| 71 | +/-- Examples (8a,b): the same individuals (*pollen*[MASS] vs *pollen grains*[COUNT]) |
| 72 | + select different pronouns based purely on the morphosyntactic feature. |
| 73 | + (8a) *There is a lot of pollen in the air. I am allergic against it / \*them.* |
| 74 | + (8b) *There are a lot of pollen grains in the air. I am allergic against them / ??it.* -/ |
| 75 | +theorem ex8_feature_determines_pronoun : |
| 76 | + selectPronoun .mass ≠ selectPronoun .count := by decide |
| 77 | + |
| 78 | + |
| 79 | +-- ════════════════════════════════════════════════════ |
| 80 | +-- § 2. Concept DRef Projection: Island Escaping |
| 81 | +-- ════════════════════════════════════════════════════ |
| 82 | + |
| 83 | +section IslandEscaping |
| 84 | + |
| 85 | +variable {W E : Type*} |
| 86 | + |
| 87 | +/-- Examples (5a,c), (25), (44–45): Concept drefs project past negation. |
| 88 | +
|
| 89 | + (5a) *John doesn't own a dog. He is afraid of them. But Mary owns one.* |
| 90 | + (5c) *John doesn't own a dog. \*It is friendly.* |
| 91 | +
|
| 92 | + In the DRT representation (25) and dynamic semantics (44–45), the concept |
| 93 | + dref x₂ for 'dog' is in the main box / presupposed in the input. After |
| 94 | + negation, x₂ persists (licensing *them₂*, *one₂*), but the entity dref |
| 95 | + x₃ is trapped under ¬∃ (blocking *\*it₃*). -/ |
| 96 | +theorem dog_concept_survives_negation |
| 97 | + {dogConcept : ConceptDRef W E} |
| 98 | + {φ : DSent W E} |
| 99 | + {g h : HAssign W E} |
| 100 | + (hDog : g 2 = .concept dogConcept) |
| 101 | + (hNovel : g 3 = .undef) |
| 102 | + (hNeg : dNeg φ g h) : |
| 103 | + h 2 = .concept dogConcept ∧ h 3 = .undef := |
| 104 | + concept_entity_asymmetry hDog hNovel hNeg |
| 105 | + |
| 106 | +end IslandEscaping |
| 107 | + |
| 108 | + |
| 109 | +-- ════════════════════════════════════════════════════ |
| 110 | +-- § 3. End-to-End: "John doesn't own a dog" (44–45) |
| 111 | +-- ════════════════════════════════════════════════════ |
| 112 | + |
| 113 | +section EndToEnd |
| 114 | + |
| 115 | +/-- Concrete entity type for the worked example. -/ |
| 116 | +inductive Ent where | john | mary |
| 117 | + deriving DecidableEq, Repr |
| 118 | + |
| 119 | +/-- Concrete world type. A world where John doesn't own a dog. -/ |
| 120 | +inductive Wld where | w₀ |
| 121 | + deriving DecidableEq, Repr |
| 122 | + |
| 123 | +/-- The concept 'dog' as a concept dref with [COUNT] feature. |
| 124 | + In this model, no entity satisfies the dog predicate (John doesn't own one). -/ |
| 125 | +def dogConcept : ConceptDRef Wld Ent where |
| 126 | + property := λ _ _ => false -- no dogs in this model |
| 127 | + feature := .count |
| 128 | + |
| 129 | +/-- Initial assignment for (44e): g₁=F(John), g₂=F(dog), F(C)(g₂). |
| 130 | + Following @cite{krifka-2026} (40g)/(44e): John's name presupposes |
| 131 | + dref 1 is anchored to John; the head noun *dog*₂ presupposes dref 2 |
| 132 | + is anchored to the 'dog' concept with [COUNT] feature. -/ |
| 133 | +def g₀ : HAssign Wld Ent := λ n => |
| 134 | + match n with |
| 135 | + | 1 => .entity .john |
| 136 | + | 2 => .concept dogConcept |
| 137 | + | _ => .undef |
| 138 | + |
| 139 | +/-- Sentence meaning for "own [DP a₃ [NP dog]₂]": introduces entity dref |
| 140 | + at index 3, constrained to satisfy the concept property at index 2. -/ |
| 141 | +def ownADog : DSent Wld Ent := entityIntro 3 (λ g h => |
| 142 | + g = h ∧ (g 2).liftConceptPred (λ c => c.property .w₀ (match g 3 with |
| 143 | + | .entity e => e | _ => .john)) = true) |
| 144 | + |
| 145 | +/-- "John₁ doesn't own [DP a₃ [NP dog]₂]" as the negation of ownADog. -/ |
| 146 | +def doesntOwnADog : DSent Wld Ent := dNeg ownADog |
| 147 | + |
| 148 | +/-- The negation is satisfiable in this model (no dogs exist). |
| 149 | + Output: g₀ = h (test), confirming no entity dref was introduced. -/ |
| 150 | +theorem negation_satisfiable : |
| 151 | + doesntOwnADog g₀ g₀ := by |
| 152 | + refine ⟨rfl, ?_⟩ |
| 153 | + intro ⟨k, e, hBody⟩ |
| 154 | + simp only [g₀, dogConcept, DRefVal.liftConceptPred] at hBody |
| 155 | + obtain ⟨hEq, hProp⟩ := hBody |
| 156 | + -- After update, g(2) = g₀(2) = .concept dogConcept, g(3) = .entity e |
| 157 | + -- The concept property returns false for all entities |
| 158 | + simp at hProp |
| 159 | + |
| 160 | +/-- **Main result**: after "John doesn't own a dog", the concept dref |
| 161 | + for 'dog' at index 2 is accessible while the entity dref at index 3 |
| 162 | + remains undefined. This is the concrete instantiation of the asymmetry |
| 163 | + predicted by @cite{krifka-2026} §4. -/ |
| 164 | +theorem concrete_concept_entity_asymmetry : |
| 165 | + ∀ h : HAssign Wld Ent, |
| 166 | + doesntOwnADog g₀ h → |
| 167 | + h 2 = .concept dogConcept ∧ h 3 = .undef := |
| 168 | + λ _ hNeg => concept_entity_asymmetry rfl rfl hNeg |
| 169 | + |
| 170 | +/-- The kind anaphor *them* selects [COUNT] for dogs, as expected. -/ |
| 171 | +theorem dog_kind_pronoun : selectPronoun dogConcept.feature = .they := rfl |
| 172 | + |
| 173 | +end EndToEnd |
| 174 | + |
| 175 | + |
| 176 | +-- ════════════════════════════════════════════════════ |
| 177 | +-- § 4. Concept vs Kind Anaphora (19a,b) |
| 178 | +-- ════════════════════════════════════════════════════ |
| 179 | + |
| 180 | +/-- Anaphoric constructions that pick up concept drefs. |
| 181 | +
|
| 182 | + @cite{krifka-2026} §3 distinguishes concept anaphors (which reuse the |
| 183 | + property directly) from kind anaphors (which derive kind individuals |
| 184 | + via ∩). Both pick up concept drefs, but they do different things. |
| 185 | +
|
| 186 | + The distinction is testable via examples like (19a,b): |
| 187 | + (19a) *John didn't get a dog from the animal shelter downtown. |
| 188 | + He is afraid of them.* — kind anaphora (OK: dogs-as-kind) |
| 189 | + (19b) *John didn't get a dog from the animal shelter downtown. |
| 190 | + But Mary got one.* — concept anaphora (OK: a dog-from-the-shelter) -/ |
| 191 | +inductive AnaphoricConstruction where |
| 192 | + | emptyNP -- *one*, empty NP: picks up concept property directly |
| 193 | + | emptyPP -- partitive *of them*: picks up concept for part-whole |
| 194 | + | kindPron -- *it*[MASS], *they*[COUNT]: derives kind via ∩(⊔)P |
| 195 | + deriving DecidableEq, Repr |
| 196 | + |
| 197 | +/-- Whether a construction derives a kind individual or reuses the property. -/ |
| 198 | +def derivesKind : AnaphoricConstruction → Bool |
| 199 | + | .kindPron => true |
| 200 | + | .emptyNP => false |
| 201 | + | .emptyPP => false |
| 202 | + |
| 203 | +/-- Kind pronouns derive kinds; concept anaphors (*one*, empty NP/PP) don't. |
| 204 | + This distinction explains (19a) vs (19b): "dogs from the animal shelter" |
| 205 | + doesn't name a kind (cf. @cite{carlson-1977}), so kind anaphora yields the |
| 206 | + general dog-kind, while concept anaphora preserves the full NP property. -/ |
| 207 | +theorem kind_vs_concept_distinction : |
| 208 | + derivesKind .kindPron = true ∧ |
| 209 | + derivesKind .emptyNP = false ∧ |
| 210 | + derivesKind .emptyPP = false := |
| 211 | + ⟨rfl, rfl, rfl⟩ |
| 212 | + |
| 213 | +end Phenomena.Reference.Studies.Krifka2026 |
0 commit comments