Alonso-Ovalle (2009): counterfactuals, correlatives, and disjunction

A would-counterfactual with a disjunctive antecedent is read as checking the consequent in the closest worlds of each disjunct, which a minimal-change semantics with Boolean or cannot do: on the bumper-crop scenario (1) it hands the modal the union and predicts the counterfactual true (bumperCrop_boolean). The paper keeps minimal change and instead lets or introduce its disjuncts as Hamblin alternatives (10) and treats conditionals as correlatives: the if-clause universally quantifies over the alternatives (25) and the consequent, abstracted over the propositional anaphor then, supplies the modal (24). The composition is distributiveImp for would and DistributiveMight for might; it validates Simplification (27), makes (1) false (bumperCrop_alternatives), and leaves the negated (29) true when one simplification holds, where a sum with the homogeneity presupposition (33) gives a gap (hitler_negation, homogeneity_ne_false).

Rival derivations fail. A strict conditional makes Simplification a monotonicity inference (strict_simplification) but not for the dual might (strictMight_not_simplifying), and Stalnaker's ◇(would) recovers it (stalnaker_might_simplification) only for epistemic modals. On von Fintel's modal horizon (44)–(45), Simplification is Strawson-valid like Strengthening the Antecedent (horizonWould_anti) but not dynamically valid (horizon_sunCold_undefined). The manner implicature (75)–(76) does not deliver both simplifications (manner_insufficient). Nute's (80) is a contradiction unless a disjunct is impossible (distributive_pair_disjoint_iff) and needs Existential Closure (82) (budget). The paper's verdicts are checked in rows_agree.

References

• [AO09]
• [Lew73b]
• [McKVI77]
• [Nut75]
• [Ham73]
• [Day96]
• [vF00a]
• [vF99a]
• [Sta84]
• [Ben03]
• [Lew77]

Conditionals as correlatives (§2)

def AlonsoOvalle2009.DistributiveMight {W : Type u_1} (ord : W → Preorder W) (S : Finset (Finset W)) (C : Set W) (w : W) : Prop

Might in the consequent (70)–(71) under the universal if-clause (25) holds when the closest worlds of every alternative are compatible with the consequent.

Equations

• AlonsoOvalle2009.DistributiveMight ord S C w = ∀ A ∈ S, w ∈ Conditional.might (Conditional.closestImp ord) (↑A) C

@[instance_reducible]

instance AlonsoOvalle2009.instDecidableDistributiveMight {W : Type u_1} (ord : W → Preorder W) (S : Finset (Finset W)) (C : Set W) (w : W) [DecidableEq W] [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ C] : Decidable (DistributiveMight ord S C w)

Equations

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

theorem AlonsoOvalle2009.simplification {W : Type u_1} (ord : W → Preorder W) (C : Set W) (w : W) [DecidableEq W] {A B : Finset W} (h : w ∈ Conditional.distributiveImp ord {A, B} C) : w ∈ Conditional.closestImp ord (↑A) C ∧ w ∈ Conditional.closestImp ord (↑B) C

Simplification (27) says that the disjunctive counterfactual entails each disjunct's.

theorem AlonsoOvalle2009.simplification_might {W : Type u_1} (ord : W → Preorder W) (C : Set W) (w : W) [DecidableEq W] {A B : Finset W} (h : DistributiveMight ord {A, B} C w) : w ∈ Conditional.might (Conditional.closestImp ord) (↑A) C ∧ w ∈ Conditional.might (Conditional.closestImp ord) (↑B) C

Simplification for might (54), the extension of §3.3.

@[reducible, inline]

abbrev AlonsoOvalle2009.goodWeatherW : Finset McKayVanInwagen1977.CropWorld

The good-weather and cold-sun worlds of the bumper-crop model.

Equations

• AlonsoOvalle2009.goodWeatherW = {x : McKayVanInwagen1977.CropWorld | x ∈ McKayVanInwagen1977.goodWeather}

@[reducible, inline]

abbrev AlonsoOvalle2009.sunColdW : Finset McKayVanInwagen1977.CropWorld

