Economy in PF Reduction

@cite{citko-gracanin-yuksek-2025}

Coordinated wh-questions (CWHs) and coordinated sluices (CSs) are two PF-reduced constructions with wh-phrase remnants. Despite superficial similarity, they differ in structure, derivational cost, and empirical properties. Economy governs the choice between ellipsis and multidominance as the PF reduction mechanism.

Key Claims

1. CWHs use non-bulk-sharing MD: each conjunct CP contains one wh-phrase; functional heads (C, T) are multiply dominated. No ellipsis is involved.

2. CSs use bulk-sharing MD + ellipsis: the entire C' is shared between conjuncts; both wh-phrases originate inside the shared vP. The E-feature on C triggers TP deletion (cf. FeatureVal.ellipsis in Core/Features.lean, which models this E-feature).

3. Economy selects the structure: MD is preferred over ellipsis (fewer operations, fewer lexical items). Bulk-sharing MD is more economical than non-bulk-sharing, but is blocked for CWHs by the MWF parameter. CSs can't have the CWH structure because of Pronunciation Economy.

Empirical Contrasts

• CWHs ban coordination of obligatory wh-arguments; CSs allow it.
• CWHs ban wh-object + wh-adjunct with obligatorily transitive verbs; CSs allow it.
• CWHs only allow nonpaired readings; CSs allow paired readings (with obligatorily transitive verbs) and nonpaired readings (with optionally transitive verbs).

Integration

• CSs are coordinated sluices — each conjunct of a CS is a sluice. Bridge theorems connect CS data to Sluicing.lean data structures.
• The MWF parameter connects to Questions/MultipleWh.lean: non-MWF languages (English) ban multiple wh-fronting in questions.
• RNR (§6.2) demonstrates that economy can force BOTH ellipsis and MD in a single derivation.

inductive Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.WHCoordType : Type

The two PF-reduced wh-coordination constructions.

• CWH : WHCoordType

  Coordinated wh-question: "What and when did John teach?"

• CS : WHCoordType

  Coordinated sluice: "I forgot what and when."

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordType.repr : WHCoordType → ℕ → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordType : Repr WHCoordType

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordType = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordType.repr }

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instDecidableEqWHCoordType : DecidableEq WHCoordType

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instDecidableEqWHCoordType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.WHCoordDatum : Type

An empirical datum contrasting CWHs and CSs.

• sentence : String
• construction : WHCoordType
• whPhrases : List String
• grammatical : Bool
• notes : String

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordDatum : Repr WHCoordDatum

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordDatum = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordDatum.repr }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprWHCoordDatum.repr : WHCoordDatum → ℕ → Std.Format

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_basic : WHCoordDatum

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_obligatory_args_banned : WHCoordDatum

CWHs ban coordination of obligatory wh-arguments (ex 5a).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_obj_adjunct_banned : WHCoordDatum

CWHs ban wh-object + wh-adjunct with obligatorily transitive verbs (ex 6a). Distinct from (5a): here only one wh-phrase is an obligatory argument; the other is an adjunct. The ban persists because the verb ('buy') is obligatorily transitive.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_basic : WHCoordDatum

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_obligatory_args_allowed : WHCoordDatum

CSs allow coordination of obligatory wh-arguments (ex 5b).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_obj_adjunct_allowed : WHCoordDatum

CSs allow wh-object + wh-adjunct coordination (ex 6b).

Equations

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

inductive Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.ReadingType : Type

Reading type for wh-coordination.

• nonpaired : ReadingType

  Each wh-phrase interpreted in its own conjunct only.

• paired : ReadingType

  The trace of the first wh-phrase is interpreted as an E-type pronoun in the second conjunct (pairing).

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingType : Repr ReadingType

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingType = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingType.repr }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingType.repr : ReadingType → ℕ → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instDecidableEqReadingType : DecidableEq ReadingType

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instDecidableEqReadingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.ReadingDatum : Type

Reading availability datum.

• sentence : String
• construction : WHCoordType
• reading : ReadingType
• available : Bool
• paraphrase : String

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingDatum.repr : ReadingDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingDatum : Repr ReadingDatum

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingDatum = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprReadingDatum.repr }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_nonpaired : ReadingDatum

