Evcen, Bale & Barner (2026): QUD, knowledge, and conditional perfection

[EBB26] test [vF01]'s answer-level exhaustivity account of conditional perfection in a three-button paradigm: Mary presses buttons that each play a sound only she can hear, answers a question with a conditional ("If you press the blue button, it will play a dog barking"), and participants judge whether a different button plays the sound ("No" = perfected). Perfection rates (estimated marginal means of "No" responses from logistic mixed-effects regressions):

• QUD (Exp 1, N = 98, between-subjects): antecedent-focused questions ("Which of these buttons will play a dog sound?") yield far more perfection (M = 0.65) than consequent-focused (M = 0.22) or neutral (M = 0.29) ones, which do not differ (p > .05).
• Answer form (Exp 2, N = 55, within-subjects): optimally (M = 0.92) and overly (M = 0.84) informative answers perfect at comparable rates (p = .16) — overly informative answers still count as QUD answers.
• Speaker knowledge (Exp 3, N = 72, within-subjects): a speaker who tested all buttons (M = 0.72) licenses far more perfection than one who tested only two (M = 0.21).

The paper's ALT constraint — alternatives are QUD answers the speaker is competent about, ALT(p) ⊆ ANS(QUD) ∩ {q : Kₛ(q) ∨ Kₛ(¬q)} — is exhaustificationLicensed; the competence half is BaleEtAl2025.Competent, derived from the speaker's observation state, the same derivation [BNRB25]'s scalar-implicature paradigm uses, so conditional perfection and scalar implicature share the competence gate by construction. Perfection is not a semantic entailment (Semantics.Conditionals.perfection_not_entailed_variablyStrict), and coverage without exclusion does not suffice (VonFintel2001.coverage_without_exclusion_insufficient).

Main results

• perfection_of_exhaustifiedAnswer: in the three-button scenario, exhaustifying Mary's answer yields conditionalPerfection.
• exhaustificationLicensed_iff: exhaustification is licensed exactly under an antecedent-focused QUD with a fully knowledgeable speaker.
• exp1_licensing / exp3_licensing: the licensed condition shows the highest observed perfection rate in each experiment.
• horn_not_entails_vonFintel: [Hor00]'s existential exclusion is strictly weaker than per-trigger exclusion — the paradigm's per-button "No" responses require the latter.

Experimental conditions and observed rates

inductive EvcenBaleBarner2026.QUDType : Type

QUD manipulation (Experiment 1): the question Mary's conditional answers.

• antecedentFocused : QUDType

  "Which of these buttons will play a dog sound?"

• consequentFocused : QUDType

  "What will happen if I press the blue button?"

• neutral : QUDType

  "What will happen if I press the buttons?"

@[instance_reducible]

instance EvcenBaleBarner2026.instDecidableEqQUDType : DecidableEq QUDType

Equations

• EvcenBaleBarner2026.instDecidableEqQUDType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive EvcenBaleBarner2026.AnswerType : Type

Answer-form manipulation (Experiment 2): whether Mary's conditional names a QUD cell or a strict subset of one.

• optimallyInformative : AnswerType

  "If you press the triangles, it will play a dog barking."

• overlyInformative : AnswerType

  "If you press the blue square, it will play a dog barking."

@[instance_reducible]

instance EvcenBaleBarner2026.instDecidableEqAnswerType : DecidableEq AnswerType

Equations

• EvcenBaleBarner2026.instDecidableEqAnswerType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def EvcenBaleBarner2026.exp1Rate : QUDType → ℚ

Experiment 1 perfection rate by QUD type (N = 98). Follow-ups with "what buttons" (M = 0.86, n = 32) and "which buttons" (M = 0.77, n = 32) phrasings replicate the antecedent-focused effect, ruling out a uniqueness presupposition from "which of these".

Equations

• EvcenBaleBarner2026.exp1Rate EvcenBaleBarner2026.QUDType.antecedentFocused = 65 / 100
• EvcenBaleBarner2026.exp1Rate EvcenBaleBarner2026.QUDType.consequentFocused = 22 / 100
• EvcenBaleBarner2026.exp1Rate EvcenBaleBarner2026.QUDType.neutral = 29 / 100

def EvcenBaleBarner2026.exp2Rate : AnswerType → ℚ

Experiment 2 perfection rate by answer form (N = 55; QUD always antecedent-focused). The two rates do not differ reliably (p = .16).

Equations

