Storment (2026): Quotative Inversion as Smuggling

This file formalizes [Sto26c]'s analysis of quotative inversion in English and Setswana, the order in which a quote precedes the verb and the agent follows it, as smuggling: the VP moves to Spec,VoiceP over the agent, which stays in Spec,vP, and the quotative theme A-moves on to Spec,TP (qiSmuggling, (122)). The paper's four arguments are theorems over its examples (Data/Examples/Storment2026.json): VP complements precede the agent and vP adjuncts follow it, in both languages (§2, order_predicted); the agent is in situ, since Setswana agreement is the default class 17, English agreement tracks the agent by defective circumvention, the theme licenses no parasitic gap, raises, and the disjoint form is excluded (§3); the transitivity constraint follows from T⁰ licensing at most one smuggled DP, so a goal DP blocks inversion and a PP or adjunct goal does not (§5, transitivity_predicted); and locative inversion shares the mechanism and the constraint (§6). The paper places quotative inversion in a family of inverse voice constructions (§4.3, InverseVoiceKind).

Implementation notes

• The Voice head of the paper is the smuggling projection and not the introducer of the external argument (§4.3); nothing here classifies the verbs of quotative inversion as unaccusative, which the paper does not do.
• Heavy NP shift (14) lets an adjunct precede the agent; the row is data and outside the ordering theorem.

References

• [Sto26c]
• [Rob10]
• [Sto25]

The derivation (§4)

inductive Storment2026.QIPosition : Type

The structural positions of the smuggling derivation (122).

• specTP : QIPosition

  The A-movement landing site of the quotative theme.

• specVoiceP : QIPosition

  The landing site of the smuggled VP.

• specvP : QIPosition

  The in-situ position of the agent.

• discourseQUOT : QIPosition

  The discourse head bearing the quotation feature that binds the theme.

@[instance_reducible]

instance Storment2026.instDecidableEqQIPosition : DecidableEq QIPosition

Equations

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

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

Equations

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

@[instance_reducible]

instance Storment2026.instReprQIPosition : Repr QIPosition

Equations

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

structure Storment2026.QIDerivation : Type

The positions of the theme, the agent, the VP and the quote's binder (§3.5, §4).

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

def Storment2026.instDecidableEqQIDerivation.decEq (x✝ x✝¹ : QIDerivation) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Storment2026.instDecidableEqQIDerivation : DecidableEq QIDerivation

Equations

• Storment2026.instDecidableEqQIDerivation = Storment2026.instDecidableEqQIDerivation.decEq

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

Equations

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

@[instance_reducible]

instance Storment2026.instReprQIDerivation : Repr QIDerivation

Equations

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

def Storment2026.qiSmuggling : QIDerivation

The paper's derivation of quotative inversion (122).

Equations

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

VP movement over the agent (§2)

Material inside the VP moves with it above the agent; material adjoined to vP stays below.

inductive Storment2026.Material : Type

Where a constituent sits relative to the VP.

• vpComplement : Material
• vpAdjunct : Material

@[instance_reducible]

instance Storment2026.instDecidableEqMaterial : DecidableEq Material

Equations

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

@[instance_reducible]

instance Storment2026.instReprMaterial : Repr Material

Equations

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

def Storment2026.instReprMaterial.repr : Material → ℕ → Std.Format

Equations

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

inductive Storment2026.Position : Type

Where a constituent surfaces relative to the agent.

• beforeAgent : Position
• afterAgent : Position

@[instance_reducible]

instance Storment2026.instDecidableEqPosition : DecidableEq Position

Equations

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

def Storment2026.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Storment2026.instReprPosition : Repr Position

Equations

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

def Storment2026.predictedPosition (d : QIDerivation) : Material → Position

The derivation predicts that a VP complement is smuggled to Spec,VoiceP above the agent and a vP adjunct is not.

Equations

• One or more equations did not get rendered due to their size.
• Storment2026.predictedPosition d Storment2026.Material.vpAdjunct = Storment2026.Position.afterAgent

def Storment2026.orderOf (ex : Datum) : Option (Material × Position)

The material and position a row records.

Equations

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

theorem Storment2026.order_predicted (ex : Datum) : ex ∈ Examples.all → ex.feature? "heavyNPShift" = none → ∀ o ∈ orderOf ex, ex.judgment = Judgment.acceptable ↔ o.2 = predictedPosition qiSmuggling o.1

In (10)–(31), a quotative inversion is acceptable exactly when its constituent surfaces where the smuggling derivation puts it, complements before the agent and adjuncts after.

The agent in situ (§3)

Each position of the derivation predicts a diagnostic.

theorem Storment2026.theme_specTP_setswana_agreement : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.ex36.judgment = Judgment.acceptable ∧ Examples.ex36_sm10.judgment = Judgment.ungrammatical ∧ Examples.ex38.judgment = Judgment.acceptable ∧ Examples.ex38_ke.judgment = Judgment.ungrammatical ∧ Examples.ex65.judgment = Judgment.acceptable ∧ Examples.ex65_ga.judgment = Judgment.ungrammatical

The theme A-moves to Spec,TP, so Setswana agreement is the default class 17 and never the agent's class (36), (38), whereas a preposed quote without inversion leaves the agent in Spec,TP and its agreement (65).