CWHs: only nonpaired reading available (ex 8a).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_no_paired : ReadingDatum

CWHs: paired reading unavailable (ex 8a).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_paired : ReadingDatum

CSs: paired reading available with obligatorily transitive verbs (ex 8b). The paired reading arises because in the bulk-sharing structure, both wh-phrases originate inside the shared vP — the lower copy of the first wh-phrase is interpreted as an E-type pronoun in the second conjunct.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_nonpaired : ReadingDatum

CSs: nonpaired reading available with optionally transitive verbs (§6.1, ex 43). With verbs like 'teach' (optionally transitive), each wh-phrase can start in its own clause, yielding a nonpaired reading. This requires a different structure: non-bulk-sharing with two independent Cs, only one bearing the E-feature.

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_bans_obligatory_args : cwh_obligatory_args_banned.grammatical = false

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_allows_obligatory_args : cs_obligatory_args_allowed.grammatical = true

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_bans_obj_adjunct : cwh_obj_adjunct_banned.grammatical = false

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_allows_obj_adjunct : cs_obj_adjunct_allowed.grammatical = true

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_bans_paired_reading : cwh_no_paired.available = false

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_allows_paired_reading : cs_paired.available = true

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_allows_nonpaired_reading : cs_nonpaired.available = true

Each conjunct of a CS is itself a sluice: the wh-phrase is the remnant and the TP is the elided material. We show this by decomposing CS examples into SluicingDatum instances from Phenomena.Ellipsis.Sluicing.

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_basic_sluice_what : Sluicing.SluicingDatum

The "what" conjunct of cs_basic as a standalone sluice: "John taught something, but I forgot what [John taught _]"

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_basic_sluice_when : Sluicing.SluicingDatum

The "when" conjunct of cs_basic as a standalone sluice: "John taught something, but I forgot when [John taught something]"

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_basic_decomposes_into_sluices : cs_basic.whPhrases = [cs_basic_sluice_what.whPhrase, cs_basic_sluice_when.whPhrase]

Each CS decomposes into sluices: the wh-phrases in a CS are exactly the remnants of the component sluices.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_components_grammatical : cs_basic_sluice_what.grammatical = true ∧ cs_basic_sluice_when.grammatical = true

Both component sluices are grammatical.

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_oblig_sluice_what : Sluicing.SluicingDatum

The "what" and "to whom" conjuncts of cs_obligatory_args_allowed.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_oblig_sluice_toWhom : Sluicing.SluicingDatum

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_obligatory_decomposes : cs_obligatory_args_allowed.whPhrases = [cs_oblig_sluice_what.whPhrase, cs_oblig_sluice_toWhom.whPhrase]

Obligatory-argument CS also decomposes into sluices.

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.english : Minimalism.MWFParameter

English is a non-MWF language: multiple wh-fronting is banned. *"Who what saw?" is ungrammatical (ex 28).

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.english = { allowsMWF := false }

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.english_bans_multiple_wh : Minimalism.mwfViolation english 2 = true

English bans multiple wh-specifiers at a phase edge.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.english_allows_single_wh : Minimalism.mwfViolation english 1 = false

A single wh-specifier is fine in English.

The MWF parameter varies cross-linguistically. We define language classifications that connect to the multiple wh-question data in Phenomena/Questions/MultipleWh.lean.

structure Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.MWFLanguageDatum : Type

MWF language classification.

• language : String
• mwfParam : Minimalism.MWFParameter
• example_ : String

  Example multiple wh-question

• grammatical : Bool

  Is the example grammatical?

• allowsMultipleSluicing : Bool

  Does this language allow multiple sluicing?

• notes : String

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprMWFLanguageDatum.repr : MWFLanguageDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprMWFLanguageDatum : Repr MWFLanguageDatum

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprMWFLanguageDatum = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprMWFLanguageDatum.repr }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.bulgarian : MWFLanguageDatum

Bulgarian: MWF language.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.german_mwf : MWFLanguageDatum

German: non-MWF language, but allows multiple sluicing.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.greek_mwf : MWFLanguageDatum

Greek: non-MWF language, but allows multiple sluicing.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.english_varietyA : MWFLanguageDatum