Equations

• AlonsoOvalle2009.sunColdW = {x : McKayVanInwagen1977.CropWorld | x ∈ McKayVanInwagen1977.sunCold}

theorem AlonsoOvalle2009.bumperCrop_boolean : McKayVanInwagen1977.CropWorld.actual ∈ Conditional.disjunctiveImp McKayVanInwagen1977.cropSim {goodWeatherW, sunColdW} McKayVanInwagen1977.bumperCrop

Boolean or (6) hands the modal the union, and (1) comes out true (Fig. 1).

theorem AlonsoOvalle2009.bumperCrop_alternatives : McKayVanInwagen1977.CropWorld.actual ∉ Conditional.distributiveImp McKayVanInwagen1977.cropSim {goodWeatherW, sunColdW} McKayVanInwagen1977.bumperCrop

With the disjuncts as alternatives (13) under universal force (26), (1) is false, since the closest cold-sun worlds have no crop.

Universal quantifier or sum (§2.2.3)

theorem AlonsoOvalle2009.homogeneity_ne_false {W : Type u_1} (ord : W → Preorder W) (S : Finset (Finset W)) (C : Set W) (w : W) [DecidableEq W] [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ C] {A : Finset W} (hA : A ∈ S) (h : w ∈ Conditional.closestImp ord (↑A) C) : Conditional.homogeneousImp ord S C w ≠ -1

A sum analysis falsifies a disjunctive counterfactual only when every disjunct's counterfactual fails.

inductive AlonsoOvalle2009.HitlerWorld : Type

In (29)–(31) Spain joining Germany is closer than Spain joining the U.S., and Hitler is pleased only in the former.

• actual : HitlerWorld
• germany : HitlerWorld
• us : HitlerWorld

@[instance_reducible]

instance AlonsoOvalle2009.instDecidableEqHitlerWorld : DecidableEq HitlerWorld

Equations

• AlonsoOvalle2009.instDecidableEqHitlerWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalle2009.instFintypeHitlerWorld : Fintype HitlerWorld

Equations

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

def AlonsoOvalle2009.HitlerWorld.rank : HitlerWorld → ℕ

Equations

• AlonsoOvalle2009.HitlerWorld.actual.rank = 0
• AlonsoOvalle2009.HitlerWorld.germany.rank = 1
• AlonsoOvalle2009.HitlerWorld.us.rank = 2

@[reducible, inline]

abbrev AlonsoOvalle2009.hitlerSim : HitlerWorld → Preorder HitlerWorld

Equations

• AlonsoOvalle2009.hitlerSim x✝ = Preorder.lift AlonsoOvalle2009.HitlerWorld.rank

@[reducible, inline]

abbrev AlonsoOvalle2009.joinedGermany : Finset HitlerWorld

Equations

• AlonsoOvalle2009.joinedGermany = {AlonsoOvalle2009.HitlerWorld.germany}

@[reducible, inline]

abbrev AlonsoOvalle2009.joinedUS : Finset HitlerWorld

Equations

• AlonsoOvalle2009.joinedUS = {AlonsoOvalle2009.HitlerWorld.us}

@[reducible, inline]

abbrev AlonsoOvalle2009.pleased : Set HitlerWorld

Equations

• AlonsoOvalle2009.pleased = {AlonsoOvalle2009.HitlerWorld.germany}

theorem AlonsoOvalle2009.hitler_negation : HitlerWorld.actual ∉ Conditional.distributiveImp hitlerSim {joinedGermany, joinedUS} pleased ∧ HitlerWorld.actual ∈ Conditional.closestImp hitlerSim (↑joinedGermany) pleased ∧ HitlerWorld.actual ∉ Conditional.closestImp hitlerSim (↑joinedUS) pleased ∧ Conditional.homogeneousImp hitlerSim {joinedGermany, joinedUS} pleased HitlerWorld.actual = 0

Under the universal quantifier (29) is true, with (30a) true and (30b) false as (31) continues; under a sum with homogeneity (33) it is a gap.

Downward entailingness (§3)

