structure Phenomena.Questions.MultipleWh.MultipleWhDatum : Type

A multiple wh-question with its answer patterns

• question : String

  The question

• numWh : ℕ

  Number of wh-phrases

• constituentAnswer : String

  Example constituent answer (short form)

• sententialAnswer : String

  Example sentential answer (long form)

• exhaustiveReading : String

  The exhaustive interpretation

• source : String

  Source

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instReprMultipleWhDatum : Repr MultipleWhDatum

Equations

• Phenomena.Questions.MultipleWh.instReprMultipleWhDatum = { reprPrec := Phenomena.Questions.MultipleWh.instReprMultipleWhDatum.repr }

def Phenomena.Questions.MultipleWh.instReprMultipleWhDatum.repr : MultipleWhDatum → ℕ → Std.Format

Equations

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

def Phenomena.Questions.MultipleWh.whichManWoman : MultipleWhDatum

G&S p. 310: "Which man loves which woman?"

Equations

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

def Phenomena.Questions.MultipleWh.whichManWoman_conj : MultipleWhDatum

Conjunctive answer: multiple pairs

Equations

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

def Phenomena.Questions.MultipleWh.whichManWoman_disj : MultipleWhDatum

Disjunctive answer: uncertain which pair

Equations

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

def Phenomena.Questions.MultipleWh.whichManWoman_quant : MultipleWhDatum

Complex answer with quantifiers

Equations

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

def Phenomena.Questions.MultipleWh.multipleWhExamples : List MultipleWhDatum

Equations

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

structure Phenomena.Questions.MultipleWh.AnswerEquivalence : Type

Constituent and sentential answers express the same proposition. @cite{groenendijk-stokhof-1984}: Both derived from the same abstract + term.

• question : String

  The question

• shortAnswer : String

  Short (constituent) answer

• longAnswer : String

  Long (sentential) answer

• equivalent : Bool

  They express the same proposition

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instReprAnswerEquivalence : Repr AnswerEquivalence

Equations

• Phenomena.Questions.MultipleWh.instReprAnswerEquivalence = { reprPrec := Phenomena.Questions.MultipleWh.instReprAnswerEquivalence.repr }

def Phenomena.Questions.MultipleWh.instReprAnswerEquivalence.repr : AnswerEquivalence → ℕ → Std.Format

Equations

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

def Phenomena.Questions.MultipleWh.johnSuzy_equiv : AnswerEquivalence

Equations

• Phenomena.Questions.MultipleWh.johnSuzy_equiv = { question := "Which man loves which woman?", shortAnswer := "John, Suzy", longAnswer := "John loves Suzy" }

def Phenomena.Questions.MultipleWh.answerEquivalenceExamples : List AnswerEquivalence

Equations

• Phenomena.Questions.MultipleWh.answerEquivalenceExamples = [Phenomena.Questions.MultipleWh.johnSuzy_equiv]

inductive Phenomena.Questions.MultipleWh.MultiWhReading : Type

Some multiple-wh questions have both pair-list and single-pair readings. G&S focus on exhaustive (pair-list) readings.

• pairList : MultiWhReading
• singlePair : MultiWhReading

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instDecidableEqMultiWhReading : DecidableEq MultiWhReading

Equations

• Phenomena.Questions.MultipleWh.instDecidableEqMultiWhReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.MultipleWh.instReprMultiWhReading.repr : MultiWhReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instReprMultiWhReading : Repr MultiWhReading

Equations

• Phenomena.Questions.MultipleWh.instReprMultiWhReading = { reprPrec := Phenomena.Questions.MultipleWh.instReprMultiWhReading.repr }

def Phenomena.Questions.MultipleWh.defaultReading : MultiWhReading

G&S: The default/semantic reading is pair-list (exhaustive). Single-pair readings are pragmatic/mention-some.

Equations

• Phenomena.Questions.MultipleWh.defaultReading = Phenomena.Questions.MultipleWh.MultiWhReading.pairList

structure Phenomena.Questions.MultipleWh.TermCategory : Type

G&S define a hierarchy of term categories: T^0 = S/S (sentence adverbs: yes, no) T^1 = S/AB^1 (ordinary terms: John, everyone) T^2 = S/AB^2 (2-place terms: John, Mary) T^n = S/AB^n (n-place terms)

• arity : ℕ

  The arity

• examples : List String

  Example expressions

• typeDesc : String

  Type description

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instReprTermCategory : Repr TermCategory

Equations

• Phenomena.Questions.MultipleWh.instReprTermCategory = { reprPrec := Phenomena.Questions.MultipleWh.instReprTermCategory.repr }

def Phenomena.Questions.MultipleWh.instReprTermCategory.repr : TermCategory → ℕ → Std.Format

Equations

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

def Phenomena.Questions.MultipleWh.t0_category : TermCategory

Equations

• Phenomena.Questions.MultipleWh.t0_category = { arity := 0, examples := ["yes", "no", "if Mary walks"], typeDesc := "S/S (sentence adverbs)" }

def Phenomena.Questions.MultipleWh.t1_category : TermCategory

