[KF99]: What's X Doing Y?

"Grammatical Constructions and Linguistic Generalizations: The What's X doing Y? Construction" (Language 75(1):1–33). WXDY has interrogative form but expressive function on the incredulity reading; the form–function mismatch is derived rather than stipulated: the literal reading is a genuine question (speaker-ignorance satisfies the PerspP presupposition), the incredulity reading a blocked one (speaker knowledge contradicts it), with the presupposed proposition and the unexpectedness CI typed via PartialProp/TwoDimProp.

The paper's own inheritance hierarchy — WXDY inheriting from the left-isolation, subject–aux-inversion, and wh-interrogative constructions of its unification-based grammar — is recorded here only as prose; assembling it as a checked network awaits verification of the paper's figures.

Main declarations

• KayFillmore1999.wxdyConstruction: the construction, typed form per Figure 12
• KayFillmore1999.allExamples: judgment data
• KayFillmore1999.perspP_disambiguates_wxdy: the two readings derived
• KayFillmore1999.wxdyPresup, wxdyTwoDim: typed pragmatics

Reading type

inductive KayFillmore1999.WXDYReading : Type

The available readings of a WXDY sentence.

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

@[implicit_reducible]

instance KayFillmore1999.instReprWXDYReading : Repr WXDYReading

Equations

• KayFillmore1999.instReprWXDYReading = { reprPrec := KayFillmore1999.instReprWXDYReading.repr }

def KayFillmore1999.instReprWXDYReading.repr : WXDYReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KayFillmore1999.instDecidableEqWXDYReading : DecidableEq WXDYReading

Equations

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

Datum structure

structure KayFillmore1999.WXDYDatum : Type

A single WXDY example with judgment and reading information.

• exId : String

  Example identifier

• sentence : String

  The sentence

• judgment : Features.Acceptability

  Acceptability judgment

• reading : WXDYReading

  Available reading(s)

• phenomenon : String

  What phenomenon this illustrates

def KayFillmore1999.instReprWXDYDatum.repr : WXDYDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KayFillmore1999.instReprWXDYDatum : Repr WXDYDatum

Equations

• KayFillmore1999.instReprWXDYDatum = { reprPrec := KayFillmore1999.instReprWXDYDatum.repr }

def KayFillmore1999.instBEqWXDYDatum.beq : WXDYDatum → WXDYDatum → Bool

Equations

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

@[implicit_reducible]

instance KayFillmore1999.instBEqWXDYDatum : BEq WXDYDatum

Equations

• KayFillmore1999.instBEqWXDYDatum = { beq := KayFillmore1999.instBEqWXDYDatum.beq }

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

def KayFillmore1999.fly_in_soup : WXDYDatum

Equations

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

def KayFillmore1999.cat_on_table : WXDYDatum

Equations

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

def 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 KayFillmore1999.john_in_kitchen_literal : WXDYDatum

Equations

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

def 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 KayFillmore1999.no_progressive : WXDYDatum

Equations

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

def KayFillmore1999.habitual_do : WXDYDatum

Equations

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

def 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 KayFillmore1999.referential_subject : WXDYDatum

Equations

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

def 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 KayFillmore1999.locative_pp : WXDYDatum

Equations

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

def KayFillmore1999.participial_vp : WXDYDatum

Equations

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

def KayFillmore1999.instrumental_pp : WXDYDatum

Equations

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

6. Ambiguous (both readings available)

def KayFillmore1999.john_in_kitchen_ambig : WXDYDatum

Equations

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

def 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 KayFillmore1999.embedded_wonder : WXDYDatum

Equations

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

def 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 KayFillmore1999.fko_comparison : WXDYDatum

Equations

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

All data

def KayFillmore1999.allExamples : List WXDYDatum

Equations

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

Verification theorems

theorem 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 KayFillmore1999.has_all_judgment_types : (allExamples.any fun (x : WXDYDatum) => x.judgment == Features.Acceptability.ok) = true ∧ (allExamples.any fun (x : WXDYDatum) => x.judgment == Features.Acceptability.unacceptable) = true ∧ (allExamples.any fun (x : WXDYDatum) => x.judgment == Features.Acceptability.marginal) = true

All judgment types are represented.

The construction

def KayFillmore1999.wxdyConstruction : ConstructionGrammar.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

The typed form is the flat projection of Figure 12's hierarchical AVM: X and Y share refIdx 2 (coinstantiation/subject control); WXDY-what is left-isolated ([loc -]) and nonreferential ([ref ∅]); doing cannot be negated ([neg -]).

Equations

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

FKO1988 idiom classification bridge

def KayFillmore1999.wxdyIdiomType : ConstructionGrammar.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 KayFillmore1999.wxdyFamiliarity : ConstructionGrammar.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

• KayFillmore1999.wxdyFamiliarity = ConstructionGrammar.FamiliarityPattern.familiarPiecesFamiliarlyArranged

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

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

