Quotative Inversion as Smuggling

[Sto26c]

Formalizes [Sto26c]: the smuggling derivation of quotative inversion in English and Setswana.

Storment's central claims

• §2 + §3: In QI clauses ("Hello," said Mary), the VP containing the quote moves to a position above the agentive AGENT, which remains in-situ in Spec,vP. Evidence: agreement, parasitic gaps, raising, conjoint/disjoint marking in Setswana.
• §4: This is smuggling ([Col05]): the VP moves to Spec,VoiceP, making the theme accessible to T⁰ for Case licensing. The smuggling projection is identified as VoiceP, which is not the external-argument-introducing head (departing from [Kra96]/Pylkkänen).
• §5: The transitivity constraint — QI is blocked when multiple DPs compete for Case licensing — falls out from the Case-licensing configuration after smuggling.
• §6: Locative inversion shares the same mechanism. QI and LI are both nonactive inverse-voice constructions.

Example rows live in Data/Examples/Storment2026.json (QI/LI data) and Data/Examples/LevinRappaportHovav1995.json (classic locative-inversion diagnostics).

§1 + §2. Lexical annotations and QI data

Per [Sto26c], every MoS verb passes the QI diagnostic and is classified unaccusative; the canonical communication verbs speak/ talk fail QI and are unergative. Quantified theorems collapse the per-verb pattern; specific instances are recoverable by fin_cases.

def Storment2026.mosUnaccusatives : List English.Predicates.Verbal.VerbEntry

MoS verbs annotated unaccusative on the basis of the QI diagnostic.

Equations

• One or more equations did not get rendered due to their size.

def Storment2026.communicationUnergatives : List English.Predicates.Verbal.VerbEntry

Canonical unergative communication verbs that fail QI.

Equations

• Storment2026.communicationUnergatives = [English.Predicates.Verbal.speak, English.Predicates.Verbal.talk]