Equations

• Phenomena.Questions.MultipleWh.t1_category = { arity := 1, examples := ["John", "everyone", "the student who left"], typeDesc := "S/(S/e) (ordinary terms)" }

def Phenomena.Questions.MultipleWh.t2_category : TermCategory

Equations

• Phenomena.Questions.MultipleWh.t2_category = { arity := 2, examples := ["John, Mary", "every man, a girl"], typeDesc := "S/((S/e)/e) (2-place terms)" }

def Phenomena.Questions.MultipleWh.termCategories : List TermCategory

Equations

• Phenomena.Questions.MultipleWh.termCategories = [Phenomena.Questions.MultipleWh.t0_category, Phenomena.Questions.MultipleWh.t1_category, Phenomena.Questions.MultipleWh.t2_category]

Languages vary in whether multiple wh-specifiers at a phase edge are tolerable at PF (@cite{rudin-1988}, @cite{citko-gracanin-yuksek-2025}). The substrate primitives (MWFParameter, PhaseEdge, EdgeAsterisk, MWFViolation, EllipsisRepairsMWF) are in Linglib/Typology/Question.lean per the project layering convention; this file holds only the per-language data + theorems consuming it.

The intra-English variety A/B split (paper-specific to @cite{citko-gracanin-yuksek-2025}) lives in Phenomena/Ellipsis/Studies/CitkoGracaninYuksek2025.lean.

structure Phenomena.Questions.MultipleWh.MWFLanguageDatum : Type

Cross-linguistic MWF datum. Records the parameter setting and an example question. AllowsMultipleSluicing is derived from the parameter via EllipsisRepairsMWF.

• language : String
• mwfParam : Typology.Question.MWFParameter
• exampleQuestion : String

  Example multiple wh-question.

• grammatical : Bool

  Is the bare multiple-wh question grammatical?

• notes : String

def Phenomena.Questions.MultipleWh.instReprMWFLanguageDatum.repr : MWFLanguageDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instReprMWFLanguageDatum : Repr MWFLanguageDatum

Equations

• Phenomena.Questions.MultipleWh.instReprMWFLanguageDatum = { reprPrec := Phenomena.Questions.MultipleWh.instReprMWFLanguageDatum.repr }

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instDecidableEqMWFLanguageDatum : DecidableEq MWFLanguageDatum

Equations

• Phenomena.Questions.MultipleWh.instDecidableEqMWFLanguageDatum = Phenomena.Questions.MultipleWh.instDecidableEqMWFLanguageDatum.decEq

def Phenomena.Questions.MultipleWh.instDecidableEqMWFLanguageDatum.decEq (x✝ x✝¹ : MWFLanguageDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Questions.MultipleWh.MWFLanguageDatum.AllowsMultipleSluicing (d : MWFLanguageDatum) : Prop

Multiple sluicing is licensed iff vP-edge ellipsis repairs the MWF violation for n = 2 wh-specifiers. Derived, not stipulated.

Equations

• d.AllowsMultipleSluicing = Typology.Question.EllipsisRepairsMWF d.mwfParam 2 true

@[implicit_reducible]

instance Phenomena.Questions.MultipleWh.instDecidableAllowsMultipleSluicing (d : MWFLanguageDatum) : Decidable d.AllowsMultipleSluicing

Equations

• Phenomena.Questions.MultipleWh.instDecidableAllowsMultipleSluicing d = id inferInstance

def Phenomena.Questions.MultipleWh.bulgarian : MWFLanguageDatum

Bulgarian: MWF language (@cite{rudin-1988} canonical case).

Equations

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

def Phenomena.Questions.MultipleWh.german : MWFLanguageDatum

German: non-MWF; vP-only asterisk; multiple sluicing repairs. @cite{citko-gracanin-yuksek-2025} ex 31a.

Equations

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

def Phenomena.Questions.MultipleWh.greek : MWFLanguageDatum

Greek: non-MWF; vP-only asterisk; multiple sluicing repairs. @cite{citko-gracanin-yuksek-2025} ex 31b.

Equations

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

def Phenomena.Questions.MultipleWh.mwfLanguageTable : List MWFLanguageDatum

Cross-linguistic MWF table (textbook-consensus subset).

Equations

• Phenomena.Questions.MultipleWh.mwfLanguageTable = [Phenomena.Questions.MultipleWh.bulgarian, Phenomena.Questions.MultipleWh.german, Phenomena.Questions.MultipleWh.greek]

theorem Phenomena.Questions.MultipleWh.bulgarian_no_violation : ¬Typology.Question.MWFViolation bulgarian.mwfParam 2

Bulgarian: MWF language → no violations on bare multiple wh.

theorem Phenomena.Questions.MultipleWh.german_violates_in_questions : Typology.Question.MWFViolation german.mwfParam 2

German question with two wh-phrases is starred.

theorem Phenomena.Questions.MultipleWh.german_greek_sluicing_repairs : german.AllowsMultipleSluicing ∧ greek.AllowsMultipleSluicing

Sluicing repairs in German and Greek (vP-only asterisk eliminated).