• EvcenBaleBarner2026.exp2Rate EvcenBaleBarner2026.AnswerType.optimallyInformative = 92 / 100
• EvcenBaleBarner2026.exp2Rate EvcenBaleBarner2026.AnswerType.overlyInformative = 84 / 100

def EvcenBaleBarner2026.exp3Rate : BaleEtAl2025.SpeakerKnowledge → ℚ

Experiment 3 perfection rate by speaker knowledge (N = 72; QUD always antecedent-focused): Mary tested all three buttons or only two.

Equations

• EvcenBaleBarner2026.exp3Rate BaleEtAl2025.SpeakerKnowledge.fullKnowledge = 72 / 100
• EvcenBaleBarner2026.exp3Rate BaleEtAl2025.SpeakerKnowledge.partialKnowledge = 21 / 100

When exhaustification is licensed

def EvcenBaleBarner2026.qudProvidesAlternatives (q : QUDType) : Prop

A QUD makes alternative antecedents salient iff it is antecedent-focused.

Equations

• EvcenBaleBarner2026.qudProvidesAlternatives q = (q = EvcenBaleBarner2026.QUDType.antecedentFocused)

def EvcenBaleBarner2026.exhaustificationLicensed (k : BaleEtAl2025.SpeakerKnowledge) (q : QUDType) : Prop

Exhaustification is licensed when the QUD provides alternative antecedents and the speaker is competent about them — the paper's ALT constraint ALT(p) ⊆ ANS(QUD) ∩ {q : Kₛ(q) ∨ Kₛ(¬q)}.

Equations

• EvcenBaleBarner2026.exhaustificationLicensed k q = (EvcenBaleBarner2026.qudProvidesAlternatives q ∧ BaleEtAl2025.Competent k)

@[simp]

theorem EvcenBaleBarner2026.exhaustificationLicensed_iff {k : BaleEtAl2025.SpeakerKnowledge} {q : QUDType} : exhaustificationLicensed k q ↔ q = QUDType.antecedentFocused ∧ k = BaleEtAl2025.SpeakerKnowledge.fullKnowledge

Exhaustification is licensed exactly under an antecedent-focused QUD with a fully knowledgeable speaker.

Licensing predicts the observed rates

theorem EvcenBaleBarner2026.exp1_licensing (q : QUDType) (h : ¬exhaustificationLicensed BaleEtAl2025.SpeakerKnowledge.fullKnowledge q) : exp1Rate q < exp1Rate QUDType.antecedentFocused

Experiment 1 (fully knowledgeable speaker): every unlicensed QUD condition shows less perfection than the licensed one.

theorem EvcenBaleBarner2026.exp3_licensing (k : BaleEtAl2025.SpeakerKnowledge) (h : ¬exhaustificationLicensed k QUDType.antecedentFocused) : exp3Rate k < exp3Rate BaleEtAl2025.SpeakerKnowledge.fullKnowledge

Experiment 3 (antecedent-focused QUD): the unlicensed knowledge condition shows less perfection than the licensed one.

theorem EvcenBaleBarner2026.exp2_above_chance (a : AnswerType) : 1 / 2 < exp2Rate a

Experiment 2: both answer forms occur under licensed conditions, and both perfect above chance.

The three-button scenario

inductive EvcenBaleBarner2026.Button : Type

The three buttons of the experimental paradigm.

• A : Button
• B : Button
• C : Button

@[instance_reducible]

instance EvcenBaleBarner2026.instDecidableEqButton : DecidableEq Button

Equations

• EvcenBaleBarner2026.instDecidableEqButton x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive EvcenBaleBarner2026.ButtonWorld : Type

Worlds of the paradigm: one button is pressed, and the target sound plays or stays silent.

• pressA_plays : ButtonWorld
• pressA_silent : ButtonWorld
• pressB_plays : ButtonWorld
• pressB_silent : ButtonWorld
• pressC_plays : ButtonWorld
• pressC_silent : ButtonWorld

@[instance_reducible]

instance EvcenBaleBarner2026.instDecidableEqButtonWorld : DecidableEq ButtonWorld

Equations

• EvcenBaleBarner2026.instDecidableEqButtonWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def EvcenBaleBarner2026.pressA : Set ButtonWorld

Button A is pressed.

Equations

• EvcenBaleBarner2026.pressA = {EvcenBaleBarner2026.ButtonWorld.pressA_plays, EvcenBaleBarner2026.ButtonWorld.pressA_silent}

def EvcenBaleBarner2026.soundPlays : Set ButtonWorld

The target sound plays.

Equations

