Documentation

Linglib.Phenomena.Reference.Studies.Krifka2026

Anaphora for Concepts, Kinds, and Parts #

@cite{krifka-2026}

Empirical data and verification theorems for @cite{krifka-2026}'s theory of concept discourse referents. Three types of anaphora are distinguished:

TypePronounPicks upExample
Entityhe/she/itindividual drefA dog₃ came in. It₃ barked.
Conceptone, empty NPconcept drefJohn has a big dog₂. Mary has a small one₂.
Kindit[MASS], they[COUNT]concept dref → kindJohn owns a dog₂. They₂ are loyal.

Key empirical claims #

  1. Concept drefs project past anaphoric islands — negation, modals, conditionals cannot trap concept drefs (unlike entity drefs)
  2. Mass/count feature determines kind pronoun — it for [MASS], they for [COUNT], independent of ontology
  3. Kind anaphora ≠ concept anaphora — kind anaphors derive kind individuals via ∩ (and ⊔ for count), concept anaphors reuse the property

End-to-End Example #

Section 3 constructs a concrete model of examples (44)–(45):

John₁ doesn't own [DP a₃ [NP dog]₂].
  → concept dref x₂ ('dog'[COUNT]) persists in output
  → entity dref x₃ (the dog) is trapped under ¬∃
He₁ is afraid of them₂,₄.
  → kind anaphor picks up concept x₂ (accessible!)
  → derives kind individual via ∩(⊔⟦dog⟧)
source
inductive Phenomena.Reference.Studies.Krifka2026.KindPronoun :
Type

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

Instances For
    source
    instance Phenomena.Reference.Studies.Krifka2026.instDecidableEqKindPronoun :
    DecidableEq KindPronoun
    Equations
    source
    def Phenomena.Reference.Studies.Krifka2026.instReprKindPronoun.repr :
    KindPronoun → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Phenomena.Reference.Studies.Krifka2026.instReprKindPronoun :
      Repr KindPronoun
      Equations
      source
      def Phenomena.Reference.Studies.Krifka2026.selectPronoun :
      MassCount → KindPronoun

      Select kind-anaphoric pronoun from the count feature.

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

      • ⟦it⟧ = λP[MASS] λi.∩P(i)
      • ⟦they⟧ = λP[COUNT] λi.∩⊔P(i)
      Equations
      Instances For
        source
        theorem Phenomena.Reference.Studies.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.

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

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

        source
        theorem Phenomena.Reference.Studies.Krifka2026.dog_concept_survives_negation {W : Type u_1} {E : Type u_2} {dogConcept : Semantics.Dynamic.Core.ConceptDRef W E} {φ : Semantics.Dynamic.Core.KindAnaphora.DSent W E} {g h : Semantics.Dynamic.Core.KindAnaphora.HAssign W E} (hDog : g 2 = Semantics.Dynamic.Core.DRefVal.concept dogConcept) (hNovel : g 3 = Semantics.Dynamic.Core.DRefVal.undef) (hNeg : Semantics.Dynamic.Core.KindAnaphora.dNeg φ g h) :
        h 2 = Semantics.Dynamic.Core.DRefVal.concept dogConcept ∧ h 3 = Semantics.Dynamic.Core.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₃).

        source
        inductive Phenomena.Reference.Studies.Krifka2026.Ent :
        Type

        Concrete entity type for the worked example.

        Instances For
          source
          instance Phenomena.Reference.Studies.Krifka2026.instDecidableEqEnt :
          DecidableEq Ent
          Equations
          source
          instance Phenomena.Reference.Studies.Krifka2026.instReprEnt :
          Repr Ent
          Equations
          source
          def Phenomena.Reference.Studies.Krifka2026.instReprEnt.repr :
          Ent → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            inductive Phenomena.Reference.Studies.Krifka2026.Wld :
            Type

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

            Instances For
              source
              instance Phenomena.Reference.Studies.Krifka2026.instDecidableEqWld :
              DecidableEq Wld
              Equations
              source
              def Phenomena.Reference.Studies.Krifka2026.instReprWld.repr :
              Wld → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance Phenomena.Reference.Studies.Krifka2026.instReprWld :
                Repr Wld
                Equations
                source
                def Phenomena.Reference.Studies.Krifka2026.dogConcept :
                Semantics.Dynamic.Core.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
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Phenomena.Reference.Studies.Krifka2026.g₀ :
                  Semantics.Dynamic.Core.KindAnaphora.HAssign Wld Ent

                  Initial assignment for (44e): g₁=F(John), g₂=F(dog), F(C)(g₂). Following @cite{krifka-2026} (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
                    source
                    def Phenomena.Reference.Studies.Krifka2026.ownADog :
                    Semantics.Dynamic.Core.KindAnaphora.DSent 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.
                    Instances For
                      source
                      def Phenomena.Reference.Studies.Krifka2026.doesntOwnADog :
                      Semantics.Dynamic.Core.KindAnaphora.DSent Wld Ent

                      "John₁ doesn't own [DP a₃ [NP dog]₂]" as the negation of ownADog.

                      Equations
                      Instances For
                        source
                        theorem Phenomena.Reference.Studies.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.

                        source
                        theorem Phenomena.Reference.Studies.Krifka2026.concrete_concept_entity_asymmetry (h : Semantics.Dynamic.Core.KindAnaphora.HAssign Wld Ent) :
                        doesntOwnADog g₀ h → h 2 = Semantics.Dynamic.Core.DRefVal.concept dogConcept ∧ h 3 = Semantics.Dynamic.Core.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 @cite{krifka-2026} §4.

                        source
                        theorem Phenomena.Reference.Studies.Krifka2026.dog_kind_pronoun :
                        selectPronoun dogConcept.feature = KindPronoun.they

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

                        source
                        inductive Phenomena.Reference.Studies.Krifka2026.AnaphoricConstruction :
                        Type

                        Anaphoric constructions that pick up concept drefs.

                        @cite{krifka-2026} §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)

                        Instances For
                          source
                          instance Phenomena.Reference.Studies.Krifka2026.instDecidableEqAnaphoricConstruction :
                          DecidableEq AnaphoricConstruction
                          Equations
                          source
                          def Phenomena.Reference.Studies.Krifka2026.instReprAnaphoricConstruction.repr :
                          AnaphoricConstruction → ℕ → Std.Format
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            instance Phenomena.Reference.Studies.Krifka2026.instReprAnaphoricConstruction :
                            Repr AnaphoricConstruction
                            Equations
                            source
                            def Phenomena.Reference.Studies.Krifka2026.derivesKind :
                            AnaphoricConstruction → Bool

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

                            Equations
                            Instances For
                              source
                              theorem Phenomena.Reference.Studies.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. @cite{carlson-1977}), so kind anaphora yields the general dog-kind, while concept anaphora preserves the full NP property.