theorem AlonsoOvalle2009.strict_simplification {W : Type u_1} {I : Type u_2} (access : I → Set W) (φ ψ χ : Set W) {i : I} (h : i ∈ Conditional.strictImp access (φ ∪ ψ) χ) : i ∈ Conditional.strictImp access φ χ ∧ i ∈ Conditional.strictImp access ψ χ

A strict conditional is antitone in its antecedent, so Simplification is a monotonicity inference, (37)–(38).

theorem AlonsoOvalle2009.stalnaker_might_simplification {W : Type u_1} {I : Type u_2} (access : I → Set W) (φ ψ χ : Set W) (E : I → Set I) {i : I} (h : ∃ i' ∈ E i, i' ∈ Conditional.strictImp access (φ ∪ ψ) χ) : (∃ i' ∈ E i, i' ∈ Conditional.strictImp access φ χ) ∧ ∃ i' ∈ E i, i' ∈ Conditional.strictImp access ψ χ

Stalnaker's might counterfactual, epistemic possibility over E of the strict would, inherits Simplification, (60)–(64).

def AlonsoOvalle2009.expand {W : Type u_1} (ord : W → Preorder W) [DecidableEq W] [Fintype W] [(w : W) → DecidableRel LE.le] (f : W → Finset W) (φ : Finset W) (w : W) : Finset W

Accommodation (44) grows the modal horizon f by every world at least as close as the closest antecedent worlds.

Equations

• AlonsoOvalle2009.expand ord f φ w = f w ∪ {w' : W | ∀ w'' ∈ φ, w' ≤ w''}

def AlonsoOvalle2009.horizonWould {W : Type u_1} [DecidableEq W] (f : W → Finset W) (φ ψ : Finset W) (w : W) : Prop

The counterfactual on a horizon (45) holds when every antecedent world in the horizon is a consequent world.

Equations

• AlonsoOvalle2009.horizonWould f φ ψ w = ∀ w' ∈ f w ∩ φ, w' ∈ ψ

def AlonsoOvalle2009.HorizonReaches {W : Type u_1} [DecidableEq W] (f : W → Finset W) (φ : Finset W) (w : W) : Prop

The presupposition of (45) is that the horizon reaches the antecedent.

Equations

• AlonsoOvalle2009.HorizonReaches f φ w = (f w ∩ φ).Nonempty

@[instance_reducible]

instance AlonsoOvalle2009.instDecidableHorizonReaches {W : Type u_1} (w : W) [DecidableEq W] (f : W → Finset W) (φ : Finset W) : Decidable (HorizonReaches f φ w)

Equations

• AlonsoOvalle2009.instDecidableHorizonReaches w f φ = { decide := decide (∃ a ∈ f w ∩ φ, true = true), reflects_decide := ⋯ }

theorem AlonsoOvalle2009.horizonWould_anti {W : Type u_1} (w : W) [DecidableEq W] {f : W → Finset W} {φ φ' ψ : Finset W} (h : φ' ⊆ φ) (hw : horizonWould f φ ψ w) : horizonWould f φ' ψ w

Strengthening the Antecedent and Simplification alike are Strawson valid (50), since on a horizon that already reaches the stronger antecedent, (45) is antitone in it.

theorem AlonsoOvalle2009.horizon_sunCold_undefined : ¬HorizonReaches (expand McKayVanInwagen1977.cropSim (fun (w : McKayVanInwagen1977.CropWorld) => {w}) (goodWeatherW ∪ sunColdW)) sunColdW McKayVanInwagen1977.CropWorld.actual

Simplification is dynamically invalid (47), since accommodating (48)'s antecedent from the initial horizon reaches the good-weather world only, so (49b) is undefined.

Might counterfactuals (§3.2)

inductive AlonsoOvalle2009.ForkWorld : Type

In (51) having a magic book is closer than being a newborn baby, and the fork is bent in one of the closest magic-book worlds and in no newborn world (Fig. 2).

• actual : ForkWorld
• book : ForkWorld
• bookBent : ForkWorld
• baby : ForkWorld

