Documentation

Linglib.Syntax.Binding.SpecificityCondition

Specificity Condition #

[Fie87] [Hua82c] [SH26]

A variable inside a specific DP cannot be bound by an operator outside that DP. This is a binding-theoretic constraint on wh-dependencies, independent of movement or the PIC.

Two notions of "specificity" #

[Fie87] ties specificity to Heim's familiarity theory of definiteness: a specific nominal is one whose referent is "already familiar at the current stage of the conversation." Demonstrative-marked DPs are paradigmatically specific in this sense.

[CS99b] use "specificity" differently — for them it is about whether an indefinite nominal gets a particular-individual reading. Bounded predicates (e.g., perfective VPs) force a "specific" reading on indefinite objects, but these DPs are NOT islands for subextraction. [SH26] §2.2 argue that the extraction-relevant notion is Fiengo's familiarity-based specificity, not Cheng & Sybesma's.

Coverage #

The Specificity Condition accounts for:

  1. Definite island effects in wh-movement (English: [Cho73])
  2. Definite island effects in wh-in-situ (Mandarin Chinese: [Hua82c], [SH26])
  3. Wh-indefinite sensitivity to demonstratives in Chinese ([Li92], [SH26] Experiment 3)
  4. Island effects for relativization ([Ros67])
  5. Island effects for unselective binding ([Li92])

The PIC independently constrains overt movement; the Specificity Condition independently constrains binding. Both are needed for full crosslinguistic coverage ([SH26] §4.1).

source
def Syntax.Binding.SpecificityCondition.isSpecific (d : Features.Definiteness.Definiteness) :
Prop

A DP is specific iff its referent is discourse-familiar in the sense of [Fie87]: "already familiar at the current stage of the conversation."

Demonstrative-marked DPs are specific; indefinite DPs (introduced with a/an, one-CL) are nonspecific. This is the extraction-relevant notion, not [CS99b]'s predicate-dependent specificity.

Equations
Instances For
    source
    @[implicit_reducible]
    instance Syntax.Binding.SpecificityCondition.instDecidableIsSpecific (d : Features.Definiteness.Definiteness) :
    Decidable (isSpecific d)
    Equations
    source
    theorem Syntax.Binding.SpecificityCondition.demonstratives_are_specific :
    isSpecific Features.Definiteness.Definiteness.definite

    Demonstratives project the familiarity/strong-article layer, hence are always specific for purposes of the Specificity Condition.

    source
    inductive Syntax.Binding.SpecificityCondition.ExternalOperator :
    Type

    The kind of operator attempting to bind into the DP.

    Instances For
      source
      @[implicit_reducible]
      instance Syntax.Binding.SpecificityCondition.instDecidableEqExternalOperator :
      DecidableEq ExternalOperator
      Equations
      source
      @[implicit_reducible]
      instance Syntax.Binding.SpecificityCondition.instReprExternalOperator :
      Repr ExternalOperator
      Equations
      source
      def Syntax.Binding.SpecificityCondition.instReprExternalOperator.repr :
      ExternalOperator → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Syntax.Binding.SpecificityCondition.blocked (_op : ExternalOperator) (dpSpecificity : Features.Definiteness.Definiteness) :
        Prop

        Whether an external operator's binding into a DP is blocked by the Specificity Condition.

        A variable inside a specific DP cannot be bound by an operator
outside the DP.

[shen-huang-2026]: this condition applies uniformly to both
overt wh-movement (where the "variable" is a trace) and wh-in-situ
(where the "variable" is the in-situ wh-phrase itself, bound by
a covert question operator).

Holds when binding is BLOCKED.
        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Syntax.Binding.SpecificityCondition.instDecidableBlocked (op : ExternalOperator) (d : Features.Definiteness.Definiteness) :
          Decidable (blocked op d)
          Equations
          source
          theorem Syntax.Binding.SpecificityCondition.blocks_definite (op : ExternalOperator) :
          blocked op Features.Definiteness.Definiteness.definite

          Specificity Condition blocks binding into definite DPs.

          source
          theorem Syntax.Binding.SpecificityCondition.allows_indefinite (op : ExternalOperator) :
          ¬blocked op Features.Definiteness.Definiteness.indefinite

          Specificity Condition allows binding into indefinite DPs.

          source
          theorem Syntax.Binding.SpecificityCondition.operator_insensitive (op₁ op₂ : ExternalOperator) (d : Features.Definiteness.Definiteness) :
          blocked op₁ d ↔ blocked op₂ d

          The Specificity Condition is insensitive to operator type — it blocks all external operators equally when the DP is specific. This is the key prediction that distinguishes it from the PIC, which is sensitive to movement type.

          source
          theorem Syntax.Binding.SpecificityCondition.wh_indefinite_blocked_in_specific_dp :
          blocked ExternalOperator.existentialClosure Features.Definiteness.Definiteness.definite

          In Chinese, wh-phrases can be interpreted as indefinites ("something", "someone") when bound by an existential closure operator. [Li92] reports that this indefinite reading is blocked when the wh-phrase appears inside a demonstrative-marked (specific) DP.

          (i)  Wǒ yǐwéi tā ná-le [yì-zhāng shénme rén de xiàngpiàn]. ✓
     'I thought he took away a picture of someone.'
(ii) *Wǒ yǐwéi tā ná-le [nà-zhāng shénme rén de xiàngpiàn]. ✗
     Intended: 'I thought he took away that picture of someone.'

          [SH26] Experiment 3 confirms this contrast experimentally (β = −0.48, s.e. = 0.15, t = −3.32, p < 0.01).

          source
          theorem Syntax.Binding.SpecificityCondition.wh_indefinite_allowed_in_nonspecific_dp :
          ¬blocked ExternalOperator.existentialClosure Features.Definiteness.Definiteness.indefinite