Citko and Gračanin-Yuksek (2025): Economy in PF Reduction: Why and When (Not) to Elide Multidominant Structures

Material can go unpronounced in two ways: shared between conjuncts (multidominance) or elided. Citko and Gračanin-Yuksek argue that economy chooses between them. Among the admissible derivations of a string with a given reading, the one spending the fewest lexical items, Merges and ellipses wins, and a derivation is admissible when none of its ellipses is vacuous (Pronunciation Economy) and no phase edge hosting several wh-phrases reaches PF in a language that bans multiple wh-fronting there. A coordinated wh-question (What and when should you teach?) therefore shares its heads but not its phrases, while a coordinated sluice (I forgot what and when) shares its whole C′ and elides it once, which hides the vP edge both wh-phrases crossed.

Main statements

• optimal_cwh_iff: in English the coordinated wh-question has one optimal derivation, which shares heads and leaves each wh-phrase in its own conjunct.
• optimal_cs_iff: in every language the coordinated sluice has two optimal derivations, the elided shared C′ of the paired reading, which displaces the authors' earlier double ellipsis, and, for the nonpaired reading, shared heads under two complementizers of which only one bears [E].
• convergesIn_multipleSluice_iff: multiple sluicing converges exactly where the CP edge may host several wh-phrases, as in German, Greek and one variety of English.
• rnr56_economy: in right node raising with matching verbs, sharing the whole verb phrase is cheaper than eliding part of it, so economy blocks two of the three derivations Belk, Neeleman and Philip license.

Implementation notes

• A candidate is a planar syntactic object spelled out by Linearization/Spellout.lean: a token at two positions is shared, a moved wh-phrase leaves traces at the vP edge and its base position, and the coordinator is left out, so a string is its conjuncts' words. A right node raising candidate is a pruning derivation of Belk, Neeleman and Philip, each free pruning an ellipsis.
• The paired reading and Pronunciation Economy are the it reading and the ban on vacuous ellipsis of the authors' earlier paper (CitkoGracaninYuksek2020).
• As the paper's footnote on the parameter allows, every edge with several wh-specifiers receives an asterisk, and a language is the set of categories whose asterisks PF cannot interpret.
• The candidates are the derivations the paper compares; optimality is minimality among them (MinimalFor) under the pointwise order on costs.

References

• B. Citko and M. Gračanin-Yuksek, Economy in PF Reduction: Why and When (Not) to Elide Multidominant Structures (2025)
• B. Citko and M. Gračanin-Yuksek, Conjunction saves multiple sluicing: How *(and) why? (2020)
• N. Chomsky, Some notes on economy of derivation and representation (1991)
• J. Merchant, The Syntax of Silence (2001)
• M. Marcolli, N. Chomsky and R. C. Berwick, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics (2025)
• Z. Belk, A. Neeleman and J. Philip, What divides, and what unites, right-node raising (2023)

The lexicon

def CitkoGracaninYuksek2025.what : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.what = CitkoGracaninYuksek2020.tok 1 Minimalist.Cat.D [] "what" true

def CitkoGracaninYuksek2025.when : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.when = CitkoGracaninYuksek2020.tok 2 Minimalist.Cat.P [] "when" true

def CitkoGracaninYuksek2025.who : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.who = CitkoGracaninYuksek2020.tok 3 Minimalist.Cat.D [] "who" true

def CitkoGracaninYuksek2025.you : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.you = CitkoGracaninYuksek2020.tok 4 Minimalist.Cat.D [] "you"

def CitkoGracaninYuksek2025.T : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.T = CitkoGracaninYuksek2020.tok 5 Minimalist.Cat.T [Minimalist.Cat.v]

def CitkoGracaninYuksek2025.v : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.v = CitkoGracaninYuksek2020.tok 6 Minimalist.Cat.v [Minimalist.Cat.V]

def CitkoGracaninYuksek2025.teach : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.teach = CitkoGracaninYuksek2020.tok 7 Minimalist.Cat.V [Minimalist.Cat.D] "teach"

def CitkoGracaninYuksek2025.should : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.should = CitkoGracaninYuksek2020.tok 8 Minimalist.Cat.C [Minimalist.Cat.T] "should"

def CitkoGracaninYuksek2025.will : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.will = CitkoGracaninYuksek2020.tok 9 Minimalist.Cat.C [Minimalist.Cat.T] "will"

def CitkoGracaninYuksek2025.c : Minimalist.LexicalItem.Token

The null complementizer, and a second one.

Equations

• CitkoGracaninYuksek2025.c = CitkoGracaninYuksek2020.tok 10 Minimalist.Cat.C [Minimalist.Cat.T]

def CitkoGracaninYuksek2025.c' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.c' = CitkoGracaninYuksek2020.tok 11 Minimalist.Cat.C [Minimalist.Cat.T]

