von Fintel (2001): Conditional Strengthening

[vF01] derives conditional perfection ([GZ71]) from answer-level exhaustivity, reconstructing [dC83]'s "presumption of exhaustivity" via [GS84]'s exhaustive answers: a conditional asserted as the answer to "under which conditions does C hold?" is exhaustified against the answers naming alternative triggers. Exhaustification excludes the alternative triggers; when the salient triggers cover every route to C, the strengthened answer yields conditionalPerfection. When they cover only a narrower set, the coverage premise fails and only relativized perfection arises (the paper's after-midnight example).

The paper runs the exclusion step as a Gamut-style quantity implicature; here it is the project-canonical innocent-exclusion operator exhIE ([Spe16]).

Main results

• exhaustifiedAnswer: exhIE at the answer level — the answer "trigger t causes C" with the alternative triggers' answers excluded.
• exhaustification_yields_perfection: if the alternative answers are innocently excludable and the salient triggers cover C, the exhaustified answer entails conditionalPerfection.

def VonFintel2001.answerAlternatives {ι : Type u_1} {W : Type u_2} (causes : ι → Set W) (triggers : Set ι) (t : ι) : Set (Set W)

The answers competing with "trigger t causes C": causes t' for the other salient triggers t'.

Equations

• VonFintel2001.answerAlternatives causes triggers t = causes '' (triggers \ {t})

def VonFintel2001.exhaustifiedAnswer {ι : Type u_1} {W : Type u_2} (causes : ι → Set W) (triggers : Set ι) (t : ι) : Set W

The exhaustified answer: assert "trigger t causes C" and innocently exclude the alternative triggers' answers.

Equations

• VonFintel2001.exhaustifiedAnswer causes triggers t = Exhaustification.exhIE (VonFintel2001.answerAlternatives causes triggers t) (causes t)

@[simp]

theorem VonFintel2001.mem_answerAlternatives {ι : Type u_1} {W : Type u_2} {causes : ι → Set W} {triggers : Set ι} {t : ι} {q : Set W} : q ∈ answerAlternatives causes triggers t ↔ ∃ t' ∈ triggers, t' ≠ t ∧ causes t' = q

theorem VonFintel2001.perfection_from_exclusion_and_coverage {ι : Type u_1} {W : Type u_2} {causes : ι → Set W} {triggers : Set ι} {t : ι} {p C : Set W} {w : W} (h_req : w ∈ causes t → w ∈ p) (h_excl : ∀ t' ∈ triggers, t' ≠ t → w ∉ causes t') (h_cov : w ∈ C → ∃ t' ∈ triggers, w ∈ causes t') : w ∈ Semantics.Conditionals.conditionalPerfection p C

Exclusion and coverage entail perfection: if trigger t requires p, no alternative salient trigger causes C at w, and every C-world has a salient trigger, then w ∈ conditionalPerfection p C.

theorem VonFintel2001.exhaustifiedAnswer_excludes {ι : Type u_1} {W : Type u_2} {causes : ι → Set W} {triggers : Set ι} {t t' : ι} {w : W} (h_exh : w ∈ exhaustifiedAnswer causes triggers t) (h_ie : Exhaustification.IsInnocentlyExcludable (answerAlternatives causes triggers t) (causes t) (causes t')) : w ∉ causes t'

The exhaustified answer excludes each innocently excludable alternative trigger at the world of evaluation.

theorem VonFintel2001.exhaustification_yields_perfection {ι : Type u_1} {W : Type u_2} {causes : ι → Set W} {triggers : Set ι} {t : ι} {p C : Set W} {w : W} (h_req : causes t ⊆ p) (h_ie : ∀ t' ∈ triggers, t' ≠ t → Exhaustification.IsInnocentlyExcludable (answerAlternatives causes triggers t) (causes t) (causes t')) (h_cov : w ∈ C → ∃ t' ∈ triggers, w ∈ causes t') (h_exh : w ∈ exhaustifiedAnswer causes triggers t) : w ∈ Semantics.Conditionals.conditionalPerfection p C

Answer-level exhaustification yields perfection: if trigger t requires p, every alternative salient trigger's answer is innocently excludable, and the salient triggers cover C, then the exhaustified answer entails conditionalPerfection p C.

theorem VonFintel2001.coverage_without_exclusion_insufficient : ∃ (W : Type) (ι : Type) (causes : ι → Set W) (triggers : Set ι) (t : ι) (p : Set W) (C : Set W) (w : W), t ∈ triggers ∧ causes t ⊆ p ∧ (∀ w ∈ C, ∃ t' ∈ triggers, w ∈ causes t') ∧ w ∉ Semantics.Conditionals.conditionalPerfection p C

Exclusion is essential: requirement and coverage alone do not yield perfection. Witness: a second salient trigger fires at a world outside p, so the paper's counterexample typology (a QUD that does not elicit an exhaustive list of sufficient conditions) predicts no perfection.