English variety A: non-MWF, bans multiple sluicing.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.english_varietyB : MWFLanguageDatum

English variety B: non-MWF, allows multiple sluicing.

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.mwf_language_questions_ok : Minimalism.mwfViolation bulgarian.mwfParam 2 = false

MWF languages never have MWF violations in questions.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.non_mwf_language_questions_bad : Minimalism.mwfViolation german_mwf.mwfParam 2 = true

Non-MWF languages DO have violations with 2+ wh-specifiers.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.german_greek_sluicing_repair : german_mwf.allowsMultipleSluicing = true ∧ greek_mwf.allowsMultipleSluicing = true ∧ Minimalism.ellipsisRepairsMWF german_mwf.mwfParam 2 true = true

German and Greek: non-MWF but allow multiple sluicing — the offending vP edge is deleted by ellipsis (same mechanism as CSs).

The derivation cost of a PF-reduced coordination depends on whether the shared material is built once (MD) or twice (ellipsis). We provide two levels of parameterization:

Coarse (MD vs ellipsis): parameterized by total shared/non-shared cost. Used for Theorems 1–2.

• sm/sl: Merge/lexical cost of shared material (built once with MD, twice with ellipsis)
• nsm/nsl: cost of non-shared parts (wh-movement, coordination)

Fine (non-bulk vs bulk sharing): decomposes shared material into heads vs phrasal structure. Used for Theorem 3.