def CitkoGracaninYuksek2025.cE : Minimalist.LexicalItem.Token

The null complementizer bearing [E], and a second one.

Equations

• CitkoGracaninYuksek2025.cE = CitkoGracaninYuksek2020.tok 12 Minimalist.Cat.C [Minimalist.Cat.T] "" false true

def CitkoGracaninYuksek2025.cE' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.cE' = CitkoGracaninYuksek2020.tok 13 Minimalist.Cat.C [Minimalist.Cat.T] "" false true

def CitkoGracaninYuksek2025.you' : Minimalist.LexicalItem.Token

The tokens a second, separately built clause draws.

Equations

• CitkoGracaninYuksek2025.you' = CitkoGracaninYuksek2020.tok 14 Minimalist.Cat.D [] "you"

def CitkoGracaninYuksek2025.T' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.T' = CitkoGracaninYuksek2020.tok 15 Minimalist.Cat.T [Minimalist.Cat.v]

def CitkoGracaninYuksek2025.v' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.v' = CitkoGracaninYuksek2020.tok 16 Minimalist.Cat.v [Minimalist.Cat.V]

def CitkoGracaninYuksek2025.teach' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.teach' = CitkoGracaninYuksek2020.tok 17 Minimalist.Cat.V [Minimalist.Cat.D] "teach"

def CitkoGracaninYuksek2025.shouldT : Minimalist.LexicalItem.Token

The auxiliary in T.

Equations

• CitkoGracaninYuksek2025.shouldT = CitkoGracaninYuksek2020.tok 18 Minimalist.Cat.T [Minimalist.Cat.v] "should"

def CitkoGracaninYuksek2025.saw : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.saw = CitkoGracaninYuksek2020.tok 20 Minimalist.Cat.V [Minimalist.Cat.D] "saw"

The candidates