theorem Storment2026.theme_specTP_english_agreement : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.ex40.judgment = Judgment.acceptable ∧ Examples.ex40_sg.judgment = Judgment.ungrammatical ∧ Examples.ex64.judgment = Judgment.acceptable ∧ Examples.ex64_sg.judgment = Judgment.ungrammatical

English agreement tracks the postverbal agent (40), by re-probing past the defective theme (defectiveCircumvention), as it must without inversion (64).

theorem Storment2026.theme_specTP_no_parasitic_gap : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.ex62a.judgment = Judgment.ungrammatical ∧ Examples.ex62b.judgment = Judgment.acceptable

The A-moved theme licenses no parasitic gap (62a); the Ā-moved preposed quote does (62b).

theorem Storment2026.theme_specTP_raising : qiSmuggling.themePosition = QIPosition.specTP ∧ Examples.ex67a.judgment = Judgment.acceptable ∧ Examples.ex69a.judgment = Judgment.ungrammatical ∧ Examples.ex77.judgment = Judgment.acceptable

The theme raises (67a), (77), as the Ā-moved preposed quote cannot (69a).

theorem Storment2026.agent_specvP_conjoint : qiSmuggling.agentPosition = QIPosition.specvP ∧ Examples.ex87.judgment = Judgment.acceptable ∧ Examples.ex87_disj.judgment = Judgment.ungrammatical

The agent stays in the vP, so the disjoint form, which needs an empty vP, is excluded (87).

theorem Storment2026.quote_discourseQUOT : qiSmuggling.quoteBinder = QIPosition.discourseQUOT ∧ Examples.ex88.judgment = Judgment.acceptable ∧ Examples.ex89.judgment = Judgment.acceptable ∧ Examples.ex90.judgment = Judgment.acceptable ∧ Examples.ex92.judgment = Judgment.acceptable ∧ Examples.ex96a.judgment = Judgment.acceptable ∧ Examples.ex97a.judgment = Judgment.acceptable ∧ Examples.ex93a.judgment = Judgment.ungrammatical

The quote is bound by the discourse head rather than moved: it may stay postverbal (88), (89), split around the verb and the agent (90), (92), and need not be a constituent or grammatical (96a), (97a), unlike the fronted phrase of locative inversion (93a).

The transitivity constraint (§5)

A smuggled DP is licensed by T⁰, which licenses one argument; Voice⁰ licenses the agent (133).

def Storment2026.Licensed (smuggledDPs : ℕ) : Prop

The smuggled constituent is licensed when it carries at most one DP for T⁰.

Equations

• Storment2026.Licensed smuggledDPs = (smuggledDPs ≤ 1)

@[instance_reducible]

instance Storment2026.instDecidableLicensed (n : ℕ) : Decidable (Licensed n)

Equations

• Storment2026.instDecidableLicensed n = { decide := n.ble 1, reflects_decide := ⋯ }

theorem Storment2026.transitivity_predicted (ex : Datum) : ex ∈ Examples.all → ∀ n ∈ ex.parse? "smuggledDPs" [("1", 1), ("2", 2)], ex.judgment = Judgment.acceptable ↔ Licensed n

In (125)–(135), an inversion is acceptable exactly when the smuggled constituent carries at most one DP, a goal DP blocking it and a PP or adjunct goal not, in quotative and locative inversion alike.

Inverse voice (§4.3, §6)

Quotative inversion joins the constructions the paper analyses as smuggling through VoiceP, and locative inversion shows the same in-situ agent, raising and transitivity constraint.

inductive Storment2026.InverseVoiceKind : Type

The constructions the paper groups as inverse voice, analysed as smuggling (§4.3).

• passive : InverseVoiceKind
• dativeShift : InverseVoiceKind
• causative : InverseVoiceKind
• middle : InverseVoiceKind
• inverseVoice : InverseVoiceKind
• quotativeInversion : InverseVoiceKind
• locativeInversion : InverseVoiceKind

@[instance_reducible]

instance Storment2026.instDecidableEqInverseVoiceKind : DecidableEq InverseVoiceKind

Equations

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

@[instance_reducible]

instance Storment2026.instReprInverseVoiceKind : Repr InverseVoiceKind

Equations

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

def Storment2026.instReprInverseVoiceKind.repr : InverseVoiceKind → ℕ → Std.Format

Equations

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

theorem Storment2026.locative_inversion_parallel : Examples.ex136a.judgment = Judgment.acceptable ∧ Examples.ex55.judgment = Judgment.acceptable ∧ Examples.ex138.judgment = Judgment.acceptable ∧ Examples.ex134a.judgment = Judgment.ungrammatical ∧ Examples.ex135.judgment = Judgment.ungrammatical

Locative inversion parallels quotative inversion: it is acceptable with an unergative verb of motion (136a) and with arrive in Setswana (55), raises the same way (138), and obeys the transitivity constraint (134a), (135).

§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' specified slots (FeatureBundle.toList).

Equations

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

@[instance_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.toList, f ∉ goal.toList

A defective goal is missing some feature the probe has.

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

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.

@[instance_reducible]

instance Storment2026.instDecidableEqProbingOutcome : DecidableEq ProbingOutcome

Equations

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

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

Equations

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

@[instance_reducible]

instance Storment2026.instReprProbingOutcome : Repr ProbingOutcome

Equations

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

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).