• hm/hl: cost of shared heads (C, T — built once either way)
• pm/pl: cost of per-conjunct phrasal structure (C', TP, vP assembly)
• wm/wl: cost of wh-phrases + coordination (non-shared)

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhMDCost (sm sl nsm nsl : ℕ) : Minimalism.DerivationCost

Cost of CWH via non-bulk-sharing MD (adopted structure, paper's (10b)). Shared material built once; no ellipsis.

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhMDCost sm sl nsm nsl = { lexicalItems := sl + nsl, mergeOps := sm + nsm, agreeOps := 0, ellipsisOps := 0 }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhEllipsisCost (sm sl nsm nsl : ℕ) : Minimalism.DerivationCost

Cost of CWH via ellipsis (biclausal alternative, paper's (11b)). Shared material duplicated; one E-feature deletion.

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhEllipsisCost sm sl nsm nsl = { lexicalItems := 2 * sl + nsl, mergeOps := 2 * sm + nsm, agreeOps := 0, ellipsisOps := 1 }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhNonBulkCost (hm hl pm pl wm wl : ℕ) : Minimalism.DerivationCost

Cost of CWH via non-bulk-sharing MD — fine-grained (paper's (10b)). Individual heads (C, T) shared; per-conjunct phrasal structure (assembling C', TP, vP around shared heads) built in each conjunct.

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhNonBulkCost hm hl pm pl wm wl = { lexicalItems := hl + 2 * pl + wl, mergeOps := hm + 2 * pm + wm, agreeOps := 0, ellipsisOps := 0 }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhBulkMDCost (hm hl pm pl wm wl : ℕ) : Minimalism.DerivationCost

Cost of CWH via bulk-sharing MD (excluded, paper's (12b)). Entire C' shared — phrasal structure built only once. More economical than non-bulk-sharing, but blocked by MWF.

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhBulkMDCost hm hl pm pl wm wl = { lexicalItems := hl + pl + wl, mergeOps := hm + pm + wm, agreeOps := 0, ellipsisOps := 0 }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.csBulkCost (sm sl nsm nsl : ℕ) : Minimalism.DerivationCost

Cost of CS via bulk-sharing MD + single ellipsis (adopted, paper's (20b)). C' shared; E-feature on C deletes TP once.

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.csBulkCost sm sl nsm nsl = { lexicalItems := sl + nsl, mergeOps := sm + nsm, agreeOps := 0, ellipsisOps := 1 }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.csDoubleEllipsisCost (sm sl nsm nsl : ℕ) : Minimalism.DerivationCost

Cost of CS via double ellipsis, no MD (excluded, paper's (19b)). Both conjuncts built in full; E-feature in each.

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.csDoubleEllipsisCost sm sl nsm nsl = { lexicalItems := 2 * sl + nsl, mergeOps := 2 * sm + nsm, agreeOps := 0, ellipsisOps := 2 }

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_md_beats_ellipsis (sm sl nsm nsl : ℕ) : Minimalism.strictlyMoreEconomical (cwhMDCost sm sl nsm nsl) (cwhEllipsisCost sm sl nsm nsl)

Theorem 1: For CWHs, the MD derivation is strictly more economical than the ellipsis alternative (paper's (10b) vs (11b)).

The MD derivation saves sm Merge operations (shared material built once instead of twice) and avoids the ellipsis operation entirely. This holds for ANY amount of shared material — even if sm = 0, the ellipsis operation alone makes the alternative costlier.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_bulk_beats_double_ellipsis (sm sl nsm nsl : ℕ) : Minimalism.strictlyMoreEconomical (csBulkCost sm sl nsm nsl) (csDoubleEllipsisCost sm sl nsm nsl)

Theorem 2: For CSs, the bulk-sharing derivation is strictly more economical than the double-ellipsis alternative (paper's (20b) vs (19b)).

The bulk-sharing derivation saves sm Merge operations and sl lexical items, and uses one fewer ellipsis operation.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_bulk_beats_nonbulk (hm hl pm pl wm wl : ℕ) (h : 0 < pm ∨ 0 < pl) : Minimalism.strictlyMoreEconomical (cwhBulkMDCost hm hl pm pl wm wl) (cwhNonBulkCost hm hl pm pl wm wl)

Theorem 3: Bulk-sharing is strictly more economical than non-bulk-sharing for CWHs (paper's (12b) vs (10b)).

This is the paper's crucial insight: the MOST economical derivation for CWHs (bulk-sharing, which builds C' once) is blocked by an independent constraint (MWF), forcing the LESS economical non-bulk-sharing structure. The precondition 0 < pm ∨ 0 < pl ensures there is at least some phrasal structure to share — which holds for any non-trivial clause.

The CS (bulk-sharing) structure places both wh-phrases inside a single vP. Both must pass through the vP phase edge, creating a phase node with multiple wh-specifiers (paper's (36b)/(37b)).

In a non-MWF language like English, this configuration receives an asterisk at PF, crashing the derivation.

Unlike CSs, CWHs do NOT involve ellipsis — the vP edge survives to PF, so the asterisk is not deleted and the crash is unavoidable.

CSs survive because the E-feature on C triggers TP deletion (including the offending vP edge), removing the asterisk before PF interprets it.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_bulk_crashes_in_english : Minimalism.mwfViolation english 2 = true

The bulk-sharing structure for CWHs crashes in English: 2 wh-specifiers at vP edge in a non-MWF language.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_no_ellipsis_repair : Minimalism.ellipsisRepairsMWF english 2 false = false

CWHs have no ellipsis to repair the MWF violation — the vP edge survives to PF, and the asterisk crashes.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_ellipsis_repairs_mwf : Minimalism.ellipsisRepairsMWF english 2 true = true

CSs survive the same MWF configuration because ellipsis deletes the vP edge containing the multiple wh-specifiers.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_nonbulk_violates_pronunciation_economy : have pfAfterFirstDeletion := ["what", "and", "when"]; have pfAfterBothDeletions := ["what", "and", "when"]; Minimalism.vacuousEllipsis pfAfterFirstDeletion pfAfterBothDeletions

If CSs had the non-bulk-sharing (CWH) structure (paper's (38d)), with a shared C bearing the E-feature, the C would have two TP complements (one per conjunct). The E-feature triggers deletion of both TPs:

1. Deleting TP₁ removes the TP-internal string from PF.
2. Deleting TP₂ would remove the same string — but it was already removed by step 1.
3. The second deletion is vacuous → violates Pronunciation Economy.

This reasoning crucially relies on C being shared (economy forces sharing unless independent Cs are needed, as in (16) where each C hosts different phonological material).

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_nonbulk_fails_pronEcon : have pfAfterFirstDeletion := ["what", "and", "when"]; have pfAfterBothDeletions := ["what", "and", "when"]; ¬Minimalism.pronunciationEconomy pfAfterFirstDeletion pfAfterBothDeletions

The Pronunciation Economy principle is violated: the second ellipsis does not change the PF output.

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwhStructure : Minimalism.PFReducedCoordination

The adopted CWH structure: non-bulk-sharing MD, no ellipsis (paper's (10b)). Shared nodes: C and T are individually multiply dominated.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.csStructure : Minimalism.PFReducedCoordination

The adopted CS structure: bulk-sharing MD + ellipsis (paper's (20b)). The E-feature on C (cf. FeatureVal.ellipsis in Core/Features.lean) triggers TP deletion, repairing the MWF violation at the vP edge. Shared nodes: entire C' is shared (includes C, TP, vP, VP).

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_uses_md_only : cwhStructure.usesMD = true ∧ cwhStructure.usesEllipsis = false

CWHs use only MD.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_uses_both : csStructure.usesBoth = true

CSs use both MD and ellipsis.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_shares_heads_cs_shares_constituent : cwhStructure.sharedNodes.length = 2 ∧ csStructure.sharedNodes.length = 3

CWHs share individual heads (C, T); CSs share an entire constituent.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_shared_categories : (cwhStructure.sharedNodes.all fun (x : Minimalism.SharedNode) => x.category.isSome) = true

All CWH shared nodes have explicit categories.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_shared_categories : (csStructure.sharedNodes.all fun (x : Minimalism.SharedNode) => x.category.isSome) = true

All CS shared nodes have explicit categories.

The paper's central contribution is explaining WHY CWHs and CSs must have different structures — and therefore different empirical properties — despite their superficial similarity.

For CWHs (§4.1):

1. Bulk-sharing MD is most economical (cwh_bulk_beats_nonbulk)
2. But bulk-sharing creates MWF violation at vP (cwh_bulk_crashes_in_english)
3. CWHs have no ellipsis to repair MWF (cwh_no_ellipsis_repair)
4. So non-bulk-sharing MD is selected (cwh_md_beats_ellipsis over ellipsis)

For CSs (§4.2):

1. Bulk-sharing MD + ellipsis is most economical (cs_bulk_beats_double_ellipsis)
2. Bulk-sharing creates MWF at vP, but ellipsis repairs it (cs_ellipsis_repairs_mwf)
3. Non-bulk-sharing (CWH structure) violates Pronunciation Economy (cs_nonbulk_fails_pronEcon)
4. So bulk-sharing MD + ellipsis is selected

Different structures → different properties:

• Non-bulk-sharing (CWH): each conjunct has one wh-phrase → bans obligatory arg coordination, bans obj+adjunct coordination with obligatorily transitive verbs, only nonpaired readings
• Bulk-sharing (CS): both wh-phrases in shared vP → allows all of the above

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.different_mechanisms : cwhStructure.mechanisms ≠ csStructure.mechanisms

The two constructions use different PF reduction mechanisms, explaining why they have different empirical properties.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.different_sharing : cwhStructure.sharing ≠ csStructure.sharing

The two constructions use different sharing types.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cwh_forced_to_nonbulk (hm hl pm pl wm wl : ℕ) (h : 0 < pm ∨ 0 < pl) : Minimalism.strictlyMoreEconomical (cwhBulkMDCost hm hl pm pl wm wl) (cwhNonBulkCost hm hl pm pl wm wl) ∧ Minimalism.mwfViolation english 2 = true ∧ Minimalism.ellipsisRepairsMWF english 2 false = false

End-to-end: CWHs cannot use bulk-sharing (most economical) because the MWF violation at vP cannot be repaired without ellipsis. Combines Theorems 3, cwh_bulk_crashes_in_english, and cwh_no_ellipsis_repair.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.cs_forced_to_bulk (sm sl nsm nsl : ℕ) : Minimalism.strictlyMoreEconomical (csBulkCost sm sl nsm nsl) (csDoubleEllipsisCost sm sl nsm nsl) ∧ Minimalism.ellipsisRepairsMWF english 2 true = true ∧ ¬Minimalism.pronunciationEconomy ["what", "and", "when"] ["what", "and", "when"]

End-to-end: CSs use bulk-sharing because it is most economical AND the MWF violation is repaired by ellipsis; the CWH structure is excluded by Pronunciation Economy.

Section 6.2 of the paper extends the economy analysis to Right Node Raising (RNR). RNR is a key test case because it can involve BOTH ellipsis and MD simultaneously — the "mix and match" analysis of @cite{belk-neeleman-philip-2023}.

The core claim: economy favors MD over ellipsis when both yield the same string and interpretation. In RNR, the shared pivot (rightmost material) is multiply dominated. When the pivot and antecedent are not morphologically identical (vehicle change), ellipsis is additionally required for the non-shared material in the first conjunct.

Examples:

• Pure MD: "Alice must, and Iris should, work on different topics" (ex 55) → No morphological mismatch, so MD alone suffices.
• Ellipsis + MD: "Alice must ⟨work on different topics⟩, and Iris ought to be, working on different topics" (ex 52/53) → Morphological mismatch forces ellipsis for verb form; MD for PP pivot.

The analysis predicts prosodic break placement: the break should occur at the onset of the MD-shared material.

inductive Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.RNRPivotType : Type

RNR pivot type: what is shared at the right edge.

• minimal : RNRPivotType

  Only the rightmost constituent (e.g., PP) is shared.

• extended : RNRPivotType

  A larger constituent (e.g., VP) is shared.

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRPivotType : Repr RNRPivotType

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRPivotType = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRPivotType.repr }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRPivotType.repr : RNRPivotType → ℕ → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instDecidableEqRNRPivotType : DecidableEq RNRPivotType

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instDecidableEqRNRPivotType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.RNRDatum : Type

An RNR datum captures the structural analysis.

• sentence : String
• pivot : String

  The shared pivot string

• morphologicalIdentity : Bool

  Does the pivot exhibit morphological identity with the antecedent?

• mdProperties : Bool

  Does the pivot exhibit properties of MD? (e.g., cumulative agreement, internal reading of relational adjective)

• involvesEllipsis : Bool

  Does the construction involve ellipsis in addition to MD?

• pivotType : RNRPivotType
• notes : String

instance Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRDatum : Repr RNRDatum

Equations

• Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRDatum = { reprPrec := Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRDatum.repr }

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.instReprRNRDatum.repr : RNRDatum → ℕ → Std.Format

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_pureMD : RNRDatum

Pure MD: identical verbs, no mismatch → economy selects MD only (ex 55).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_ellipsisPlusMD : RNRDatum

Ellipsis + MD: verb morphology mismatch forces ellipsis for VP, but PP pivot is still shared via MD (ex 52/53).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_ellipsisOnly : RNRDatum

Morphological mismatch signals ellipsis, not MD.

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_internalReading : RNRDatum

Relational adjective with internal reading signals MD.

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_economy_prefers_md : rnr_pureMD.involvesEllipsis = false ∧ rnr_pureMD.morphologicalIdentity = true ∧ rnr_pureMD.mdProperties = true

Economy prediction for RNR: when morphology matches and no independent constraint forces ellipsis, pure MD is selected.

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_mismatch_forces_ellipsis : rnr_ellipsisPlusMD.morphologicalIdentity = false ∧ rnr_ellipsisPlusMD.involvesEllipsis = true ∧ rnr_ellipsisPlusMD.mdProperties = true

When morphology mismatches, ellipsis is ADDITIONALLY needed.

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnrMDPivotCost (pivotMerge pivotLex nonsharedMerge nonsharedLex : ℕ) : Minimalism.DerivationCost

RNR pivot cost: MD derivation for the shared pivot. The pivot is built once (MD) rather than twice (ellipsis).

Equations

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

def Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnrEllipsisCost (pivotMerge pivotLex nonsharedMerge nonsharedLex : ℕ) : Minimalism.DerivationCost

RNR cost with full ellipsis (no MD): pivot duplicated.

Equations

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

theorem Phenomena.Ellipsis.Studies.CitkoGracaninYuksek2025.rnr_md_beats_ellipsis (pm pl nm nl : ℕ) : Minimalism.strictlyMoreEconomical (rnrMDPivotCost pm pl nm nl) (rnrEllipsisCost pm pl nm nl)

Theorem 4: For RNR, MD is strictly more economical than ellipsis when both yield the same string. Same reasoning as Theorem 1 (CWHs).