@cite{kay-fillmore-1999}: What's X Doing Y? — Empirical Data

@cite{kay-fillmore-1999}

Theory-neutral judgment data from "Grammatical Constructions and Linguistic Generalizations: The What's X doing Y? Construction" (Language 75(1):1–33).

Phenomena covered

1. Incredulity reading: "What's this fly doing in my soup?" (speaker knows the answer)
2. Literal question reading: "What's John doing in the kitchen?" (genuine information-seeking)
3. Progressive requirement: WXDY requires progressive doing; bare infinitive is out
4. Subject referentiality: referential subjects OK; non-referential degraded
5. Complement types: locative PP, participial VP, instrumental PP
6. Ambiguity: sentences admitting both readings
7. Embedding / CI projection: WXDY meaning under embedding predicates
8. FKO1988 comparison: relation to Incredulity Response construction

def Phenomena.Constructions.Studies.KayFillmore1999.containsSubstr (s sub : String) : Bool

Check if a string contains a substring.

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.containsSubstr s sub = decide ((s.splitOn sub).length > 1)

Reading type

inductive Phenomena.Constructions.Studies.KayFillmore1999.WXDYReading : Type

The available readings of a WXDY sentence.

• literal : WXDYReading
• incredulity : WXDYReading
• ambiguous : WXDYReading

def Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYReading.repr : WXDYReading → ℕ → Std.Format

Equations

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

instance Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYReading : Repr WXDYReading

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYReading = { reprPrec := Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYReading.repr }

instance Phenomena.Constructions.Studies.KayFillmore1999.instDecidableEqWXDYReading : DecidableEq WXDYReading

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.instDecidableEqWXDYReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYReading.beq : WXDYReading → WXDYReading → Bool

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYReading : BEq WXDYReading

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYReading = { beq := Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYReading.beq }

Datum structure

structure Phenomena.Constructions.Studies.KayFillmore1999.WXDYDatum : Type

A single WXDY example with judgment and reading information.

• exId : String

  Example identifier

• sentence : String

  The sentence

• judgment : Core.Empirical.Acceptability

  Acceptability judgment

• reading : WXDYReading

  Available reading(s)

• phenomenon : String

  What phenomenon this illustrates

def Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYDatum.repr : WXDYDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYDatum : Repr WXDYDatum

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYDatum = { reprPrec := Phenomena.Constructions.Studies.KayFillmore1999.instReprWXDYDatum.repr }

def Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYDatum.beq : WXDYDatum → WXDYDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYDatum.beq x✝¹ x✝ = false

instance Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYDatum : BEq WXDYDatum

Equations

• Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYDatum = { beq := Phenomena.Constructions.Studies.KayFillmore1999.instBEqWXDYDatum.beq }

1. Basic incredulity (§1, pp.1–3)

def Phenomena.Constructions.Studies.KayFillmore1999.fly_in_soup : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.cat_on_table : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.car_in_driveway : WXDYDatum

Equations

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

2. Literal question (genuine information-seeking)

def Phenomena.Constructions.Studies.KayFillmore1999.john_in_kitchen_literal : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.mary_with_scissors : WXDYDatum

Equations

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

3. Progressive requirement (§2.2)

WXDY requires the progressive auxiliary + doing. Without it, only a standard wh-question remains; the incredulity reading disappears.

def Phenomena.Constructions.Studies.KayFillmore1999.no_progressive : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.habitual_do : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.bare_infinitive : WXDYDatum

Equations

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

4. Subject referentiality (§2.3)

Referential subjects are fine; non-referential or quantified subjects are degraded on the incredulity reading.

def Phenomena.Constructions.Studies.KayFillmore1999.referential_subject : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.nonreferential_subject : WXDYDatum

Equations

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

5. Complement types (§2.4)

WXDY accepts various complement types: locative PPs, participial VPs, and instrumental PPs.

def Phenomena.Constructions.Studies.KayFillmore1999.locative_pp : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.participial_vp : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.instrumental_pp : WXDYDatum

Equations

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

6. Ambiguous (both readings available)

def Phenomena.Constructions.Studies.KayFillmore1999.john_in_kitchen_ambig : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.dog_on_couch : WXDYDatum

Equations

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

7. Embedding / CI projection (§3)

Under embedding, the incredulity component projects like a CI.

def Phenomena.Constructions.Studies.KayFillmore1999.embedded_wonder : WXDYDatum

Equations

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