def CitkoGracaninYuksek2025.clause (wh c subj T v : Minimalist.LexicalItem.Token) (VP : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

clause builds [CP wh [C′ c [TP subj [T′ T [vP wh [v′ v VP]]]]]], the wh-phrase moved through the edge of vP.

Equations

• CitkoGracaninYuksek2025.clause wh c subj T v VP = ↑wh * (↑c * (↑subj * (↑T * (Minimalist.PlanarSyntacticObject.traceOf wh * (↑v * VP)))))

def CitkoGracaninYuksek2025.nonBulk (c₁ c₂ : Minimalist.LexicalItem.Token) : Minimalist.PlanarSyntacticObject

In non-bulk sharing under the complementizers c₁ and c₂, each wh-phrase stays in its own conjunct and the subject, T, v and verb are shared ((10b), (14), (16b), (38d), (45c), (46b)).

Equations

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

def CitkoGracaninYuksek2025.bulk (c : Minimalist.LexicalItem.Token) : Minimalist.PlanarSyntacticObject

In bulk sharing one C′ sits under both wh-phrases, both of which moved through its vP edge ((12b), (20b)).

Equations

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

def CitkoGracaninYuksek2025.bulkTP (c₁ c₂ : Minimalist.LexicalItem.Token) : Minimalist.PlanarSyntacticObject

Footnote 21's alternative to bulk shares a TP under two complementizers.

Equations

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

def CitkoGracaninYuksek2025.cwhEllipsis : Minimalist.PlanarSyntacticObject

The ellipsis analysis of the coordinated wh-question (11b) builds two clauses from separate tokens and elides the first under its [E] complementizer, with its auxiliary in T as the Sluicing-COMP generalization requires of a sluice.

Equations

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

def CitkoGracaninYuksek2025.csEllipsis : Minimalist.PlanarSyntacticObject

The double-ellipsis analysis of the coordinated sluice (19b), the authors' earlier one, builds two clauses from separate tokens and elides both; the second clause's object is a deleted copy of what, which vehicle change reads as it.

Equations

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

def CitkoGracaninYuksek2025.csnrEllipsis : Minimalist.PlanarSyntacticObject

Its nonpaired counterpart (45b) leaves the second clause's verb without an object.

Equations

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

def CitkoGracaninYuksek2025.multipleQuestion (c : Minimalist.LexicalItem.Token) : Minimalist.PlanarSyntacticObject

In a multiple question both wh-phrases are fronted through the vP edge, as in (28b) and, under an [E] complementizer, the multiple sluice (29b).

Equations

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

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwh : Minimalist.PlanarSyntacticObject

The coordinated wh-question (10b), its complementizer shared.

Equations

• CitkoGracaninYuksek2025.cwh = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.should CitkoGracaninYuksek2025.should

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwhBulk : Minimalist.PlanarSyntacticObject

Its bulk-sharing rival (12b).

Equations

• CitkoGracaninYuksek2025.cwhBulk = CitkoGracaninYuksek2025.bulk CitkoGracaninYuksek2025.should

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwhNullC : Minimalist.PlanarSyntacticObject

Its rival with a null complementizer in the first conjunct (14).

Equations

• CitkoGracaninYuksek2025.cwhNullC = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.c CitkoGracaninYuksek2025.should

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwhNullCSecond : Minimalist.PlanarSyntacticObject

Footnote 15 puts the null complementizer in the second conjunct instead.

Equations

• CitkoGracaninYuksek2025.cwhNullCSecond = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.should CitkoGracaninYuksek2025.c

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwhEmbedded : Minimalist.PlanarSyntacticObject

The embedded coordinated wh-question (15a) with its null complementizer shared, and with two (15b).

Equations

• CitkoGracaninYuksek2025.cwhEmbedded = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.c CitkoGracaninYuksek2025.c

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwhEmbeddedTwoC : Minimalist.PlanarSyntacticObject

Equations

• CitkoGracaninYuksek2025.cwhEmbeddedTwoC = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.c CitkoGracaninYuksek2025.c'

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cwhTwoAux : Minimalist.PlanarSyntacticObject

Two pronounced complementizers (16b).

Equations

• CitkoGracaninYuksek2025.cwhTwoAux = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.should CitkoGracaninYuksek2025.will

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.cs : Minimalist.PlanarSyntacticObject

The coordinated sluice (20b), (26b), (38b).

Equations

• CitkoGracaninYuksek2025.cs = CitkoGracaninYuksek2025.bulk CitkoGracaninYuksek2025.cE

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.csTwoC : Minimalist.PlanarSyntacticObject

Its rival with two [E] complementizers over a shared TP (footnote 21).

Equations

• CitkoGracaninYuksek2025.csTwoC = CitkoGracaninYuksek2025.bulkTP CitkoGracaninYuksek2025.cE CitkoGracaninYuksek2025.cE'

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.csSharedC : Minimalist.PlanarSyntacticObject

The coordinated sluice with the shape of the coordinated wh-question, one shared [E] complementizer over two TPs ((38d), (45c)).

Equations

• CitkoGracaninYuksek2025.csSharedC = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.cE CitkoGracaninYuksek2025.cE

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.csnr : Minimalist.PlanarSyntacticObject

The nonpaired coordinated sluice (46b) has two complementizers, one bearing [E].

Equations

• CitkoGracaninYuksek2025.csnr = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.cE CitkoGracaninYuksek2025.c

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.csnrTwoE : Minimalist.PlanarSyntacticObject

Its rival in which both complementizers bear [E], set aside after (46b).

Equations

• CitkoGracaninYuksek2025.csnrTwoE = CitkoGracaninYuksek2025.nonBulk CitkoGracaninYuksek2025.cE CitkoGracaninYuksek2025.cE'

Cost

inductive CitkoGracaninYuksek2025.CostDimension : Type

A derivation's cost has three dimensions, the lexical items drawn, the Merges, and the applications of ellipsis.

• lexicalItems : CostDimension
• mergeOps : CostDimension
• ellipsisOps : CostDimension

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableEqCostDimension : DecidableEq CostDimension

Equations

• CitkoGracaninYuksek2025.instDecidableEqCostDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CitkoGracaninYuksek2025.instFintypeCostDimension : Fintype CostDimension

Equations

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

theorem CitkoGracaninYuksek2025.CostDimension.forall {p : CostDimension → Prop} : (∀ (i : CostDimension), p i) ↔ p lexicalItems ∧ p mergeOps ∧ p ellipsisOps

@[reducible, inline]

abbrev CitkoGracaninYuksek2025.DerivationCost : Type

The cost of a derivation is a count per dimension, ordered pointwise, so that one derivation is more economical than another when it spends no more on any dimension and less on one.

Equations

• CitkoGracaninYuksek2025.DerivationCost = (CitkoGracaninYuksek2025.CostDimension → ℕ)

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableLEDerivationCost : DecidableLE DerivationCost

Equations

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

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableLTDerivationCost : DecidableLT DerivationCost

Equations

• CitkoGracaninYuksek2025.instDecidableLTDerivationCost = decidableLTOfDecidableLE

def CitkoGracaninYuksek2025.planarCost (t : Minimalist.PlanarSyntacticObject) : DerivationCost

The cost of an object counts its tokens as the lexical items drawn, its internal terms as the Merges, a shared constituent being built once, and its elided domains as the applications of ellipsis. The terms are [MCB25]'s subtrees, each taken once.

Equations

• One or more equations did not get rendered due to their size.
• CitkoGracaninYuksek2025.planarCost t CitkoGracaninYuksek2025.CostDimension.lexicalItems = (CitkoGracaninYuksek2020.tokens t).card
• CitkoGracaninYuksek2025.planarCost t CitkoGracaninYuksek2025.CostDimension.ellipsisOps = (Minimalist.elidedDomains t).length

The multiple-wh-fronting parameter (27)

def CitkoGracaninYuksek2025.projection : RoseTree Minimalist.SyntacticObject.Vertex → Option (List (RoseTree Minimalist.SyntacticObject.Vertex) × Minimalist.LexicalItem.Token)

projection t finds the specifiers and head of the projection at the root of t. Going down the right spine, the specifiers are the left daughters above the head, which is the first selecting item met; the result is none when the spine ends first. This is the drawing convention headIndex? falls back on where the raising head is undefined, as it is wherever a phrase stands in a specifier.

Equations

• One or more equations did not get rendered due to their size.
• CitkoGracaninYuksek2025.projection x✝ = none

def CitkoGracaninYuksek2025.headToken? (s : RoseTree Minimalist.SyntacticObject.Vertex) : Option Minimalist.LexicalItem.Token

The token heading a constituent is its raising head, and for a deleted copy the token whose phrase it copies.

Equations

• CitkoGracaninYuksek2025.headToken? s = match s.value with | Sum.inr (some tok) => some tok | x => Minimalist.treeRaisingHead s

def CitkoGracaninYuksek2025.IsWhSpecifier (s : RoseTree Minimalist.SyntacticObject.Vertex) : Prop

A constituent is a wh-specifier when its head is a wh-token or its trace.

Equations

• CitkoGracaninYuksek2025.IsWhSpecifier s = ∃ tok ∈ (CitkoGracaninYuksek2025.headToken? s).toList, tok.item.wh = true

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableIsWhSpecifier (s : RoseTree Minimalist.SyntacticObject.Vertex) : Decidable (IsWhSpecifier s)

Equations

• CitkoGracaninYuksek2025.instDecidableIsWhSpecifier s = CitkoGracaninYuksek2025.instDecidableIsWhSpecifier._aux_1 s

def CitkoGracaninYuksek2025.asterisked (t : Minimalist.PlanarSyntacticObject) : List Minimalist.LexicalItem.Token

The heads of the projections whose edges host several wh-specifiers, each of which receives an asterisk.

Equations

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

def CitkoGracaninYuksek2025.pfAsterisks (t : Minimalist.PlanarSyntacticObject) : Finset Minimalist.Cat

The categories of the asterisked projections whose heads reach PF unsilenced.

Equations

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

def CitkoGracaninYuksek2025.ConvergesIn (mwf : Finset Minimalist.Cat) (t : Minimalist.PlanarSyntacticObject) : Prop

t converges at PF in a language whose multiple-wh-fronting parameter is mwf, the categories whose asterisks PF cannot interpret, when no asterisk of those categories reaches PF.

Equations

• CitkoGracaninYuksek2025.ConvergesIn mwf t = Disjoint mwf (CitkoGracaninYuksek2025.pfAsterisks t)

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableConvergesIn (mwf : Finset Minimalist.Cat) (t : Minimalist.PlanarSyntacticObject) : Decidable (ConvergesIn mwf t)

Equations

• CitkoGracaninYuksek2025.instDecidableConvergesIn mwf t = { decide := decide (∀ ⦃a : Minimalist.Cat⦄, a ∈ mwf → a ∉ CitkoGracaninYuksek2025.pfAsterisks t), reflects_decide := ⋯ }

theorem CitkoGracaninYuksek2025.convergesIn_of_pfAsterisks_eq_empty {t : Minimalist.PlanarSyntacticObject} (h : pfAsterisks t = ∅) (mwf : Finset Minimalist.Cat) : ConvergesIn mwf t

def CitkoGracaninYuksek2025.englishA : Finset Minimalist.Cat

In English variety A several wh-specifiers are banned at both phase edges.

Equations

• CitkoGracaninYuksek2025.englishA = {Minimalist.Cat.v, Minimalist.Cat.C}

def CitkoGracaninYuksek2025.englishB : Finset Minimalist.Cat

In English variety B they are banned at the vP edge only.

Equations

• CitkoGracaninYuksek2025.englishB = {Minimalist.Cat.v}

def CitkoGracaninYuksek2025.german : Finset Minimalist.Cat

German and Greek lack multiple wh-fronting (30) but have multiple sluicing (31).

Equations

• CitkoGracaninYuksek2025.german = {Minimalist.Cat.v}

def CitkoGracaninYuksek2025.greek : Finset Minimalist.Cat

Equations

• CitkoGracaninYuksek2025.greek = {Minimalist.Cat.v}

def CitkoGracaninYuksek2025.russian : Finset Minimalist.Cat

Russian moves all its wh-phrases, where English moves one (after (29)).

Equations

• CitkoGracaninYuksek2025.russian = ∅

def CitkoGracaninYuksek2025.romanian : Finset Minimalist.Cat

Romanian, where bulk sharing derives coordinated wh-questions (footnote 14).

Equations

• CitkoGracaninYuksek2025.romanian = ∅

Optimality

def CitkoGracaninYuksek2025.Admissible (mwf : Finset Minimalist.Cat) (t : Minimalist.PlanarSyntacticObject) : Prop

A derivation is admissible in a language when none of its ellipses is vacuous, Pronunciation Economy (39), and it converges at PF.

Equations

• CitkoGracaninYuksek2025.Admissible mwf t = (CitkoGracaninYuksek2020.NoVacuousEllipsis t ∧ CitkoGracaninYuksek2025.ConvergesIn mwf t)

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableAdmissible (mwf : Finset Minimalist.Cat) (t : Minimalist.PlanarSyntacticObject) : Decidable (Admissible mwf t)

Equations

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

def CitkoGracaninYuksek2025.Competes (s t : Minimalist.PlanarSyntacticObject) : Prop

s competes with t when it yields the same string with the same reading.

Equations

• CitkoGracaninYuksek2025.Competes s t = (Minimalist.pfPhon s = Minimalist.pfPhon t ∧ (CitkoGracaninYuksek2020.ItReading s ↔ CitkoGracaninYuksek2020.ItReading t))

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableCompetes (s t : Minimalist.PlanarSyntacticObject) : Decidable (Competes s t)

Equations

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

def CitkoGracaninYuksek2025.Optimal (mwf : Finset Minimalist.Cat) (l : List Minimalist.PlanarSyntacticObject) (t : Minimalist.PlanarSyntacticObject) : Prop

Economy makes t optimal among the candidates l in a language when it is admissible and no admissible competitor among them costs less.

Equations

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

theorem CitkoGracaninYuksek2025.optimal_iff {mwf : Finset Minimalist.Cat} {l : List Minimalist.PlanarSyntacticObject} {t : Minimalist.PlanarSyntacticObject} : Optimal mwf l t ↔ (t ∈ l ∧ Admissible mwf t) ∧ ∀ s ∈ l, Competes s t → Admissible mwf s → planarCost s ≤ planarCost t → planarCost t ≤ planarCost s

@[instance_reducible]

instance CitkoGracaninYuksek2025.instDecidableOptimal {mwf : Finset Minimalist.Cat} {l : List Minimalist.PlanarSyntacticObject} {t : Minimalist.PlanarSyntacticObject} : Decidable (Optimal mwf l t)

Equations

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

theorem CitkoGracaninYuksek2025.optimal_congr {mwf mwf' : Finset Minimalist.Cat} {l : List Minimalist.PlanarSyntacticObject} {t : Minimalist.PlanarSyntacticObject} (h : ∀ s ∈ l, pfAsterisks s = ∅) : Optimal mwf l t ↔ Optimal mwf' l t

Among candidates none of whose asterisks reaches PF, optimality is the same in every language.

Coordinated wh-questions (§3.1, §4.1)

def CitkoGracaninYuksek2025.cwhCandidates : List Minimalist.PlanarSyntacticObject

The derivations of What and when should you teach? the paper compares.

Equations

• CitkoGracaninYuksek2025.cwhCandidates = [CitkoGracaninYuksek2025.cwh, CitkoGracaninYuksek2025.cwhEllipsis, CitkoGracaninYuksek2025.cwhBulk, CitkoGracaninYuksek2025.cwhNullC]

theorem CitkoGracaninYuksek2025.cwh_pf : Minimalist.pfPhon cwh = ["what", "when", "should", "you", "teach"]

theorem CitkoGracaninYuksek2025.pfPhon_cwhCandidates (t : Minimalist.PlanarSyntacticObject) : t ∈ cwhCandidates → Minimalist.pfPhon t = Minimalist.pfPhon cwh

theorem CitkoGracaninYuksek2025.cwhNullCSecond_pf : Minimalist.pfPhon cwhNullCSecond = ["what", "should", "when", "you", "teach"]

A pronounced complementizer in the first conjunct only precedes the second wh-phrase (footnote 15).

theorem CitkoGracaninYuksek2025.cwhTwoAux_pf : Minimalist.pfPhon cwhTwoAux = ["what", "should", "when", "will", "you", "teach"]

theorem CitkoGracaninYuksek2025.cwh_nonpaired : Minimalist.orphanTraces cwh = []

Each wh-phrase is interpreted in its own conjunct.

theorem CitkoGracaninYuksek2025.cwhBulk_paired : CitkoGracaninYuksek2020.ItReading cwhBulk

The shared C′ carries a copy of each wh-phrase into the other conjunct.

theorem CitkoGracaninYuksek2025.cwhBulk_lt_cwh : planarCost cwhBulk < planarCost cwh

Bulk sharing is cheaper than non-bulk sharing.

theorem CitkoGracaninYuksek2025.pfAsterisks_cwhBulk : pfAsterisks cwhBulk = {Minimalist.Cat.v}

Of the three phase edges of the bulk-sharing object, the two CP edges host one wh-phrase each and the shared vP edge both, and its asterisk reaches PF ((37b)).

theorem CitkoGracaninYuksek2025.convergesIn_cwhBulk_iff {mwf : Finset Minimalist.Cat} : ConvergesIn mwf cwhBulk ↔ Minimalist.Cat.v ∉ mwf

So bulk sharing crashes wherever the vP edge counts.

theorem CitkoGracaninYuksek2025.pfAsterisks_cwh : pfAsterisks cwh = ∅

Non-bulk sharing leaves one wh-phrase at each edge, so no asterisk arises.

theorem CitkoGracaninYuksek2025.optimal_cwh_iff (t : Minimalist.PlanarSyntacticObject) : t ∈ cwhCandidates → (Optimal englishA cwhCandidates t ↔ t = cwh) ∧ (Optimal englishB cwhCandidates t ↔ t = cwh)

In both English varieties the coordinated wh-question has one optimal derivation, non-bulk sharing: the ellipsis analysis and the extra null complementizer cost more, and bulk sharing, though cheaper, crashes at the vP edge, so the paired reading is unavailable.

theorem CitkoGracaninYuksek2025.optimal_cwhBulk_romanian : Optimal romanian cwhCandidates cwhBulk

In a language with multiple wh-fronting bulk sharing is optimal (footnote 14).

theorem CitkoGracaninYuksek2025.cwhEmbedded_lt_twoC : Minimalist.pfPhon cwhEmbeddedTwoC = Minimalist.pfPhon cwhEmbedded ∧ planarCost cwhEmbedded < planarCost cwhEmbeddedTwoC

With the complementizer null in both conjuncts, it is shared (15).

Coordinated sluices (§3.2, §4.2, §6.1)

def CitkoGracaninYuksek2025.csCandidates : List Minimalist.PlanarSyntacticObject

The derivations of what and when the paper compares, paired and nonpaired.

Equations

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

theorem CitkoGracaninYuksek2025.cs_pf : Minimalist.pfPhon cs = ["what", "when"]

theorem CitkoGracaninYuksek2025.pfPhon_csCandidates (t : Minimalist.PlanarSyntacticObject) : t ∈ csCandidates → Minimalist.pfPhon t = Minimalist.pfPhon cs

theorem CitkoGracaninYuksek2025.paired_csCandidates (t : Minimalist.PlanarSyntacticObject) : t ∈ csCandidates → (CitkoGracaninYuksek2020.ItReading t ↔ t = cs ∨ t = csEllipsis ∨ t = csTwoC)

The paired candidates are bulk sharing, its shared-TP rival and the double ellipsis.

theorem CitkoGracaninYuksek2025.v_mem_asterisked_cs : v ∈ asterisked cs

The shared vP edge hosts two wh-specifiers, the asterisk of (26b).

theorem CitkoGracaninYuksek2025.pfAsterisks_csCandidates (t : Minimalist.PlanarSyntacticObject) : t ∈ csCandidates → pfAsterisks t = ∅

Elided, it never reaches PF, and neither does any other candidate's asterisk.

theorem CitkoGracaninYuksek2025.csSharedC_vacuous : ¬CitkoGracaninYuksek2020.NoVacuousEllipsis csSharedC

With one shared [E] complementizer over two TPs, the second deletion silences nothing new, the authors' earlier argument (CitkoGracaninYuksek2020.csFromCWH_vacuous).

theorem CitkoGracaninYuksek2025.csnrTwoE_excluded : ¬CitkoGracaninYuksek2020.NoVacuousEllipsis csnrTwoE ∧ planarCost csSharedC < planarCost csnrTwoE

Two [E] complementizers are excluded twice over, since they elide the shared material twice and sharing the complementizer would be cheaper.

theorem CitkoGracaninYuksek2025.optimal_cs_iff (mwf : Finset Minimalist.Cat) (t : Minimalist.PlanarSyntacticObject) : t ∈ csCandidates → (Optimal mwf csCandidates t ↔ t = cs ∨ t = csnr)

In every language the coordinated sluice has two optimal derivations. For the paired reading, the elided shared C′ is cheaper than eliding two clauses or sharing TP under two complementizers. For the nonpaired reading, two complementizers of which only one bears [E] are cheaper than eliding two clauses, while a shared [E] complementizer, which draws one token fewer, elides vacuously, as does a second [E].

theorem CitkoGracaninYuksek2025.csEllipsis_admissible_not_optimal (mwf : Finset Minimalist.Cat) : Admissible mwf csEllipsis ∧ ¬Optimal mwf csCandidates csEllipsis

The authors' earlier double ellipsis is admissible in every language but not optimal, since bulk sharing yields the same string with the same reading more cheaply.

theorem CitkoGracaninYuksek2025.csnr_silences_shared : (∃ p ∈ Minimalist.occurrences csnr teach, ∀ K ∈ Minimalist.elidedDomains csnr, ¬K ≤ p) ∧ Minimalist.IsSilenced csnr teach

The shared verb occurs in the second conjunct outside the elided TP and is silenced all the same, so the nonpaired sluice cannot surface as a coordinated wh-question (footnote 30).

Multiple questions and multiple sluices (§3.2.2)

theorem CitkoGracaninYuksek2025.pfAsterisks_multipleQuestion : pfAsterisks (multipleQuestion c) = {Minimalist.Cat.v, Minimalist.Cat.C}

Both phase edges of a multiple question reach PF with two wh-specifiers ((28b)).

theorem CitkoGracaninYuksek2025.pfAsterisks_multipleSluice : pfAsterisks (multipleQuestion cE) = {Minimalist.Cat.C}

Multiple sluicing elides the vP edge but not the CP edge ((29b)).

theorem CitkoGracaninYuksek2025.convergesIn_multipleQuestion_iff {mwf : Finset Minimalist.Cat} : ConvergesIn mwf (multipleQuestion c) ↔ Minimalist.Cat.v ∉ mwf ∧ Minimalist.Cat.C ∉ mwf

A multiple question converges only where neither edge counts.

theorem CitkoGracaninYuksek2025.convergesIn_multipleSluice_iff {mwf : Finset Minimalist.Cat} : ConvergesIn mwf (multipleQuestion cE) ↔ Minimalist.Cat.C ∉ mwf

Multiple sluicing converges exactly where the CP edge does not count.

theorem CitkoGracaninYuksek2025.multipleQuestion_multipleSluice : ¬ConvergesIn englishA (multipleQuestion c) ∧ ¬ConvergesIn englishB (multipleQuestion c) ∧ ConvergesIn russian (multipleQuestion c) ∧ ¬ConvergesIn englishA (multipleQuestion cE) ∧ ConvergesIn englishB (multipleQuestion cE) ∧ ConvergesIn german (multipleQuestion cE) ∧ ConvergesIn greek (multipleQuestion cE)

So a multiple question crashes in both English varieties and converges in Russian, and multiple sluicing converges in variety B, German and Greek but not in variety A.

Right node raising (§6.2)

def CitkoGracaninYuksek2025.rnrCost (d : BelkNeelemanPhilip2023.Derivation) : DerivationCost

The cost of a derivation of right node raising counts the lexical items and Merges of its structure, and each free pruning as an application of ellipsis.

Equations

• CitkoGracaninYuksek2025.rnrCost d CitkoGracaninYuksek2025.CostDimension.lexicalItems = CitkoGracaninYuksek2025.planarCost d.input CitkoGracaninYuksek2025.CostDimension.lexicalItems
• CitkoGracaninYuksek2025.rnrCost d CitkoGracaninYuksek2025.CostDimension.mergeOps = CitkoGracaninYuksek2025.planarCost d.input CitkoGracaninYuksek2025.CostDimension.mergeOps
• CitkoGracaninYuksek2025.rnrCost d CitkoGracaninYuksek2025.CostDimension.ellipsisOps = d.free.length

def CitkoGracaninYuksek2025.alice : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.alice = CitkoGracaninYuksek2020.tok 21 Minimalist.Cat.D [] "Alice"

def CitkoGracaninYuksek2025.iris : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.iris = CitkoGracaninYuksek2020.tok 22 Minimalist.Cat.D [] "Iris"

def CitkoGracaninYuksek2025.must : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.must = CitkoGracaninYuksek2020.tok 23 Minimalist.Cat.T [Minimalist.Cat.V] "must"

def CitkoGracaninYuksek2025.oughtToBe : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.oughtToBe = CitkoGracaninYuksek2020.tok 25 Minimalist.Cat.T [Minimalist.Cat.V] "ought to be"

def CitkoGracaninYuksek2025.shouldRNR : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.shouldRNR = CitkoGracaninYuksek2020.tok 26 Minimalist.Cat.T [Minimalist.Cat.V] "should"

def CitkoGracaninYuksek2025.work : Minimalist.LexicalItem.Token

Work, a second work, and working.

Equations

• CitkoGracaninYuksek2025.work = CitkoGracaninYuksek2020.tok 27 Minimalist.Cat.V [Minimalist.Cat.P] "work"

def CitkoGracaninYuksek2025.work' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.work' = CitkoGracaninYuksek2020.tok 35 Minimalist.Cat.V [Minimalist.Cat.P] "work"

def CitkoGracaninYuksek2025.working : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.working = CitkoGracaninYuksek2020.tok 28 Minimalist.Cat.V [Minimalist.Cat.P] "working"

def CitkoGracaninYuksek2025.on : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.on = CitkoGracaninYuksek2020.tok 29 Minimalist.Cat.P [Minimalist.Cat.N] "on"

def CitkoGracaninYuksek2025.different : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.different = CitkoGracaninYuksek2020.tok 30 Minimalist.Cat.A [] "different"

def CitkoGracaninYuksek2025.topics : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.topics = CitkoGracaninYuksek2020.tok 31 Minimalist.Cat.N [] "topics"

def CitkoGracaninYuksek2025.on' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.on' = CitkoGracaninYuksek2020.tok 32 Minimalist.Cat.P [Minimalist.Cat.N] "on"

def CitkoGracaninYuksek2025.different' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.different' = CitkoGracaninYuksek2020.tok 33 Minimalist.Cat.A [] "different"

def CitkoGracaninYuksek2025.topics' : Minimalist.LexicalItem.Token

Equations

• CitkoGracaninYuksek2025.topics' = CitkoGracaninYuksek2020.tok 34 Minimalist.Cat.N [] "topics"

def CitkoGracaninYuksek2025.pivot : Minimalist.PlanarSyntacticObject

The pivot, on different topics.

Equations

• CitkoGracaninYuksek2025.pivot = ↑CitkoGracaninYuksek2025.on * (↑CitkoGracaninYuksek2025.different * ↑CitkoGracaninYuksek2025.topics)

def CitkoGracaninYuksek2025.tp (subj T : Minimalist.LexicalItem.Token) (VP : Minimalist.PlanarSyntacticObject) : Minimalist.PlanarSyntacticObject

[TP subj [T′ T VP]].

Equations

• CitkoGracaninYuksek2025.tp subj T VP = ↑subj * (↑T * VP)

def CitkoGracaninYuksek2025.rnrMixed : BelkNeelemanPhilip2023.Derivation

In example (53b), Belk, Neeleman and Philip's analysis of Larson's mixed pivot, the pivot is multidominated and its first branch pruned, and then the first verb phrase, by then the bare verb, is pruned freely.

Equations

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

def CitkoGracaninYuksek2025.rnrElided : BelkNeelemanPhilip2023.Derivation

Example (54) builds the first verb phrase with its own pivot and elides it.

Equations

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

def CitkoGracaninYuksek2025.rnrShared : BelkNeelemanPhilip2023.Derivation

Example (55b) multidominates the verb phrase, the verbs matching.

Equations

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

def CitkoGracaninYuksek2025.rnrMatchedMixed : BelkNeelemanPhilip2023.Derivation

The rival of (55b) with the shape of (53b), each conjunct with its own work.

Equations

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

theorem CitkoGracaninYuksek2025.rnrMixed_phon : rnrMixed.phon = ["Alice", "must", "Iris", "ought to be", "working", "on", "different", "topics"]

theorem CitkoGracaninYuksek2025.rnrMixed_lt_elided : rnrMixed.Licensed ∧ rnrElided.Licensed ∧ rnrElided.phon = rnrMixed.phon ∧ rnrCost rnrMixed < rnrCost rnrElided

With mismatched verbs, multidominating the pivot beats building it twice.

theorem CitkoGracaninYuksek2025.rnrShared_phon : rnrShared.phon = ["Alice", "must", "Iris", "should", "work", "on", "different", "topics"]

theorem CitkoGracaninYuksek2025.rnrShared_lt_mixed : rnrShared.Licensed ∧ rnrMatchedMixed.Licensed ∧ rnrMatchedMixed.phon = rnrShared.phon ∧ rnrCost rnrShared < rnrCost rnrMatchedMixed

With matching verbs, ellipsis is no longer an option.

theorem CitkoGracaninYuksek2025.rnr56_economy : (∀ d ∈ BelkNeelemanPhilip2023.derivations51, d.Licensed) ∧ BelkNeelemanPhilip2023.shareAuxP.pivotOnset = some "have" ∧ rnrCost BelkNeelemanPhilip2023.shareAuxP < rnrCost BelkNeelemanPhilip2023.shareVP ∧ rnrCost BelkNeelemanPhilip2023.shareAuxP < rnrCost BelkNeelemanPhilip2023.sharePP

Belk, Neeleman and Philip license three derivations of (56), their (51), with the prosodic break before have, traveled or to. Multidominating the whole auxiliary phrase is cheaper than either derivation that elides, so economy blocks those (the paper's (57) and (58)) and leaves the break before have (59).