Alonso-Ovalle 2009 — "Counterfactuals, correlatives, and disjunction"

[AO09]

Linguistics and Philosophy 32(2): 207–244.

Core proposal

The natural interpretation of disjunctive counterfactuals — "if A or B, would C" — selects from each disjunct's closest worlds, NOT from the union's closest worlds. [AO09] (p. 207) refutes [Lew73b]'s standard minimal-change semantics on this reading without abandoning minimal change. Two refinements:

1. Disjunctions introduce propositional alternatives in the semantic derivation (Hamblin-style alternative semantics, following Aloni 2003a, Simons 2005, and Alonso-Ovalle's own dissertation). The Or Rule (10) p. 212: or outputs the SET {⟦B⟧, ⟦C⟧} as alternatives rather than the Boolean union.
2. Conditionals are correlative constructions (von Fintel 1994, Izvorski 1996, Bhatt & Pancheva 2006, Schlenker 2004). The if-clause is a universal quantifier over propositions; then is a propositional anaphor. This forces universal quantification over the disjunct alternatives.

Truth condition (eqn 25-26 p. 217)

⟦if A, would C⟧ = λw. ∀p ∈ Alt(A): f_{≤,w}(p) ⊆ ⟦C⟧

Equivalently: every disjunct alternative's closest worlds satisfy the consequent. This is structurally [San18b]'s sdaEval — universal-over-per-alternative-conditionals (Simplification reading).

Connection to linglib substrate

aoConditional IS [San18b]'s sdaEval (Studies/Santorio2018.lean); the bridge is rfl. The frameworks DIFFER in their treatment of the alternative set, not the per-alternative evaluation:

• [AO09] (Hamblin Or Rule, eqn 13 p. 213): alts = {⟦disjunct₁⟧, ⟦disjunct₂⟧, ...} — only the disjuncts themselves.
• [San18b] (Katzir-generated ALT_S + stability algorithm): alts include the disjuncts + their conjunction + their disjunction; truthmakers are minimal-stable subsets, which can include "mixed" truthmakers [AO09] cannot generate.

The differential prediction lives in [San18b] §IV.3 (Karenina/W&P 8-alternative example) and is proved as santorio_finds_mixed_truthmaker_ao_misses_it in that file.

§1 The bumper crop scenario (p. 208)

Same scenario as [McKVI77] (a variation of Nute 1975): "If we had had good weather this summer or the sun had grown cold, we would have had a bumper crop." Standard minimal-change with Boolean or predicts TRUE; intuition says FALSE. Worlds and similarity ordering already formalised in Studies/McKayVanInwagen1977.lean::cropSim and consumed via the substrate.

§2.1–2.2 The analysis

def AlonsoOvalle2009.aoConditional {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (alts : List (Santorio2018.DecAlt W)) (C : W → Prop) [DecidablePred C] (w : W) : Prop

[AO09] conditional verdict for a disjunctive antecedent (eqn 25–26 p. 217): every disjunct alternative's closest worlds satisfy the consequent.

Definitionally equal to [San18b]'s sdaEval — the Simplification reading. The two accounts diverge in how the alternative SET is generated (see module docstring), not in this per-alternative evaluation rule.

Equations

• AlonsoOvalle2009.aoConditional sim alts C w = Santorio2018.sdaEval sim alts C w

theorem AlonsoOvalle2009.aoConditional_eq_sdaEval {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (alts : List (Santorio2018.DecAlt W)) (C : W → Prop) [DecidablePred C] (w : W) : aoConditional sim alts C w = Santorio2018.sdaEval sim alts C w

Bridge: AO = Santorio's sdaEval. Definitionally equal; the two formalisations of the per-alternative-conditional reading coincide. The substantive difference between [AO09] and [San18b] is the alternative-set construction, not this evaluation rule.

def AlonsoOvalle2009.aoAlternatives {W : Type u_1} (A B : W → Prop) [DecidablePred A] [DecidablePred B] : List (Santorio2018.DecAlt W)

Disjunct-only alternative set construction (Hamblin Or Rule, eqn 13 p. 213). For a disjunctive antecedent A or B, [AO09]'s alternative set is exactly [⟨A, _⟩, ⟨B, _⟩] — the two disjunct denotations bundled with decidability. No conjunction, no disjunctive closure, no Katzir-generated structural alternatives. This is the locality [San18b] §III argues against.

Equations

• AlonsoOvalle2009.aoAlternatives A B = [⟨A, inferInstance⟩, ⟨B, inferInstance⟩]

§2.2.3 Universal force

The two-component analysis — alternative-generating or plus correlative-style universal quantification — entails the conjunction inference (27a) ⊨ (27b) ∧ (27c). The Lean witness below uses sdaEval_iff_forall from the [San18b] substrate.

theorem AlonsoOvalle2009.ao_conjunction_inference {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (A B : W → Prop) [DecidablePred A] [DecidablePred B] (C : W → Prop) [DecidablePred C] (w : W) : aoConditional sim (aoAlternatives A B) C w → Semantics.Conditionals.Counterfactual.universalCounterfactual sim A C w ∧ Semantics.Conditionals.Counterfactual.universalCounterfactual sim B C w

Conjunction inference (eqn 27 p. 218): a disjunctive would- counterfactual entails each per-disjunct counterfactual. This is the SDA validity that [AO09]'s analysis derives from universal force over alternatives. Consequence of sdaEval_iff_forall.

§1 The divergence: Boolean or (Coordinator.op .disj) is the wrong meaning

The Coordinator API's disjunction Coordinator.op .disj is the Boolean join ⊔ — at the proposition carrier CropWorld → Prop, exactly the union goodWeather ∨ sunCold whose minimal-change reading [AO09] (p. 208–210, the bumper-crop counterfactual) refutes. So feeding op .disj to a counterfactual antecedent overgenerates: it collapses the disjuncts into one proposition, predicting the disjunctive counterfactual TRUE, where the alternative-semantics reading (disjuncts kept as a set) correctly predicts FALSE. This is the disjunction analogue of the [Cha16b] and-overgeneration: op is faithful at the Boolean carrier, but the rival construal the data demands diverges from it.

theorem AlonsoOvalle2009.op_disj_eq_union : Coordinator.op Coordinator.Role.disj McKayVanInwagen1977.goodWeather McKayVanInwagen1977.sunCold = fun (w : McKayVanInwagen1977.CropWorld) => McKayVanInwagen1977.goodWeather w ∨ McKayVanInwagen1977.sunCold w

Coordinator.op .disj at the proposition carrier IS the Boolean union of the disjuncts — the [Lew73b] reading [AO09] refutes (eqn 6, p. 209).

theorem AlonsoOvalle2009.op_disj_overgenerates_disjunctive_counterfactual : Semantics.Conditionals.Counterfactual.universalCounterfactual McKayVanInwagen1977.cropSim (fun (w : McKayVanInwagen1977.CropWorld) => McKayVanInwagen1977.goodWeather w ∨ McKayVanInwagen1977.sunCold w) McKayVanInwagen1977.bumperCrop McKayVanInwagen1977.CropWorld.actual ∧ ¬aoConditional McKayVanInwagen1977.cropSim (aoAlternatives McKayVanInwagen1977.goodWeather McKayVanInwagen1977.sunCold) McKayVanInwagen1977.bumperCrop McKayVanInwagen1977.CropWorld.actual

The payoff ([AO09] §1, p. 208–210): the Boolean disjunction Coordinator.op .disj (= the union goodWeather ⊔ sunCold, op_disj_eq_union) fed to the minimal-change conditional overgenerates — it predicts "if good weather or the sun grew cold, we'd have a bumper crop" TRUE (bumperCrop_lewis_true: the closest union-world is a good-weather world), whereas the alternative-semantics reading (disjuncts kept as a set) correctly predicts it FALSE (the cold-sun alternative gives no crop). So op .disj is NOT the meaning of or in a disjunctive antecedent: the alternatives must stay separate.