• EvcenBaleBarner2026.soundPlays = {EvcenBaleBarner2026.ButtonWorld.pressA_plays, EvcenBaleBarner2026.ButtonWorld.pressB_plays, EvcenBaleBarner2026.ButtonWorld.pressC_plays}

def EvcenBaleBarner2026.causes : Button → Set ButtonWorld

Button b causes the target sound: b is pressed and the sound plays.

Equations

• EvcenBaleBarner2026.causes EvcenBaleBarner2026.Button.A = {EvcenBaleBarner2026.ButtonWorld.pressA_plays}
• EvcenBaleBarner2026.causes EvcenBaleBarner2026.Button.B = {EvcenBaleBarner2026.ButtonWorld.pressB_plays}
• EvcenBaleBarner2026.causes EvcenBaleBarner2026.Button.C = {EvcenBaleBarner2026.ButtonWorld.pressC_plays}

def EvcenBaleBarner2026.buttons : Set Button

All three buttons are salient triggers.

Equations

• EvcenBaleBarner2026.buttons = {EvcenBaleBarner2026.Button.A, EvcenBaleBarner2026.Button.B, EvcenBaleBarner2026.Button.C}

theorem EvcenBaleBarner2026.causes_A_subset_pressA : causes Button.A ⊆ pressA

Button A causes the sound only if button A is pressed.

theorem EvcenBaleBarner2026.coverage {w : ButtonWorld} (hw : w ∈ soundPlays) : ∃ b ∈ buttons, w ∈ causes b

Coverage: every world where the sound plays has a button causing it.

theorem EvcenBaleBarner2026.alt_isInnocentlyExcludable {b : Button} (hb : b ∈ buttons) (hne : b ≠ Button.A) : Exhaustification.IsInnocentlyExcludable (VonFintel2001.answerAlternatives causes buttons Button.A) (causes Button.A) (causes b)

Every alternative button's answer is innocently excludable: at pressA_plays, A's answer holds while both alternatives fail.

theorem EvcenBaleBarner2026.perfection_of_exhaustifiedAnswer {w : ButtonWorld} (h_exh : w ∈ VonFintel2001.exhaustifiedAnswer causes buttons Button.A) : w ∈ Semantics.Conditionals.conditionalPerfection pressA soundPlays

Theory chain: exhaustifying Mary's answer "button A plays the sound" yields conditional perfection — if A is not pressed, the sound does not play.

theorem EvcenBaleBarner2026.perfection_of_exclusion {w : ButtonWorld} (hB : w ∉ causes Button.B) (hC : w ∉ causes Button.C) : w ∈ Semantics.Conditionals.conditionalPerfection pressA soundPlays

The participant's inference: granting exclusion of the other buttons, a world where A is unpressed is a world without the sound.

Per-trigger vs existential exclusion

def EvcenBaleBarner2026.vonFintelPrediction {ι : Type u_1} {W : Type u_2} (causes : ι → Set W) (triggers : Set ι) (t : ι) (w : W) : Prop

[vF01]-style prediction: every alternative salient trigger is excluded.

Equations

• EvcenBaleBarner2026.vonFintelPrediction causes triggers t w = ∀ t' ∈ triggers, t' ≠ t → w ∉ causes t'

def EvcenBaleBarner2026.hornPrediction {ι : Type u_1} {W : Type u_2} (causes : ι → Set W) (triggers : Set ι) (t : ι) (w : W) : Prop

[Hor00]-style prediction: some alternative salient trigger is excluded, with no commitment to which.

Equations

• EvcenBaleBarner2026.hornPrediction causes triggers t w = ∃ t' ∈ triggers, t' ≠ t ∧ w ∉ causes t'

theorem EvcenBaleBarner2026.vonFintel_entails_horn {ι : Type u_1} {W : Type u_2} {causes : ι → Set W} {triggers : Set ι} {t : ι} {w : W} (h_other : ∃ t' ∈ triggers, t' ≠ t) (h_vf : vonFintelPrediction causes triggers t w) : hornPrediction causes triggers t w

Per-trigger exclusion implies existential exclusion.

theorem EvcenBaleBarner2026.horn_not_entails_vonFintel : ∃ (w : ButtonWorld), hornPrediction causes buttons Button.A w ∧ ¬vonFintelPrediction causes buttons Button.A w

At pressB_plays, Horn's existential holds (button C is excluded) but von Fintel's universal fails (button B does cause the sound): per-trigger exclusion is strictly stronger, and participants' "No" responses to specific other buttons require it.