def Phenomena.Constructions.Studies.KayFillmore1999.embedded_tell : WXDYDatum

Equations

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

8. FKO1988 comparison

WXDY relates to the Incredulity Response construction from FKO1988 ("Him be a doctor?"). Both express speaker incredulity via non-standard question form.

def Phenomena.Constructions.Studies.KayFillmore1999.fko_comparison : WXDYDatum

Equations

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

All data

def Phenomena.Constructions.Studies.KayFillmore1999.allExamples : List WXDYDatum

Equations

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

Verification theorems

theorem Phenomena.Constructions.Studies.KayFillmore1999.has_both_readings : (allExamples.any fun (x : WXDYDatum) => x.reading == WXDYReading.literal) = true ∧ (allExamples.any fun (x : WXDYDatum) => x.reading == WXDYReading.incredulity) = true ∧ (allExamples.any fun (x : WXDYDatum) => x.reading == WXDYReading.ambiguous) = true

Both readings are attested in the data.

theorem Phenomena.Constructions.Studies.KayFillmore1999.has_all_judgment_types : (allExamples.any fun (x : WXDYDatum) => x.judgment == Core.Empirical.Acceptability.ok) = true ∧ (allExamples.any fun (x : WXDYDatum) => x.judgment == Core.Empirical.Acceptability.unacceptable) = true ∧ (allExamples.any fun (x : WXDYDatum) => x.judgment == Core.Empirical.Acceptability.marginal) = true

All judgment types are represented.

theorem Phenomena.Constructions.Studies.KayFillmore1999.progressive_is_required : ((List.filter (fun (d : WXDYDatum) => d.judgment == Core.Empirical.Acceptability.ok && d.reading != WXDYReading.literal) allExamples).all fun (d : WXDYDatum) => containsSubstr d.sentence "doing" || containsSubstr d.sentence "is doing") = true

All grammatical WXDY examples with incredulity reading have progressive.

Bridge content (merged from CxG_KayFillmore1999Bridge.lean)

@cite{kay-fillmore-1999}: What's X Doing Y? Construction

@cite{kay-fillmore-1999} @cite{dayal-2025} @cite{potts-2005}

Formalization of "Grammatical Constructions and Linguistic Generalizations: The What's X doing Y? Construction" (Language 75(1):1–33).

Key insight

WXDY has interrogative form but expressive function on the incredulity reading. This form–function mismatch is precisely what the existing LeftPeriphery + Expressives + Presupposition infrastructure can derive:

• Interrogative form: +WH feature, wh-fronting, subject-aux inversion
• Expressive function: CI content (unexpectedness), presupposed proposition

The two readings are distinguished by the PerspectiveP layer:

• Literal: speaker is ignorant → PerspP satisfied → genuine question
• Incredulity: speaker knows the answer → PerspP blocked → not a real question

Bridge targets (10 modules)

#	Module	Bridge
1	Core/Presupposition	WXDY presupposes the embedded proposition
2	Expressives/Basic	Incredulity is CI content (projects through negation)
3	Semantics.Questions/Hamblin	Literal = standard which; incredulity = degenerate Q
4	Semantics.Questions/LeftPeriphery	PerspP disambiguates the two readings
5	Core/CommonGround	Presupposition requires CG entailment
6	Verb/Aspect	Progressive requirement (durative ∧ dynamic)
7	Focus/DomainWidening	Incongruity = normative expectation violation
8	Semantics.Questions/Polarity	Incredulity = rhetorical question
9	FKO1988	WXDY is a formal idiom; sibling to Incredulity Response
10	Phenomena/KayFillmore1999	Per-datum verification

def ConstructionGrammar.Studies.KayFillmore1999.wxdyConstruction : Construction

The WXDY construction as a Construction.