Presupposition bridge (Core/Presupposition.lean)

def KayFillmore1999.wxdyPresup {W : Type u_1} (embeddedProp : W → Prop) : Semantics.Presupposition.PartialProp 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

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

theorem KayFillmore1999.wxdy_presup_projects_neg {W : Type u_1} (embeddedProp : W → Prop) (w : W) : (wxdyPresup embeddedProp).neg.presup w ↔ embeddedProp w

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

Two-dimensional semantics bridge (Expressives/Basic.lean)

def KayFillmore1999.wxdyTwoDim {W : Type u_1} (embeddedProp unexpectedness : W → Prop) : Pragmatics.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 [Pot05]'s analysis of expressives: the expressive content is independent of at-issue truth.

Equations

• KayFillmore1999.wxdyTwoDim embeddedProp unexpectedness = Pragmatics.Expressives.TwoDimProp.withCI embeddedProp unexpectedness

def KayFillmore1999.wxdyCIProperties : Pragmatics.Expressives.SecondaryMeaningProperties

WXDY's CI properties: perspective-dependent (speaker-oriented), not repeatable (you don't say "What's this fly doing in my soup?" twice for emphasis), immediate, independent, nondisplaceable, descriptively ineffable (the unexpectedness resists paraphrase).

Equations

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

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

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

theorem KayFillmore1999.wxdy_ci_independent {W : Type u_1} (embeddedProp unexpectedness : W → Prop) (w : W) (h_ci : unexpectedness w) : ((wxdyTwoDim embeddedProp unexpectedness).atIssue w → (wxdyTwoDim embeddedProp unexpectedness).ci w) ∧ (¬(wxdyTwoDim embeddedProp unexpectedness).atIssue w → (wxdyTwoDim embeddedProp unexpectedness).ci w)

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

Hamblin question semantics bridge (Semantics/Questions/Hamblin.lean substrate)

def KayFillmore1999.wxdyLiteralQ {W : Type u_1} {E : Type u_2} (activities : Set E) (pred : E → Set W) : Question W

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

Equations

• KayFillmore1999.wxdyLiteralQ activities pred = Question.which activities pred

def KayFillmore1999.wxdyIncredulityQ {W : Type u_1} (presupposedProp : Set W) : Question 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.

In the substrate, this is the declarative principal ideal of the presupposed proposition — a single-alternative question.

Equations

• KayFillmore1999.wxdyIncredulityQ presupposedProp = Question.declarative presupposedProp

theorem KayFillmore1999.incredulity_single_answer {W : Type u_1} (presupposedProp : Set W) : (wxdyIncredulityQ presupposedProp).alt = {presupposedProp}

The incredulity reading has exactly one alternative: the presupposed proposition. The proposition itself is the unique alternative.

theorem KayFillmore1999.literal_is_genuine_question {W : Type u_1} {E : Type u_2} (activities : Set E) (pred : E → Set W) : wxdyLiteralQ activities pred = Question.which activities pred

The literal reading is a genuine (non-degenerate) question: it delegates to substrate Question.which, which yields a Hamblin-style alternative set indexed by the activity domain.

Left Periphery bridge (ArgumentStructure.Linking/LeftPeriphery.lean) — DEEPEST BRIDGE

def KayFillmore1999.wxdyWHFeature : Minimalist.LeftPeriphery.WHFeature

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

Equations

• KayFillmore1999.wxdyWHFeature = Minimalist.LeftPeriphery.WHFeature.plusWH

def KayFillmore1999.wxdyIncredulitySpeakerModel {W : Type u_1} (w : W) : Minimalist.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

• KayFillmore1999.wxdyIncredulitySpeakerModel w = Minimalist.LeftPeriphery.veridicalModel w

theorem KayFillmore1999.wxdy_incredulity_blocks_perspP {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : Minimalist.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 KayFillmore1999.wxdy_literal_allows_perspP {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : Minimalist.LeftPeriphery.perspPPresupComp Minimalist.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 KayFillmore1999.perspP_disambiguates_wxdy {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w : W) : Minimalist.LeftPeriphery.perspPPresupComp (wxdyIncredulitySpeakerModel w) q w = false ∧ Minimalist.LeftPeriphery.perspPPresupComp Minimalist.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.

Common ground bridge (Core/CommonGround.lean)

theorem KayFillmore1999.wxdy_presup_requires_cg {W : Type u_1} (c : CommonGround.ContextSet W) (embeddedProp : W → Prop) (h : c.entails (wxdyPresup embeddedProp).presup) (w : W) (hw : c w) : (wxdyPresup embeddedProp).presup w

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

Aspect bridge (Semantics.Montague/Verb/Aspect.lean + Diagnostics)

theorem KayFillmore1999.wxdy_requires_progressive_aspect (c : Features.VendlerClass) : Features.progressivePrediction c = Features.DiagnosticResult.accept ↔ c.duration = Features.Duration.durative ∧ c.dynamicity = Features.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.