@[instance_reducible]

instance AlonsoOvalle2009.instDecidableEqForkWorld : DecidableEq ForkWorld

Equations

• AlonsoOvalle2009.instDecidableEqForkWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalle2009.instFintypeForkWorld : Fintype ForkWorld

Equations

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

def AlonsoOvalle2009.ForkWorld.rank : ForkWorld → ℕ

Equations

• AlonsoOvalle2009.ForkWorld.actual.rank = 0
• AlonsoOvalle2009.ForkWorld.book.rank = 1
• AlonsoOvalle2009.ForkWorld.bookBent.rank = 1
• AlonsoOvalle2009.ForkWorld.baby.rank = 2

@[reducible, inline]

abbrev AlonsoOvalle2009.forkSim : ForkWorld → Preorder ForkWorld

Equations

• AlonsoOvalle2009.forkSim x✝ = Preorder.lift AlonsoOvalle2009.ForkWorld.rank

@[reducible, inline]

abbrev AlonsoOvalle2009.hasBook : Finset ForkWorld

Equations

• AlonsoOvalle2009.hasBook = {AlonsoOvalle2009.ForkWorld.book, AlonsoOvalle2009.ForkWorld.bookBent}

@[reducible, inline]

abbrev AlonsoOvalle2009.newborn : Finset ForkWorld

Equations

• AlonsoOvalle2009.newborn = {AlonsoOvalle2009.ForkWorld.baby}

@[reducible, inline]

abbrev AlonsoOvalle2009.bent : Set ForkWorld

Equations

• AlonsoOvalle2009.bent = {AlonsoOvalle2009.ForkWorld.bookBent}

theorem AlonsoOvalle2009.fork : ForkWorld.actual ∈ Conditional.might (Conditional.closestImp forkSim) (↑(hasBook ∪ newborn)) bent ∧ ¬DistributiveMight forkSim {hasBook, newborn} bent ForkWorld.actual ∧ ForkWorld.actual ∈ Conditional.might (Conditional.closestImp forkSim) (↑hasBook) bent ∧ ForkWorld.actual ∉ Conditional.might (Conditional.closestImp forkSim) (↑newborn) bent

Under (52)–(53) the closest worlds of the union are magic-book worlds, one of which bends the fork, so (51) is true; under the correlative analysis it is false, since (58a) is true but (58b) is not.

theorem AlonsoOvalle2009.strictMight_not_simplifying : (∃ w ∈ hasBook ∪ newborn, w ∈ bent) ∧ ¬∃ w ∈ newborn, w ∈ bent

The strict dual might, with every world accessible, is true of the disjunction but not of the newborn disjunct, (57)–(58).

An implicature? (§4)

inductive AlonsoOvalle2009.BeliefWorld : Type

Figures 3–4 have two worlds compatible with the speaker's beliefs; magic-book and newborn worlds are equally close to each, and the fork is bent in a closest magic-book world of the first and in a closest newborn world of the second.

• w₃ : BeliefWorld
• book₃ : BeliefWorld
• baby₃ : BeliefWorld
• w₄ : BeliefWorld
• book₄ : BeliefWorld
• baby₄ : BeliefWorld

@[instance_reducible]

instance AlonsoOvalle2009.instDecidableEqBeliefWorld : DecidableEq BeliefWorld

Equations

• AlonsoOvalle2009.instDecidableEqBeliefWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalle2009.instFintypeBeliefWorld : Fintype BeliefWorld

Equations

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

def AlonsoOvalle2009.BeliefWorld.rank : BeliefWorld → BeliefWorld → ℕ

Equations

• AlonsoOvalle2009.BeliefWorld.w₃.rank AlonsoOvalle2009.BeliefWorld.w₃ = 0
• AlonsoOvalle2009.BeliefWorld.w₄.rank AlonsoOvalle2009.BeliefWorld.w₄ = 0
• AlonsoOvalle2009.BeliefWorld.w₃.rank AlonsoOvalle2009.BeliefWorld.book₃ = 1
• AlonsoOvalle2009.BeliefWorld.w₃.rank AlonsoOvalle2009.BeliefWorld.baby₃ = 1
• AlonsoOvalle2009.BeliefWorld.w₄.rank AlonsoOvalle2009.BeliefWorld.book₄ = 1
• AlonsoOvalle2009.BeliefWorld.w₄.rank AlonsoOvalle2009.BeliefWorld.baby₄ = 1
• x✝¹.rank x✝ = 2