Form: [CP What's [TP NP doing [VP/PP...]]]

• Interrogative form: wh-fronting, subject-aux inversion, +WH
• doing is frozen progressive: licenses the construction
• Complement: locative PP, participial VP, or instrumental PP

Equations

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

def ConstructionGrammar.Studies.KayFillmore1999.wxdyIdiomType : FillmoreKayOConnor1988.IdiomType

WXDY is a formal idiom in FKO1988's typology: encoding (must learn the incredulity convention), grammatical (fills proper grammatical slots), formal (productive open pattern).

Equations

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

def ConstructionGrammar.Studies.KayFillmore1999.wxdyFamiliarity : FillmoreKayOConnor1988.FamiliarityPattern

WXDY uses familiar pieces in a familiar arrangement: "what", "doing", etc. are all standard English items in standard syntactic positions. The non-compositional meaning (incredulity) is what must be learned.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyFamiliarity = ConstructionGrammar.Studies.FillmoreKayOConnor1988.FamiliarityPattern.familiarPiecesFamiliarlyArranged

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_is_formal_idiom : wxdyIdiomType.formality = FillmoreKayOConnor1988.IdiomFormality.formal ∧ wxdyConstruction.specificity = Specificity.partiallyOpen ∧ wxdyConstruction.pragmaticFunction.isSome = true

WXDY is a formal idiom: partially open, with pragmatic function.

def ConstructionGrammar.Studies.KayFillmore1999.wxdyInheritanceFromWhQ : InheritanceLink

WXDY inherits from wh-questions: wh-fronting, +WH feature, subject-aux inversion. Overrides: question semantics (on the incredulity reading, it's not a genuine information-seeking question).

Equations

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

def ConstructionGrammar.Studies.KayFillmore1999.wxdyInheritanceFromProgressive : InheritanceLink

WXDY inherits progressive morphology from the progressive construction: doing carries -ing morphology.

Equations

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

def ConstructionGrammar.Studies.KayFillmore1999.wxdyInheritanceFromIncredulity : InheritanceLink

WXDY and FKO1988's Incredulity Response ("Him be a doctor?") are siblings in the "rhetorical question family" — both express incredulity via non-standard question forms.

Equations

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

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_same_class_as_incredulity_response : wxdyInheritanceFromIncredulity.parent = "Rhetorical question family"

WXDY and the Incredulity Response share the same expressive family.

def ConstructionGrammar.Studies.KayFillmore1999.wxdyPresup {W : Type u_1} (embeddedProp : W → Bool) : Core.Presupposition.PrProp W

On the incredulity reading, WXDY presupposes the embedded proposition (the situation that the speaker finds surprising) and has trivial assertion.

"What's this fly doing in my soup?" presupposes: there is a fly in the soup. The at-issue assertion is trivial — the point is to express the CI.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyPresup embeddedProp = { presup := embeddedProp, assertion := fun (x : W) => true }

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_presup_projects_neg {W : Type u_1} (embeddedProp : W → Bool) : (wxdyPresup embeddedProp).neg.presup = embeddedProp

Presupposition projects through negation: "It's not the case that [what's this fly doing in my soup]" still presupposes the fly is there.

def ConstructionGrammar.Studies.KayFillmore1999.wxdyTwoDim {W : Type u_1} (embeddedProp unexpectedness : W → Bool) : Semantics.Lexical.Expressives.TwoDimProp W

WXDY on the incredulity reading has two-dimensional meaning:

• At-issue: the embedded proposition (there's a fly in my soup)
• CI: speaker finds this unexpected/inappropriate

This mirrors @cite{potts-2005}'s analysis of expressives: the expressive content is independent of at-issue truth.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyTwoDim embeddedProp unexpectedness = Semantics.Lexical.Expressives.TwoDimProp.withCI embeddedProp unexpectedness

def ConstructionGrammar.Studies.KayFillmore1999.wxdyCIProperties : Semantics.Lexical.Expressives.CIExprProperties

WXDY's CI properties: speaker-oriented, not repeatable (you don't say "What's this fly doing in my soup?" twice for emphasis), immediate (affects context just by being uttered), independent of at-issue truth.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyCIProperties = { speakerOriented := true, repeatable := false, immediate := true, independent := true }

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_ci_projects_through_neg {W : Type u_1} (embeddedProp unexpectedness : W → Bool) : (wxdyTwoDim embeddedProp unexpectedness).neg.ci = unexpectedness

CI projects through negation: the unexpectedness meaning survives under negation. Delegates to TwoDimProp.ci_projects_through_neg.

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_ci_independent {W : Type u_1} (embeddedProp unexpectedness : W → Bool) (w : W) (h_ci : unexpectedness w = true) : ((wxdyTwoDim embeddedProp unexpectedness).atIssue w = true → (wxdyTwoDim embeddedProp unexpectedness).ci w = true) ∧ ((wxdyTwoDim embeddedProp unexpectedness).atIssue w = false → (wxdyTwoDim embeddedProp unexpectedness).ci w = true)

CI is independent of at-issue truth: the unexpectedness holds regardless of whether the embedded proposition is true or false.

def ConstructionGrammar.Studies.KayFillmore1999.wxdyLiteralQ {W : Type u_1} {E : Type u_2} [BEq W] (activities : List E) (pred : E → W → Bool) (worlds : List W) : Semantics.Questions.Hamblin.QuestionDen W

Literal reading: standard wh-question "which activity is X engaged in?" Delegates to Hamblin.which over a domain of activities.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyLiteralQ activities pred worlds = Semantics.Questions.Hamblin.which activities pred worlds

def ConstructionGrammar.Studies.KayFillmore1999.wxdyIncredulityQ {W : Type u_1} [BEq W] (presupposedProp : W → Bool) (worlds : List W) : Semantics.Questions.Hamblin.QuestionDen W

Incredulity reading: degenerate question with only the presupposed proposition as an answer. The "question" is not information-seeking; the speaker already knows the answer.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyIncredulityQ presupposedProp worlds ans = worlds.all fun (w : W) => ans w == presupposedProp w

theorem ConstructionGrammar.Studies.KayFillmore1999.incredulity_single_answer {W : Type u_1} [BEq W] [LawfulBEq W] (presupposedProp : W → Bool) (worlds : List W) : wxdyIncredulityQ presupposedProp worlds presupposedProp = true

The incredulity reading has exactly one answer: the presupposed proposition. The proposition itself is trivially recognized as an answer.

theorem ConstructionGrammar.Studies.KayFillmore1999.literal_is_genuine_question {W : Type u_1} {E : Type u_2} [BEq W] (activities : List E) (pred : E → W → Bool) (worlds : List W) : wxdyLiteralQ activities pred worlds = Semantics.Questions.Hamblin.which activities pred worlds

The literal reading is a genuine (non-degenerate) question: it delegates to standard Hamblin.which, which partitions the answer space by activity.

def ConstructionGrammar.Studies.KayFillmore1999.wxdyWHFeature : Semantics.Questions.LeftPeriphery.WHFeature

WXDY has a +WH feature on C (it is syntactically interrogative).

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyWHFeature = Semantics.Questions.LeftPeriphery.WHFeature.plusWH

def ConstructionGrammar.Studies.KayFillmore1999.wxdyIncredulitySpeakerModel {W : Type u_1} (w : W) : Semantics.Questions.LeftPeriphery.EpistemicModel W

On the incredulity reading, the speaker KNOWS the answer to the question. This is modeled as a veridical epistemic model at the evaluation world.

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyIncredulitySpeakerModel w = Semantics.Questions.LeftPeriphery.veridicalModel w

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_incredulity_blocks_perspP {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : Semantics.Questions.LeftPeriphery.perspPPresupComp (wxdyIncredulitySpeakerModel w) q w = false

CORE DERIVATION: Veridical speaker model → PerspP presupposition fails → not a real question.

On the incredulity reading, the speaker knows the answer (veridical model). PerspP presupposes possible ignorance: ◇¬know(speaker, Ans(Q)). But veridical knowledge contradicts possible ignorance. Therefore PerspP is blocked, and the utterance is NOT a genuine question.

Delegates to responsive_contradicts_perspP_comp from LeftPeriphery.lean.

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_literal_allows_perspP {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : Semantics.Questions.LeftPeriphery.perspPPresupComp Semantics.Questions.LeftPeriphery.ignorantModel q w = true

On the literal reading, the speaker is genuinely ignorant (ignorant model). PerspP presupposition is satisfied → genuine question.

Delegates to rogative_allows_perspP_comp from LeftPeriphery.lean.

theorem ConstructionGrammar.Studies.KayFillmore1999.perspP_disambiguates_wxdy {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : Semantics.Questions.LeftPeriphery.perspPPresupComp (wxdyIncredulitySpeakerModel w) q w = false ∧ Semantics.Questions.LeftPeriphery.perspPPresupComp Semantics.Questions.LeftPeriphery.ignorantModel q w = true

PerspP STATUS DISAMBIGUATES the two readings:

• Incredulity: PerspP fails (veridical model) → not a question → expressive
• Literal: PerspP succeeds (ignorant model) → genuine question

This is the deepest bridge: the form–function mismatch of WXDY is derived from the PerspP mechanism, not stipulated.

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_presup_requires_cg {W : Type u_1} (c : Core.CommonGround.ContextSet W) (embeddedProp : W → Bool) (h : c ⊧ embeddedProp) (w : W) (hw : c w) : (wxdyPresup embeddedProp).presup w = true

The WXDY presupposition must be entailed by the common ground. For "What's this fly doing in my soup?", the CG must already entail that there is a fly in the soup (the speaker sees it).

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_requires_progressive_aspect (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) : Phenomena.TenseAspect.Diagnostics.progressivePrediction c = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept ↔ c.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative ∧ c.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

WXDY's doing selects for activities and accomplishments — predicates that are durative ∧ dynamic. This connects to the progressive diagnostic: progressivePrediction =.accept ↔ durative ∧ dynamic.

The progressive requirement in WXDY reflects the same aspectual constraint as the standard progressive: it selects predicates with internal stages.

def ConstructionGrammar.Studies.KayFillmore1999.wxdyAlternativeSource : Semantics.Montague.Sentence.DomainWidening.AlternativeSource

WXDY's incredulity arises from a normative expectation violation: the situation violates what the speaker considers normal/appropriate. This is the same alternative source as counterexpectational just ("He's just texting during the lecture!").

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyAlternativeSource = Semantics.Montague.Sentence.DomainWidening.AlternativeSource.normative

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_incongruity_is_counterexpectational : wxdyAlternativeSource = Semantics.Montague.Sentence.DomainWidening.associatedSource Phenomena.Focus.Exclusives.JustFlavor.counterexpectational

WXDY's incongruity and counterexpectational just share the same alternative source: both involve normative expectations being violated.

• WXDY: "What's this fly doing in my soup?" — violates dining norms
• just: "He's just texting during the lecture!" — violates classroom norms

def ConstructionGrammar.Studies.KayFillmore1999.wxdyAsRhetoricalQ {W : Type u_1} (prop : W → Bool) : Semantics.Questions.Polarity.RhetoricalQuestion W

WXDY on the incredulity reading is a rhetorical question:

• The speaker presupposes the positive answer (the situation obtains)
• Belief strength is maximal (speaker SEES the situation)
• Question form is used for pragmatic effect, not information seeking

Equations

• ConstructionGrammar.Studies.KayFillmore1999.wxdyAsRhetoricalQ prop = { prop := prop, presupposedPositive := true, beliefStrength := 1 }

theorem ConstructionGrammar.Studies.KayFillmore1999.wxdy_rhetorical_requires_polar {W : Type u_1} (prop : W → Bool) : Semantics.Questions.Polarity.expectedTypeForUse Semantics.Questions.Polarity.QuestionUse.rhetorical ≠ Semantics.Questions.Polarity.PolarQuestionType.alternative

Rhetorical questions require polar form — they cannot be alternative questions. WXDY on the incredulity reading has this property: you can't say *"What's this fly doing in my soup or not?"

theorem ConstructionGrammar.Studies.KayFillmore1999.progressive_required_all : ((List.filter (fun (d : Phenomena.Constructions.Studies.KayFillmore1999.WXDYDatum) => d.judgment == Core.Empirical.Acceptability.ok && d.reading != Phenomena.Constructions.Studies.KayFillmore1999.WXDYReading.literal) Phenomena.Constructions.Studies.KayFillmore1999.allExamples).all fun (d : Phenomena.Constructions.Studies.KayFillmore1999.WXDYDatum) => Phenomena.Constructions.Studies.KayFillmore1999.containsSubstr d.sentence "doing" || Phenomena.Constructions.Studies.KayFillmore1999.containsSubstr d.sentence "is doing") = true

All grammatical WXDY examples use progressive doing.

theorem ConstructionGrammar.Studies.KayFillmore1999.all_readings_attested : (Phenomena.Constructions.Studies.KayFillmore1999.allExamples.any fun (d : Phenomena.Constructions.Studies.KayFillmore1999.WXDYDatum) => d.reading == Phenomena.Constructions.Studies.KayFillmore1999.WXDYReading.literal) = true ∧ (Phenomena.Constructions.Studies.KayFillmore1999.allExamples.any fun (d : Phenomena.Constructions.Studies.KayFillmore1999.WXDYDatum) => d.reading == Phenomena.Constructions.Studies.KayFillmore1999.WXDYReading.incredulity) = true ∧ (Phenomena.Constructions.Studies.KayFillmore1999.allExamples.any fun (d : Phenomena.Constructions.Studies.KayFillmore1999.WXDYDatum) => d.reading == Phenomena.Constructions.Studies.KayFillmore1999.WXDYReading.ambiguous) = true

The data contains all three reading types.