von Fintel (2001): Conditional Strengthening

This file formalizes [vF01]'s account of the strengthening of conditionals beyond their truth conditions. A conditional if p, q is a restricted universal over the relevant situations (5), Conditional.strictImp, and the conditional perfection of [GZ71], if not p, not q, is not entailed. The paper argues with [Lil72] that perfection does not arise routinely, but a weaker strengthening does: by the quantity reasoning [Gam91] formalizes as correct use (12), CorrectUse, the assertion of if p, q competes with the stronger q no matter what (14), universal quantification over antecedents that reduces to q throughout the relevant situations, so the speaker is taken not to believe that q holds unconditionally, an implicature which, against [Hor00], falls short of perfection. True perfection arises by the presumption of exhaustivity of [dC83], the exclusion of if p or r, q for the alternative antecedents r: over all alternatives not entailing p this is perfection, over a narrower set only the relativized perfection of (18). What makes the exclusion required is the exhaustive interpretation of answers of [GS84]: a conditional asserted as the answer to under which conditions does q hold? is exhaustified against the answers naming the alternative antecedents (exhaustifiedAnswer), which yields a typology of cases without perfection, among them the yes/no conditional question, whose answer has no alternative to exclude.

Implementation notes

Situations are worlds and the relevant situations are given by an accessibility function. Belief and relevance are predicates on propositions, so an implicature is what every correct use of the sentence carries, and the step from not believing a proposition to believing its negation is an explicit opinionatedness hypothesis. The exclusion of the alternative answers is the innocent-exclusion operator exhIE, over alternatives indexed by their antecedents. The monotonicity condition on scales of [Mat95] and the semantic exhaustivity of Groenendijk and Stokhof are not formalized.

References

• [vF01]
• [GZ71]
• [Lil72]
• [Gam91]
• [Hor00]
• [dC83]
• [GS84]
• [Mat95]

Conditionals and perfection

def VonFintel2001.perfection {W : Type u_1} (acc : W → Set W) (p q : Set W) : Set W

Perfection, if not p, not q, says that no relevant situation outside p is a q-situation.

Equations

• VonFintel2001.perfection acc p q = Conditional.strictImp acc pᶜ qᶜ

theorem VonFintel2001.mem_perfection {W : Type u_1} {acc : W → Set W} {p q : Set W} {s : W} : s ∈ perfection acc p q ↔ ∀ s' ∈ acc s, s' ∉ p → s' ∉ q

Quantity implicatures (12), (13)

structure VonFintel2001.CorrectUse {W : Type u_1} (bel rel : Set W → Prop) (A : Set W) : Prop

Gamut's conditions of correct use (12) require that the speaker believes the sentence, holds it relevant, and believes and holds relevant no strictly stronger sentence.

• believes : bel A
• relevant : rel A
• quantity (B : Set W) : B ⊂ A → ¬(bel B ∧ rel B)

def VonFintel2001.Implicature {W : Type u_1} (rel : Set W → Prop) (A : Set W) (P : (Set W → Prop) → Prop) : Prop

P is an implicature of A when it follows from the conditions of correct use, whatever the speaker's beliefs (13).

Equations

• VonFintel2001.Implicature rel A P = ∀ (bel : Set W → Prop), VonFintel2001.CorrectUse bel rel A → P bel

theorem VonFintel2001.implicature_not_bel {W : Type u_1} {rel : Set W → Prop} {A B : Set W} (hB : B ⊂ A) (hrel : rel B) : Implicature rel A fun (bel : Set W → Prop) => ¬bel B

A relevant proposition strictly stronger than the assertion is implicated not to be believed.

theorem VonFintel2001.bel_compl_of_correctUse {W : Type u_1} {bel rel : Set W → Prop} {A B : Set W} (h : CorrectUse bel rel A) (hB : B ⊂ A) (hrel : rel B) (hop : bel B ∨ bel Bᶜ) : bel Bᶜ

An opinionated speaker is taken to believe the negation of the stronger proposition, the further step of Mill's reasoning.

q no matter what (14), (15)

def VonFintel2001.noMatterWhat {W : Type u_1} (acc : W → Set W) (q : Set W) : Set W

q no matter what says that every antecedent conditionally yields q (14).

Equations

• VonFintel2001.noMatterWhat acc q = ⋂ (r : Set W), Conditional.strictImp acc r q

theorem VonFintel2001.mem_noMatterWhat {W : Type u_1} {acc : W → Set W} {q : Set W} {s : W} : s ∈ noMatterWhat acc q ↔ acc s ⊆ q

q no matter what is q throughout the relevant situations (15).

theorem VonFintel2001.noMatterWhat_subset_strictImp {W : Type u_1} {acc : W → Set W} {p q : Set W} : noMatterWhat acc q ⊆ Conditional.strictImp acc p q

q no matter what entails if p, q, the stronger alternative of the quantity reasoning.