@[reducible, inline]

abbrev AlonsoOvalle2009.beliefSim (w₀ : BeliefWorld) : Preorder BeliefWorld

Equations

• AlonsoOvalle2009.beliefSim w₀ = Preorder.lift w₀.rank

@[reducible, inline]

abbrev AlonsoOvalle2009.belief : Finset BeliefWorld

Equations

• AlonsoOvalle2009.belief = {AlonsoOvalle2009.BeliefWorld.w₃, AlonsoOvalle2009.BeliefWorld.w₄}

@[reducible, inline]

abbrev AlonsoOvalle2009.bookB : Finset BeliefWorld

Equations

• AlonsoOvalle2009.bookB = {AlonsoOvalle2009.BeliefWorld.book₃, AlonsoOvalle2009.BeliefWorld.book₄}

@[reducible, inline]

abbrev AlonsoOvalle2009.babyB : Finset BeliefWorld

Equations

• AlonsoOvalle2009.babyB = {AlonsoOvalle2009.BeliefWorld.baby₃, AlonsoOvalle2009.BeliefWorld.baby₄}

@[reducible, inline]

abbrev AlonsoOvalle2009.bentB : Set BeliefWorld

Equations

• AlonsoOvalle2009.bentB = {AlonsoOvalle2009.BeliefWorld.book₃, AlonsoOvalle2009.BeliefWorld.baby₄}

theorem AlonsoOvalle2009.manner_insufficient : (∀ w ∈ belief, w ∈ Conditional.might (Conditional.closestImp beliefSim) (↑(bookB ∪ babyB)) bentB) ∧ (∃ w ∈ belief, w ∉ Conditional.might (Conditional.closestImp beliefSim) (↑bookB) bentB) ∧ (∃ w ∈ belief, w ∉ Conditional.might (Conditional.closestImp beliefSim) (↑babyB) bentB) ∧ ∀ w ∈ belief, ¬DistributiveMight beliefSim {bookB, babyB} bentB w

Manner (75)–(76) is satisfied — (73) holds throughout the belief state and neither (74a) nor (74b) does — yet the two simplifications hold together nowhere in it, so (77) is not predicted deviant.

The visibility of the disjuncts (§5.2)

theorem AlonsoOvalle2009.distributive_pair_disjoint_iff {W : Type u_1} (ord : W → Preorder W) (w : W) [DecidableEq W] {A B : Finset W} (h : Disjoint A B) : w ∈ Conditional.distributiveImp ord {A, B} ↑A ↔ B = ∅

On Nute's recipe (80), when the consequent is one of two incompatible disjuncts, the analysis makes the counterfactual true only if the other disjunct is impossible.

inductive AlonsoOvalle2009.BudgetWorld : Type

In (80) more defense spending is closer than more education spending.

• actual : BudgetWorld
• defense : BudgetWorld
• education : BudgetWorld

@[instance_reducible]

instance AlonsoOvalle2009.instDecidableEqBudgetWorld : DecidableEq BudgetWorld

Equations

• AlonsoOvalle2009.instDecidableEqBudgetWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalle2009.instFintypeBudgetWorld : Fintype BudgetWorld

Equations

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

def AlonsoOvalle2009.BudgetWorld.rank : BudgetWorld → ℕ

Equations

• AlonsoOvalle2009.BudgetWorld.actual.rank = 0
• AlonsoOvalle2009.BudgetWorld.defense.rank = 1
• AlonsoOvalle2009.BudgetWorld.education.rank = 2

@[reducible, inline]

abbrev AlonsoOvalle2009.budgetSim : BudgetWorld → Preorder BudgetWorld

