Documentation

Linglib.Theories.Syntax.Binding.SpecificityCondition

Specificity Condition #

@cite{fiengo-1987} @cite{huang-1982b} @cite{shen-huang-2026}

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" #

@cite{fiengo-1987} 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.

@cite{cheng-sybesma-1999} 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. @cite{shen-huang-2026} §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: @cite{chomsky-1973})
  2. Definite island effects in wh-in-situ (Mandarin Chinese: @cite{huang-1982b}, @cite{shen-huang-2026})
  3. Wh-indefinite sensitivity to demonstratives in Chinese (@cite{li-1992}, @cite{shen-huang-2026} Experiment 3)
  4. Island effects for relativization (@cite{ross-1967})
  5. Island effects for unselective binding (@cite{li-1992})

The PIC independently constrains overt movement; the Specificity Condition independently constrains binding. Both are needed for full crosslinguistic coverage (@cite{shen-huang-2026} §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 @cite{fiengo-1987}: "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 @cite{cheng-sybesma-1999}'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.

    • whTrace : ExternalOperator

      Overt wh-movement leaves a trace/copy inside the DP

    • questionOperator : ExternalOperator

      Covert question operator binds an in-situ wh-phrase (@cite{li-1992}, @cite{aoun-li-1993})

    • existentialClosure : ExternalOperator

      Existential closure binds a wh-indefinite (@cite{li-1992}: wh-phrases as indefinites)

    • relOperator : ExternalOperator

      Relativization operator

    • focusOperator : ExternalOperator

      Focus operator

    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.

@cite{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. @cite{li-1992} 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.'

          @cite{shen-huang-2026} 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