theorem VonFintel2001.implicature_not_noMatterWhat {W : Type u_1} {acc : W → Set W} {p q : Set W} {rel : Set W → Prop} (hlt : noMatterWhat acc q ⊂ Conditional.strictImp acc p q) (hrel : rel (noMatterWhat acc q)) : Implicature rel (Conditional.strictImp acc p q) fun (bel : Set W → Prop) => ¬bel (noMatterWhat acc q)

Correct use of if p, q, with the unconditional claim relevant and strictly stronger, implicates that the speaker does not believe q holds no matter what.

theorem VonFintel2001.exists_not_noMatterWhat_not_perfection : ∃ (acc : Fin 3 → Set (Fin 3)) (p : Set (Fin 3)) (q : Set (Fin 3)), ∃ s ∈ Conditional.strictImp acc p q, s ∉ noMatterWhat acc q ∧ s ∉ perfection acc p q

Against [Hor00], the negation of q no matter what is not perfection. With a relevant q-situation outside p and a relevant situation outside q, if p, q holds, q no matter what fails, and perfection fails.

The road to true perfection

theorem VonFintel2001.strictImp_union_subset {W : Type u_1} {acc : W → Set W} {p q r : Set W} : Conditional.strictImp acc (p ∪ r) q ⊆ Conditional.strictImp acc p q

If p or r, q is stronger than if p, q, by the downward monotonicity of the universal.

theorem VonFintel2001.exists_of_not_mem_strictImp_union {W : Type u_1} {acc : W → Set W} {p q r : Set W} {s : W} (h : s ∈ Conditional.strictImp acc p q) (h' : s ∉ Conditional.strictImp acc (p ∪ r) q) : ∃ s' ∈ acc s, s' ∈ r ∧ s' ∉ q

The implicature for one alternative antecedent says that some relevant r-situation is not a q-situation.

theorem VonFintel2001.perfection_of_forall {W : Type u_1} {acc : W → Set W} {p q : Set W} {s : W} (h : ∀ (r : Set W), ¬r ⊆ p → s ∉ Conditional.strictImp acc r q) : s ∈ perfection acc p q

Excluding if r, q for every antecedent r not entailing p is perfection (7).

theorem VonFintel2001.exists_relativized_not_perfection : ∃ (acc : Fin 3 → Set (Fin 3)) (p : Set (Fin 3)) (q : Set (Fin 3)) (R : Set (Set (Fin 3))), ∃ s ∈ Conditional.strictImp acc p q, (∀ r ∈ R, ¬r ⊆ p → s ∉ Conditional.strictImp acc r q) ∧ s ∉ perfection acc p q

Relativized perfection (18), excluding the alternatives of a narrower set of antecedents, falls short of perfection. Situation 0 is a call after midnight, 1 a polite call before midnight and 2 an insulting one; excluding if you call before midnight, I will be upset leaves the insult upsetting.

Exhaustive answers

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

The answers competing with "antecedent t yields the consequent" are the answers for the other antecedents in triggers.

Equations

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

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

The exhaustified answer is "antecedent t yields the consequent" with the other antecedents' answers innocently excluded.

Equations

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

@[simp]

theorem VonFintel2001.mem_answerAlternatives {W : Type u_1} {ι : 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.exhaustifiedAnswer_excludes {W : Type u_1} {ι : Type u_2} {s : W} {causes : ι → Set W} {triggers : Set ι} {t t' : ι} (h_exh : s ∈ exhaustifiedAnswer causes triggers t) (h_ie : Exhaustification.IsInnocentlyExcludable (answerAlternatives causes triggers t) (causes t) (causes t')) : s ∉ causes t'

The exhaustified answer excludes each innocently excludable alternative.

def VonFintel2001.conditionalAnswer {W : Type u_1} (acc : W → Set W) (R : Set (Set W)) (p q : Set W) : Set W

The conditional if p, q asserted as the answer to under which conditions does q hold? over the antecedents R.

Equations

• VonFintel2001.conditionalAnswer acc R p q = VonFintel2001.exhaustifiedAnswer (fun (r : Set W) => Conditional.strictImp acc r q) R p

theorem VonFintel2001.perfection_of_conditionalAnswer {W : Type u_1} {acc : W → Set W} {p q : Set W} {s : W} {R : Set (Set W)} (h : s ∈ conditionalAnswer acc R p q) (hie : ∀ r ∈ R, r ≠ p → Exhaustification.IsInnocentlyExcludable (answerAlternatives (fun (r : Set W) => Conditional.strictImp acc r q) R p) (Conditional.strictImp acc p q) (Conditional.strictImp acc r q)) (hR : ∀ s' ∈ acc s, {s'} ∈ R) : s ∈ perfection acc p q

Over all antecedents the exhaustified conditional answer is perfection, since, every alternative being innocently excludable, the singleton antecedents of the relevant situations suffice.

theorem VonFintel2001.conditionalAnswer_singleton {W : Type u_1} {acc : W → Set W} {p q : Set W} : conditionalAnswer acc {p} p q = Conditional.strictImp acc p q

A yes/no conditional question offers no alternative antecedent, so the answer is the plain conditional and exhaustivity applies vacuously.