theorem Storment2026.mos_unaccusatives_annotated (v : English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → v.unaccusative = true

theorem Storment2026.communication_unergatives_annotated (v : English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → v.unaccusative = false

theorem Storment2026.seem_unaccusative : English.Predicates.Verbal.seem.unaccusative = true

theorem Storment2026.arrive_unaccusative : English.Predicates.Verbal.arrive.unaccusative = true

§3. TransitivityClass derivation

Maps a Verb to the three-way transitivity classification used by the auxiliary-selection substrate (Typology/AuxiliaryVerbs.lean).

def Storment2026.deriveTransitivityClass (v : Verb) : ArgumentStructure.AuxiliarySelection.TransitivityClass

Derive TransitivityClass from Verb fields.

Equations

• One or more equations did not get rendered due to their size.

theorem Storment2026.mos_unaccusatives_transitivity (v : English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → deriveTransitivityClass v.toVerb = ArgumentStructure.AuxiliarySelection.TransitivityClass.unaccusative

theorem Storment2026.communication_unergatives_transitivity (v : English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → deriveTransitivityClass v.toVerb = ArgumentStructure.AuxiliarySelection.TransitivityClass.unergative

theorem Storment2026.kick_transitive : deriveTransitivityClass English.Predicates.Verbal.kick.toVerb = ArgumentStructure.AuxiliarySelection.TransitivityClass.transitive

§4. Voice bridge

Verb.voiceFor (defined in Semantics/Lexical/VerbSmuggling.lean) maps unaccusative→non-thematic Voice and unergative→agentive Voice. Per [Sto26c]'s §4.3, the Voice head is the smuggling projection (not the external-argument introducer of [Kra96]); permitting smuggling is equivalent to being non-phase, which is equivalent to not introducing an external argument.

theorem Storment2026.mos_unaccusatives_nonThematic_voice (v : English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → v.voiceFor = Minimalist.voiceAnticausative

theorem Storment2026.communication_unergatives_agentive_voice (v : English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → v.voiceFor = Minimalist.voiceAgent

§5. Auxiliary selection bridge

In split-auxiliary languages (Italian, French, German), unaccusatives select be and unergatives select have.

theorem Storment2026.mos_unaccusatives_select_be (v : English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → ArgumentStructure.AuxiliarySelection.canonicalSelection (deriveTransitivityClass v.toVerb) = ArgumentStructure.AuxiliarySelection.PerfectAux.be

theorem Storment2026.communication_unergatives_select_have (v : English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → ArgumentStructure.AuxiliarySelection.canonicalSelection (deriveTransitivityClass v.toVerb) = ArgumentStructure.AuxiliarySelection.PerfectAux.have

§6. Levin §37.3 mannerOfSpeaking class membership

Pure data — the divergence and within-class split analysis lives in ../Unaccusativity/VerbClasses.lean.

theorem Storment2026.whisper_levinClass : English.Predicates.Verbal.whisper.levinClass = some Semantics.Lexical.LevinClass.mannerOfSpeaking

theorem Storment2026.speak_levinClass : English.Predicates.Verbal.speak.levinClass = some Semantics.Lexical.LevinClass.mannerOfSpeaking

§8. Smuggling derivation of QI

Verb.derivedQI (defined in Semantics/Lexical/VerbSmuggling.lean) derives QI licensing from two independently motivated properties: (1) Voice is non-phase (= unaccusative); (2) verb has a complement (the quote).

These two properties are then verified against the empirical QI diagnostic data: every MoS unaccusative with a complement is correctly predicted to license QI; agentive speak/talk is correctly predicted to block QI; unaccusative arrive (no complement) is correctly predicted not to license QI (it requires LI, not QI).

theorem Storment2026.mos_unaccusatives_derivedQI (v : English.Predicates.Verbal.VerbEntry) : v ∈ mosUnaccusatives → v.derivedQI = true

theorem Storment2026.communication_unergatives_derivedQI (v : English.Predicates.Verbal.VerbEntry) : v ∈ communicationUnergatives → v.derivedQI = false

theorem Storment2026.arrive_no_qi : English.Predicates.Verbal.arrive.derivedQI = false

arrive is unaccusative but has no complement: doesn't license QI. This is correct — *"arrived Mary" requires a fronted locative (LI), not a fronted quote (QI).

theorem Storment2026.qi_data_matches_derivedQI (p : Data.Examples.LinguisticExample × Verb) : p ∈ [(Examples.qi_whisper, English.Predicates.Verbal.whisper.toVerb), (Examples.qi_murmur, English.Predicates.Verbal.murmur.toVerb), (Examples.qi_shout, English.Predicates.Verbal.shout.toVerb), (Examples.qi_cry, English.Predicates.Verbal.cry.toVerb), (Examples.qi_scream, English.Predicates.Verbal.scream.toVerb), (Examples.qi_mumble, English.Predicates.Verbal.mumble.toVerb), (Examples.qi_mutter, English.Predicates.Verbal.mutter.toVerb), (Examples.qi_shriek, English.Predicates.Verbal.shriek.toVerb), (Examples.qi_yell, English.Predicates.Verbal.yell.toVerb), (Examples.qi_groan, English.Predicates.Verbal.groan.toVerb), (Examples.qi_grumble, English.Predicates.Verbal.grumble.toVerb), (Examples.qi_hiss, English.Predicates.Verbal.hiss.toVerb), (Examples.qi_sigh, English.Predicates.Verbal.sigh.toVerb), (Examples.qi_whimper, English.Predicates.Verbal.whimper.toVerb), (Examples.qi_snap, English.Predicates.Verbal.snap.toVerb), (Examples.qi_speak, English.Predicates.Verbal.speak.toVerb), (Examples.qi_talk, English.Predicates.Verbal.talk.toVerb)] → (p.1.judgment = Features.Judgment.acceptable ↔ p.2.derivedQI = true)

Consistency: each (QI row, verb) pair has its judgment matching derivedQI. Pairs the rows of Data/Examples/Storment2026.json with the smuggling prediction.

§9. QI ∥ LI distributional contrasts (Storment §6)

Storment §6: QI and LI share the smuggling mechanism but differ in their inputs (quote vs. locative PP) and distribution. Both are subject to the transitivity constraint (§5). The shared inverse-voice family membership is captured by Minimalist.qiCanonical and liCanonical in Syntax/Minimalism/Movement/InverseVoice.lean.

theorem Storment2026.qi_li_diverge_on_whisper : Examples.qi_whisper.judgment = Features.Judgment.acceptable ∧ LevinRappaportHovav1995.Examples.loc_whisper.judgment = Features.Judgment.marginal

whisper passes QI but is only marginal in LI — same mechanism (smuggling), different inputs.

theorem Storment2026.qi_transitivity_constraint : Examples.qi_warn_double_obj.judgment = Features.Judgment.unacceptable ∧ Examples.qi_whisper_transitive.judgment = Features.Judgment.acceptable

The transitivity constraint (§5): QI is blocked with multiple DP arguments (using warn per Storment eq. 125, naturally ditransitive); QI is fine with a quote + PP goal.

theorem Storment2026.li_vs_qi_pronouns : Examples.li_arrive_pronoun.judgment = Features.Judgment.unacceptable ∧ Examples.qi_whisper_pronoun.judgment = Features.Judgment.marginal

LI categorically blocks pronominal subjects; QI merely degrades them.

theorem Storment2026.li_blocks_transitive : Examples.li_kick.judgment = Features.Judgment.unacceptable

LI blocks transitive verbs, just as QI does.

theorem Storment2026.li_arrive_smuggling_unified : English.Predicates.Verbal.arrive.voiceFor = Minimalist.voiceAnticausative ∧ LevinRappaportHovav1995.Examples.loc_arrive.judgment = Features.Judgment.acceptable

Unified smuggling analysis (§6): LI with arrive works because arrive projects non-thematic Voice, permitting VP-smuggling — the same mechanism that licenses QI.

§11 + §12. The QI derivation (Storment §3 + §4)

The smuggling derivation assigns each major constituent to a structural position. Each position predicts observable consequences tested against the §3 structural-evidence data.

Quote vs. quotative operator (Storment §3.5, eq. 103). The quote itself is not in the syntactic derivation — it may be totally absent from QI clauses (Says me!). What sits in Spec,TP is a null quotative operator (the THEME), bound by a Discourse⁰[QUOT] head in DiscourseP. The fields below distinguish the operator's landing site (Spec,TP) from the quote's binding head (DiscourseP).

inductive Storment2026.QIPosition : Type

Structural position in the QI derivation.

• specTP : QIPosition
• specVoiceP : QIPosition
• specvP : QIPosition
• discourseQUOT : QIPosition

@[implicit_reducible]

instance Storment2026.instDecidableEqQIPosition : DecidableEq QIPosition

Equations

• Storment2026.instDecidableEqQIPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Storment2026.instReprQIPosition : Repr QIPosition

Equations

• Storment2026.instReprQIPosition = { reprPrec := Storment2026.instReprQIPosition.repr }

def Storment2026.instReprQIPosition.repr : QIPosition → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Storment2026.QIDerivation : Type

The QI derivation assigns four major constituents to structural positions. Note that quoteBinder is the binding head in DiscourseP, not the quote itself (which is not in the syntax — Storment §3.5).

• themePosition : QIPosition
• agentPosition : QIPosition
• vpPosition : QIPosition
• quoteBinder : QIPosition

@[implicit_reducible]

instance Storment2026.instReprQIDerivation : Repr QIDerivation

Equations

• Storment2026.instReprQIDerivation = { reprPrec := Storment2026.instReprQIDerivation.repr }

def Storment2026.instReprQIDerivation.repr : QIDerivation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Storment2026.instBEqQIDerivation.beq : QIDerivation → QIDerivation → Bool

Equations

• One or more equations did not get rendered due to their size.
• Storment2026.instBEqQIDerivation.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Storment2026.instBEqQIDerivation : BEq QIDerivation

Equations

• Storment2026.instBEqQIDerivation = { beq := Storment2026.instBEqQIDerivation.beq }

def Storment2026.qiSmuggling : QIDerivation

Storment's smuggling derivation of QI.

Equations

• One or more equations did not get rendered due to their size.

Each structural position predicts an observable property. We verify each prediction against the §3 rows. The bridge theorems below pair the position assignment (Storment's claim) with the empirical observation (also Storment's claim).

theorem Storment2026.theme_specTP_agreement : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.qi_agreement_english.judgment = Features.Judgment.acceptable

Theme-as-operator in Spec,TP → agreement can track agent via defective circumvention (§3.1).

theorem Storment2026.theme_specTP_setswana_sm17 : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.qi_agreement_setswana.judgment = Features.Judgment.acceptable

Theme-as-operator is phi-deficient → Setswana SM surfaces as default SM17 (§3.1).

theorem Storment2026.theme_specTP_no_parasitic_gap : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.qi_parasitic_gap_blocked.judgment = Features.Judgment.unacceptable ∧ Examples.qi_parasitic_gap_baseline.judgment = Features.Judgment.acceptable

Theme-as-operator A-moves → cannot license parasitic gaps, unlike the A-bar-moved preposed quote of the non-QI baseline (§3.2).

theorem Storment2026.theme_specTP_raising : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.qi_raising.judgment = Features.Judgment.acceptable

Theme-as-operator A-moves → compatible with subject-to-subject raising (§3.3).

theorem Storment2026.agent_specvP_conjoint : qiSmuggling.agentPosition = QIPosition.specvP ∧ Examples.qi_conjoint_disjoint.judgment = Features.Judgment.unacceptable

Agent in Spec,vP → Setswana disjoint morpheme blocked (§3.4).

theorem Storment2026.quote_discourseQUOT_split : qiSmuggling.quoteBinder = QIPosition.discourseQUOT ∧ Examples.qi_quote_split.judgment = Features.Judgment.acceptable ∧ Examples.qi_quote_nongrammatical.judgment = Features.Judgment.acceptable

Quote (separately from operator) bound by Discourse⁰[QUOT] → can split around verb + agent, need not be grammatical (§3.5).

theorem Storment2026.vp_smuggling_ordering : qiSmuggling.vpPosition = QIPosition.specVoiceP ∧ Examples.qi_ordering_complement.judgment = Features.Judgment.acceptable ∧ Examples.qi_ordering_depictive.judgment = Features.Judgment.acceptable ∧ Examples.qi_ordering_manner.judgment = Features.Judgment.acceptable ∧ Examples.qi_ordering_purpose.judgment = Features.Judgment.acceptable

VP smuggling predicts: VP-internal material (complements) precedes Agent; vP-external material (adjuncts) follows Agent (§2).

§13. Inverse-voice family membership

QI is one instance of the inverse-voice family (§4.3 + §6 + §7). The canonical instance lives in Syntax/Minimalism/Movement/ InverseVoice.lean; here we just affirm membership.

theorem Storment2026.qi_is_inverse_voice : Minimalist.qiCanonical.kind = Minimalist.InverseVoiceKind.quotativeInversion ∧ Minimalist.qiCanonical.licensed = true

theorem Storment2026.qi_li_share_voice : Minimalist.qiCanonical.voice = Minimalist.liCanonical.voice

§14. Defective circumvention derives the agreement contrast

Storment §3.1.4 (eq. 59): the difference between Setswana QI agreement (always SM17 default) and English QI agreement (optionally tracks the postverbal agent) reduces to a single parameter — whether the probe T⁰ is allowed to re-probe past the defective quotative-theme operator. Roberts's defective goal and the defective-circumvention operation are defined inline below (folded in from the former single-consumer Minimalist/Probing/); the theorems then wire them to the QI data.

The theorems abstract over the precise feature bundles and feature- compatibility predicate — Storment's substantive claim is that the operation is the same and only the allowReprobe parameter varies.

def Storment2026.DefectiveGoal (probe goal : Minimalist.FeatureBundle) : Prop

A goal G is defective w.r.t. a probe P iff G's formal features are a proper subset of P's, so checking is incomplete ([Rob10], ch. 2; eq. (49) in [Sto26c]). The feature comparison is over the bundles' grammatical-feature lists (FeatureBundle.toGramFeatures).

Equations

• Storment2026.DefectiveGoal probe goal = (goal.toGramFeatures ⊆ probe.toGramFeatures ∧ ∃ f ∈ probe.toGramFeatures, f ∉ goal.toGramFeatures)

@[implicit_reducible]

instance Storment2026.instDecidableDefectiveGoal (probe goal : Minimalist.FeatureBundle) : Decidable (DefectiveGoal probe goal)

Equations

• Storment2026.instDecidableDefectiveGoal probe goal = id inferInstance

theorem Storment2026.DefectiveGoal.empty_of_nonempty (probe : Minimalist.FeatureBundle) (h : probe ≠ ⊥) : DefectiveGoal probe ⊥

The empty goal is defective w.r.t. any nonempty probe.

theorem Storment2026.DefectiveGoal.exists_missing {probe goal : Minimalist.FeatureBundle} (h : DefectiveGoal probe goal) : ∃ f ∈ probe.toGramFeatures, f ∉ goal.toGramFeatures

A defective goal is missing some feature the probe has.

theorem Storment2026.DefectiveGoal.subset {probe goal : Minimalist.FeatureBundle} (h : DefectiveGoal probe goal) : goal.toGramFeatures ⊆ probe.toGramFeatures

A defective goal's features are all in the probe.

theorem Storment2026.DefectiveGoal.irrefl (fb : Minimalist.FeatureBundle) : ¬DefectiveGoal fb fb

No goal is defective w.r.t. itself.

inductive Storment2026.ProbingOutcome : Type

The four outcomes of a probe that may invoke defective circumvention ([Sto25] ch. 2; eq. 59 in [Sto26c]): the probe Agrees with a higher defective goal α, then conditionally re-probes past α to a lower, more specified goal β.

• trackHigher : ProbingOutcome

  α was not defective; α suffices, no re-probe.

• defaultAgreement : ProbingOutcome

  α defective; re-probe disallowed; default features spell out.

• trackLower : ProbingOutcome

  α defective; re-probe to β succeeded (features compatible).

• featureClash : ProbingOutcome

  α defective; re-probe to β attempted but features conflict; crash.

@[implicit_reducible]

instance Storment2026.instDecidableEqProbingOutcome : DecidableEq ProbingOutcome

Equations

• Storment2026.instDecidableEqProbingOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Storment2026.instReprProbingOutcome : Repr ProbingOutcome

Equations

• Storment2026.instReprProbingOutcome = { reprPrec := Storment2026.instReprProbingOutcome.repr }

def Storment2026.instReprProbingOutcome.repr : ProbingOutcome → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Storment2026.defectiveCircumvention (probe alpha beta : Minimalist.FeatureBundle) (allowReprobe : Bool) (compatible : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) : ProbingOutcome

Defective-circumvention probing, parameterized by allowReprobe (may the probe search past a defective goal) and compatible (can circumvention complete without feature conflict).

Equations

• One or more equations did not get rendered due to their size.

theorem Storment2026.defectiveCircumvention_trackHigher_of_nondefective (probe alpha beta : Minimalist.FeatureBundle) (allowReprobe : Bool) (compatible : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (h : ¬DefectiveGoal probe alpha) : defectiveCircumvention probe alpha beta allowReprobe compatible = ProbingOutcome.trackHigher

A non-defective higher goal never invokes circumvention.

theorem Storment2026.defectiveCircumvention_default_when_no_reprobe (probe alpha beta : Minimalist.FeatureBundle) (compatible : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : DefectiveGoal probe alpha) : defectiveCircumvention probe alpha beta false compatible = ProbingOutcome.defaultAgreement

Defective higher goal, re-probe disallowed → default agreement (Setswana case).

theorem Storment2026.defectiveCircumvention_tracks_lower (probe alpha beta : Minimalist.FeatureBundle) (compatible : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : DefectiveGoal probe alpha) (hc : compatible alpha beta = true) : defectiveCircumvention probe alpha beta true compatible = ProbingOutcome.trackLower

Defective higher goal, re-probe allowed, β compatible → tracks β (English advise the dieticians).

theorem Storment2026.defectiveCircumvention_clash_on_incompatible (probe alpha beta : Minimalist.FeatureBundle) (compatible : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : DefectiveGoal probe alpha) (hc : compatible alpha beta = false) : defectiveCircumvention probe alpha beta true compatible = ProbingOutcome.featureClash

Defective higher goal, re-probe allowed, β incompatible → crash (English *ask we).

theorem Storment2026.setswana_vs_english_reduces_to_reprobe (probe alpha beta : Minimalist.FeatureBundle) (compat : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : DefectiveGoal probe alpha) (hc : compat alpha beta = true) : defectiveCircumvention probe alpha beta false compat = ProbingOutcome.defaultAgreement ∧ defectiveCircumvention probe alpha beta true compat = ProbingOutcome.trackLower

The same defective-probing situation produces Setswana's obligatory default agreement (no re-probe) and English's optional agent-tracking agreement (re-probe with compatible features) — a single Bool parameter accounts for the cross-linguistic split.

theorem Storment2026.english_qi_clash_on_incompatible_agent (probe alpha beta : Minimalist.FeatureBundle) (compat : Minimalist.FeatureBundle → Minimalist.FeatureBundle → Bool) (hd : DefectiveGoal probe alpha) (hc : compat alpha beta = false) : defectiveCircumvention probe alpha beta true compat = ProbingOutcome.featureClash

Storment's English-specific prediction: a 1st/2nd person agent (whose phi-features clash with the defective theme's [3]) cannot license re-probe — *"What do we do now?" ask we. The derivation crashes on feature incompatibility (eq. 46, page 14).