Equations

• AlonsoOvalle2009.budgetSim x✝ = Preorder.lift AlonsoOvalle2009.BudgetWorld.rank

@[reducible, inline]

abbrev AlonsoOvalle2009.defense : Finset BudgetWorld

Equations

• AlonsoOvalle2009.defense = {AlonsoOvalle2009.BudgetWorld.defense}

@[reducible, inline]

abbrev AlonsoOvalle2009.education : Finset BudgetWorld

Equations

• AlonsoOvalle2009.education = {AlonsoOvalle2009.BudgetWorld.education}

theorem AlonsoOvalle2009.budget : (∀ (w : BudgetWorld), w ∉ Conditional.distributiveImp budgetSim {defense, education} ↑defense) ∧ BudgetWorld.actual ∈ Conditional.disjunctiveImp budgetSim {defense, education} ↑defense

(80) is a contradiction under the analysis and true once Existential Closure (82) returns the Boolean antecedent.

The paper's verdicts

def AlonsoOvalle2009.cropAlts : String → Option (Finset (Finset McKayVanInwagen1977.CropWorld))

The alternatives a row's antecedent feature names in each model.

Equations

• AlonsoOvalle2009.cropAlts "good weather" = some {AlonsoOvalle2009.goodWeatherW}
• AlonsoOvalle2009.cropAlts "sun cold" = some {AlonsoOvalle2009.sunColdW}
• AlonsoOvalle2009.cropAlts "good weather or sun cold" = some {AlonsoOvalle2009.goodWeatherW, AlonsoOvalle2009.sunColdW}
• AlonsoOvalle2009.cropAlts x✝ = none

def AlonsoOvalle2009.hitlerAlts : String → Option (Finset (Finset HitlerWorld))

Equations

• AlonsoOvalle2009.hitlerAlts "joined Germany" = some {AlonsoOvalle2009.joinedGermany}
• AlonsoOvalle2009.hitlerAlts "joined the U.S." = some {AlonsoOvalle2009.joinedUS}
• AlonsoOvalle2009.hitlerAlts "joined Germany or the U.S." = some {AlonsoOvalle2009.joinedGermany, AlonsoOvalle2009.joinedUS}
• AlonsoOvalle2009.hitlerAlts x✝ = none

def AlonsoOvalle2009.forkAlts : String → Option (Finset (Finset ForkWorld))

Equations

• AlonsoOvalle2009.forkAlts "magic book" = some {AlonsoOvalle2009.hasBook}
• AlonsoOvalle2009.forkAlts "newborn baby" = some {AlonsoOvalle2009.newborn}
• AlonsoOvalle2009.forkAlts "magic book or newborn baby" = some {AlonsoOvalle2009.hasBook, AlonsoOvalle2009.newborn}
• AlonsoOvalle2009.forkAlts x✝ = none

def AlonsoOvalle2009.verdict {W : Type u_1} (ord : W → Preorder W) (S : Finset (Finset W)) (C : Set W) (w : W) [DecidableEq W] [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ C] : String → Bool → Option Bool

The verdict of the analysis for a would or might consequent, possibly negated.

Equations

• AlonsoOvalle2009.verdict ord S C w "would" x✝ = some (decide (w ∈ Conditional.distributiveImp ord S C) != x✝)
• AlonsoOvalle2009.verdict ord S C w "might" x✝ = some (decide (AlonsoOvalle2009.DistributiveMight ord S C w) != x✝)
• AlonsoOvalle2009.verdict ord S C w x✝¹ x✝ = none

def AlonsoOvalle2009.predicted (row : Datum) : Option Bool

A row's predicted verdict from its scenario, antecedent, modal, and polarity features; (80) takes the Existential Closure reading (82).

Equations

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

theorem AlonsoOvalle2009.rows_agree (row : Datum) : row ∈ Examples.all → ∀ (v : String), row.feature? "verdict" = some v → ∀ (b : Bool), predicted row = some b → v = if b = true then "true" else "false"

Every row with a stated verdict that the models cover carries the predicted one.