Documentation

Linglib.Semantics.Lexical.VerbSmuggling

Verb ↔ Smuggling Interface #

[Col05] [Sto26c] [Kra96]

Promotes the bridge from Verb's lexical fields to the smuggling operators in Syntax/Minimalism/Movement/Smuggling.lean. These are general operations on Verb reused across argument-structure studies (QI, locative inversion, passives), not study-local helpers.

Composition #

Verb.derivedUnaccusative  →  Verb.voiceFor : VoiceHead
Verb.complementType       →  Verb.hasComplement : Bool
                                       ↓
                         Verb.derivedQI = licensesQI ∘ voiceFor ∘ hasComplement

voiceFor consults Verb.derivedUnaccusative (which itself reads voiceType.assignsTheta when present), keeping the chain rooted in the deeper Voice-as-not-introducing-external-argument characterization rather than the surface unaccusative : Bool annotation.

source
def Verb.hasComplement (v : Verb) :
Bool

A verb has a syntactic complement iff its complementType is anything other than .none. Used by smuggling derivations to check that there is something to smuggle.

Equations
Instances For
    source
    def Verb.voiceFor (v : Verb) :
    Minimalist.VoiceHead

    The Voice head determined by a verb's derived unaccusativity: non-thematic (anticausative) for unaccusatives, agentive for unergatives. Reads derivedUnaccusative, which consults voiceType.assignsTheta when present, so the bridge is grounded in the Voice-as-not-introducing- external-argument characterization ([Kra96]).

    Equations
    Instances For
      source
      def Verb.derivedQI (v : Verb) :
      Bool

      Derived prediction: does the verb license quotative inversion? Composes voiceFor and hasComplement through licensesQI ([Sto26c], §4: smuggling requires non-phase Voice + a complement to smuggle).

      Equations
      Instances For
        source
        theorem Verb.derivedQI_iff (v : Verb) :
        v.derivedQI = true ↔ v.voiceFor.permitsSmuggling = true ∧ v.hasComplement = true

        A verb licenses QI iff its derived Voice permits smuggling and it has a complement to smuggle. Direct unfolding from licensesQI's definition.

        source
        theorem Verb.voiceFor_of_unaccusative (v : Verb) (h : v.derivedUnaccusative = true) :
        v.voiceFor = Minimalist.voiceAnticausative

        Unaccusative verbs project non-thematic (anticausative) Voice.

        source
        theorem Verb.voiceFor_of_unergative (v : Verb) (h : v.derivedUnaccusative = false) :
        v.voiceFor = Minimalist.voiceAgent

        Unergative verbs project agentive Voice.

        source
        theorem Verb.derivedQI_of_unaccusative_with_complement (v : Verb) (hu : v.derivedUnaccusative = true) (hc : v.hasComplement = true) :
        v.derivedQI = true

        An unaccusative verb with a complement licenses QI. The two independent properties — non-phase Voice and complement availability — suffice.

        source
        theorem Verb.derivedQI_blocked_when_unergative (v : Verb) (hu : v.derivedUnaccusative = false) :
        v.derivedQI = false

        An unergative verb cannot license QI (regardless of complement), because agentive Voice blocks smuggling.