Conditional Perfection via Answer-Level Exhaustification

@cite{cornulier-1983} @cite{evcen-bale-barner-2026} @cite{groenendijk-stokhof-1984} @cite{von-fintel-2001} @cite{geis-zwicky-1971}

Formalizes the connection between conditional perfection and speech-act level exhaustification, following @cite{von-fintel-2001} "Conditional strengthening."

Key Insight

Propositional-level exhaustification of the material conditional does NOT yield perfection: EXH(¬A∨C, {¬B∨C}) = (¬A∨C) ∧ B ∧ ¬C — a specific world, not ¬A→¬C. Instead, conditional perfection arises from answer-level exhaustification: the answer "A causes C" is exhaustified against the alternative "B causes C," yielding "only A causes C." Combined with a coverage assumption (every C-event has some trigger), this entails ¬A→¬C.

This is @cite{von-fintel-2001}'s reconstruction of @cite{cornulier-1983}: when the QUD asks for sufficient conditions for C (antecedent-focus), the conditional answer triggers exhaustification over alternative antecedents. @cite{evcen-bale-barner-2026} experimentally validate this prediction.

structure Semantics.Conditionals.Exhaustivity.AnswerSpace (Trigger : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

An answer space for conditional perfection scenarios.

In a conditional perfection scenario, there is a set of potential triggers (antecedents) and a causal relation saying which trigger is active at which world. The key QUD is "which trigger causes C?" and the answer "trigger t causes C" has alternatives "trigger t' causes C" for each other trigger t'.

This models @cite{von-fintel-2001}'s analysis: the relevant alternatives are not propositional alternatives to the conditional, but alternative answers to the question "under which conditions does C hold?"

• causes : Trigger → W → Prop

  Which trigger is active at which world

• triggers : Set Trigger

  The set of contextually relevant triggers

def Semantics.Conditionals.Exhaustivity.answerProp {Trigger : Type u_1} {W : Type u_2} (as : AnswerSpace Trigger W) (t : Trigger) : Prop' W

The proposition "trigger t causes C (at world w)." This is the answer to the antecedent-focus QUD for trigger t.

Equations

• Semantics.Conditionals.Exhaustivity.answerProp as t w = as.causes t w

def Semantics.Conditionals.Exhaustivity.answerAlternatives {Trigger : Type u_1} {W : Type u_2} (as : AnswerSpace Trigger W) (t : Trigger) : Set (Prop' W)

The set of alternative answers: {"t' causes C" | t' ∈ triggers, t' ≠ t}. These are the answers that compete with "t causes C" under exhaustification.

Equations

• Semantics.Conditionals.Exhaustivity.answerAlternatives as t = {p : Prop' W | ∃ t' ∈ as.triggers, t' ≠ t ∧ p = Semantics.Conditionals.Exhaustivity.answerProp as t'}

def Semantics.Conditionals.Exhaustivity.antecedentFocusQUD {Trigger : Type u_1} {W : Type u_2} [DecidableEq Trigger] (activeTrigger : W → Option Trigger) : QUD W

Antecedent-focus QUD: partitions worlds by which trigger is active.

Under this QUD, asserting "t causes C" invites exhaustification against alternative triggers, following @cite{groenendijk-stokhof-1984} theory of exhaustive answers applied to conditionals.

Equations

• Semantics.Conditionals.Exhaustivity.antecedentFocusQUD activeTrigger = QUD.ofDecEq activeTrigger "antecedent-focus"

def Semantics.Conditionals.Exhaustivity.consequentFocusQUD {Effect : Type u_1} {W : Type u_2} [DecidableEq Effect] (activeEffect : W → Option Effect) : QUD W

Consequent-focus QUD: partitions worlds by what effect obtains.

Under this QUD, the answer lists consequences of a given antecedent. No exhaustification over alternative antecedents occurs, so no perfection.

Equations

• Semantics.Conditionals.Exhaustivity.consequentFocusQUD activeEffect = QUD.ofDecEq activeEffect "consequent-focus"

def Semantics.Conditionals.Exhaustivity.exhaustifiedAnswer {Trigger : Type u_1} {W : Type u_2} (as : AnswerSpace Trigger W) (t : Trigger) : Prop' W

The exhaustified answer: assert "t causes C" and innocently exclude all alternative triggers.

This is exhIE from @cite{spector-2016} applied at the answer level rather than the propositional level — the key move that makes exhaustification yield perfection rather than a contradictory specific world.

At the propositional level, EXH(¬A∨C, {¬B∨C}) gives A ∧ B ∧ ¬C. At the answer level, EXH("A causes C", {"B causes C"}) gives "A causes C and B does not cause C" — which with coverage yields perfection.

Equations

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

theorem Semantics.Conditionals.Exhaustivity.perfection_from_exclusion_and_coverage {W : Type u_1} {Trigger : Type u_2} (causes : Trigger → W → Prop) (triggers : Set Trigger) (t : Trigger) (_ht : t ∈ triggers) (p C : W → Prop) (h_t_requires_p : ∀ (w : W), causes t w → p w) (h_exclusion : ∀ t' ∈ triggers, t' ≠ t → ∀ (w : W), ¬causes t' w) (h_coverage : ∀ (w : W), C w → ∃ t' ∈ triggers, causes t' w) (w : W) (hnp : ¬p w) : ¬C w

Conditional perfection from exclusion and coverage.

If:

• trigger t requires precondition p (t-worlds are p-worlds),
• all other triggers are excluded (exhaustification),
• every C-event has some trigger (coverage/closure),

then ¬p → ¬C.

This is the core logical step underlying @cite{von-fintel-2001}'s analysis: exhaustification provides exclusion (only t causes C), the QUD-driven coverage assumption closes the gap to perfection (every C has a cause, the only cause requires p, so ¬p → ¬C).

The proof is purely structural (no sorry, no native_decide).

theorem Semantics.Conditionals.Exhaustivity.AnswerSpace.perfection {Trigger : Type u_1} {W : Type u_2} (as : AnswerSpace Trigger W) (t : Trigger) (ht : t ∈ as.triggers) (p C : W → Prop) (h_t_requires_p : ∀ (w : W), as.causes t w → p w) (h_exclusion : ∀ t' ∈ as.triggers, t' ≠ t → ∀ (w : W), ¬as.causes t' w) (h_coverage : ∀ (w : W), C w → ∃ t' ∈ as.triggers, as.causes t' w) (w : W) (hnp : ¬p w) : ¬C w

Perfection from an answer space with exclusion and coverage.

Connects the AnswerSpace abstraction to the general perfection theorem. When the exhaustified answer excludes all alternative triggers (exclusion) and every instance of C has some trigger (coverage), precondition failure entails consequent failure: ¬p → ¬C.

theorem Semantics.Conditionals.Exhaustivity.exhaustifiedAnswer_excludes {Trigger : Type u_1} {W : Type u_2} (as : AnswerSpace Trigger W) (t t' : Trigger) (w : W) (h_exh : exhaustifiedAnswer as t w) (h_ie : Exhaustification.isInnocentlyExcludable (answerAlternatives as t) (answerProp as t) (answerProp as t')) : ¬as.causes t' w

Exhaustification excludes innocently excludable alternatives.

If the exhaustified answer holds at world w and alternative trigger t' is innocently excludable (its negation belongs to every MC-set), then t' does not cause C at w.

This is the key connecting lemma: it bridges exhIE to the exclusion hypothesis in perfection_from_exclusion_and_coverage. Without it, exhaustifiedAnswer and the perfection theorem are disconnected definitions.

theorem Semantics.Conditionals.Exhaustivity.exhaustification_yields_perfection {Trigger : Type u_1} {W : Type u_2} (as : AnswerSpace Trigger W) (t : Trigger) (p C : W → Prop) (w : W) (h_t_requires_p : ∀ (w : W), as.causes t w → p w) (h_all_ie : ∀ t' ∈ as.triggers, t' ≠ t → Exhaustification.isInnocentlyExcludable (answerAlternatives as t) (answerProp as t) (answerProp as t')) (h_coverage : C w → ∃ t' ∈ as.triggers, as.causes t' w) (h_exh : exhaustifiedAnswer as t w) (hnp : ¬p w) : ¬C w

Full prediction chain: exhaustification → perfection.

This is the genuine dependency chain from theory to prediction:

1. exhaustifiedAnswer as t w holds (speaker asserts under antecedent-focus QUD)
2. All alternative triggers are innocently excludable (h_all_ie)
3. Every C-event has some trigger (h_coverage)
4. Trigger t requires precondition p (h_t_requires_p)
5. Therefore: ¬p w → ¬C w

Steps 1–2 yield local exclusion at w (via exhaustifiedAnswer_excludes). Step 3 is the coverage/closure assumption driven by the QUD. The conclusion follows by perfection_from_exclusion_and_coverage.

This theorem closes the gap between the exhaustification mechanism (exhIE) and the perfection result. Without it, the theory has two disconnected pieces: the definition of exhaustified answers and the perfection theorem, with no proof that the former provides the exclusion the latter requires.

theorem Semantics.Conditionals.Exhaustivity.singleton_alt_innocently_excludable {World : Type u_1} (ALT : Set (Prop' World)) (φ a : Prop' World) (h_mem : a ∈ ALT) (h_all_eq : ∀ a' ∈ ALT, a' = a) (h_consist : ∃ (w : World), φ w ∧ ¬a w) : Exhaustification.isInnocentlyExcludable ALT φ a

Singleton alternatives are innocently excludable.

When the alternative set effectively contains a single proposition a (every member equals a) and the assertion φ is jointly satisfiable with ¬a, then a is innocently excludable.

Proof sketch: Any MC-set E ⊆ {φ, ∼a} (by compatibility, every element is φ or ∼a' for a' ∈ ALT, and all a' = a). The set {φ, ∼a} is itself compatible (consistency from h_consist). By maximality of E with E ⊆ {φ, ∼a}: {φ, ∼a} ⊆ E. Hence ∼a ∈ E for every MC-set E.

This closes the gap between the abstract IE machinery and concrete scenarios with a single competing alternative — the typical case in conditional perfection with two triggers.

theorem Semantics.Conditionals.Exhaustivity.all_alt_innocently_excludable {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (h_consist : ∃ (w : World), φ w ∧ ∀ a ∈ ALT, ¬a w) (a : Prop' World) : a ∈ ALT → Exhaustification.isInnocentlyExcludable ALT φ a

All alternatives are innocently excludable when full exclusion is consistent.

When there exists a world where φ holds and every alternative in ALT is false, every alternative is innocently excludable. This generalizes singleton_alt_innocently_excludable from singleton to arbitrary ALT.

Proof: The set S = {φ} ∪ {∼a | a ∈ ALT} is the unique MC-set: it is compatible by hypothesis, and every compatible set is a subset of it (by the compatibility constraint, every element is φ or ∼a for some a ∈ ALT). By maximality, every MC-set equals S. Since ∼a ∈ S for all a ∈ ALT, every alternative is in IE.

This covers conditional perfection scenarios with any number of alternative triggers — e.g., 3 buttons in @cite{evcen-bale-barner-2026}'s experimental paradigm.