Zani, Ciardelli and Sanfelici (2026): Simplification of Disjunctive Antecedents

This file formalizes the semantic predictions that Zani, Ciardelli and Sanfelici test in an acquisition study of conditionals with disjunctive antecedents, if A or B, C. The three readings of Table 2 are truth conditions over a similarity model: the simplification reading SDA is the conjunction of the two simplifications, the substrate's distributiveImp; the disjunctive conditional reading DCR is their disjunction; and the asymmetric reading AR is the simplification of the more realistic disjunct. Under Lewis's minimal-change semantics, the substrate's disjunctiveImp, the DAC quantifies over the closest worlds of the disjunction, and §2's case analysis follows: when neither disjunct is more realistic than the other the DAC is equivalent to SDA (would_iff_distributive_of_equallyRealistic), and when one is more realistic it is equivalent to that disjunct's simplification (would_iff_of_moreRealistic). The readings are ordered by strength, SDA entails AR entails DCR (would_of_distributive, dcr_of_would).

The experiment's target items (9) are evaluated in the race scenario of §4: the squirrel and the tortoise compete, the prize named in the consequent belongs to one of them, and the similarity orderings of Figure 3 make the squirrel a more realistic winner than the tortoise or tie them. Table 3's response patterns follow by computation (table3_sda, table3_dcr, table3_ar), and acceptance of the closeness evaluation item if the hare doesn't win, the squirrel will win reveals that the participant regards the squirrel as the more realistic winner (moreRealistic_of_closeness). On the homogeneity accounts of Santorio and of Cariani and Goldstein, SDA is the universal and DCR the existential resolution of the homogeneous quantification over the disjuncts (dcr_iff_homogeneity_ne_false), which is the source of the paper's prediction that children shift from DCR to SDA as they do for plural definites; on Bar-Lev and Fox's account, the literal meaning is Lewis's (literal_eq_would) and exhaustification strengthens it to SDA (distributive_of_exh).

Implementation notes

• A proposition is more realistic than another at w when it has closest worlds and each of them is strictly closer than every closest world of the other (MoreRealistic); the case analysis of §2 assumes total similarity preorders on finitely many worlds.
• The scenario's worlds are the three possible winners, ordered by speed from the actual world in which the hare wins; the two orderings realize the conditions of Figure 3.

TODO

• The response patterns of Tables 5–8, the rates of Figures 4 and 5 and the regression of Table 4 await a data format for experimental results.

References

• [ZCS26]
• [Lew73b]
• [AO09]
• [San18b]
• [CG20]
• [BLF20]
• [TKC19]

Realism (§2)

def ZaniCiardelliSanfelici2026.MoreRealistic {W : Type u_1} (ord : W → Preorder W) (A B : Set W) (w : W) : Prop

A is more realistic than B at w when A has closest worlds and each of them is strictly closer to w than every closest B-world.

Equations

• ZaniCiardelliSanfelici2026.MoreRealistic ord A B w = (((ord w).minimals A).Nonempty ∧ ∀ a ∈ (ord w).minimals A, ∀ b ∈ (ord w).minimals B, a < b)

theorem ZaniCiardelliSanfelici2026.minimals_union_of_moreRealistic {W : Type u_1} {ord : W → Preorder W} {A B : Set W} {w : W} [Finite W] (htot : ∀ (w : W), Std.Total LE.le) (h : MoreRealistic ord A B w) : (ord w).minimals (A ∪ B) = (ord w).minimals A

In case 2 of §2, when A is more realistic than B, the closest worlds of the disjunction are the closest A-worlds.

theorem ZaniCiardelliSanfelici2026.minimals_union_of_equallyRealistic {W : Type u_1} {ord : W → Preorder W} {A B : Set W} {w : W} [Finite W] (htot : ∀ (w : W), Std.Total LE.le) (hAB : ¬MoreRealistic ord A B w) (hBA : ¬MoreRealistic ord B A w) : (ord w).minimals (A ∪ B) = (ord w).minimals A ∪ (ord w).minimals B

In case 1 of §2, when neither disjunct is more realistic than the other, the closest worlds of the disjunction are the closest worlds of the disjuncts together.

The three readings (Table 2)

def ZaniCiardelliSanfelici2026.DCR {W : Type u_1} (ord : W → Preorder W) (A B : Finset W) (C : Set W) (w : W) : Prop

The disjunctive conditional reading holds when some simplification holds.

Equations

• ZaniCiardelliSanfelici2026.DCR ord A B C w = (w ∈ Conditional.closestImp ord (↑A) C ∨ w ∈ Conditional.closestImp ord (↑B) C)

theorem ZaniCiardelliSanfelici2026.would_iff_distributive_of_equallyRealistic {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) {w : W} [DecidableEq W] [Fintype W] (htot : ∀ (w : W), Std.Total LE.le) (hAB : ¬MoreRealistic ord (↑A) (↑B) w) (hBA : ¬MoreRealistic ord (↑B) (↑A) w) : w ∈ Conditional.disjunctiveImp ord {A, B} C ↔ w ∈ Conditional.distributiveImp ord {A, B} C

When neither disjunct is more realistic, Lewis's DAC is equivalent to SDA.

theorem ZaniCiardelliSanfelici2026.would_iff_of_moreRealistic {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) {w : W} [DecidableEq W] [Fintype W] (htot : ∀ (w : W), Std.Total LE.le) (h : MoreRealistic ord (↑A) (↑B) w) : w ∈ Conditional.disjunctiveImp ord {A, B} C ↔ w ∈ Conditional.closestImp ord (↑A) C

When A is more realistic than B, Lewis's DAC is equivalent to the simplification with the more realistic disjunct, which is the asymmetric reading.

theorem ZaniCiardelliSanfelici2026.would_of_distributive {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) {w : W} [DecidableEq W] (h : w ∈ Conditional.distributiveImp ord {A, B} C) : w ∈ Conditional.disjunctiveImp ord {A, B} C

SDA entails Lewis's DAC, and so the asymmetric reading.

theorem ZaniCiardelliSanfelici2026.dcr_of_would {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) {w : W} [DecidableEq W] (htot : ∀ (w : W), Std.Total LE.le) (h : w ∈ Conditional.disjunctiveImp ord {A, B} C) : DCR ord A B C w

Lewis's DAC, and so the asymmetric reading, entails DCR under a total ordering.

Homogeneity and exhaustification (§2, §3)

theorem ZaniCiardelliSanfelici2026.dcr_iff_homogeneity_ne_false {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) {w : W} [DecidableEq W] [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ C] : DCR ord A B C w ↔ Conditional.homogeneousImp ord {A, B} C w ≠ -1

On the homogeneity accounts, DCR is the existential resolution of the homogeneous quantification over the disjuncts, on which the DAC is not false. SDA is its universal resolution, homogeneousImp_eq_one_iff.

theorem ZaniCiardelliSanfelici2026.literal_eq_would {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) [DecidableEq W] : Conditional.closestImp ord (↑A ∪ ↑B) C = Conditional.disjunctiveImp ord {A, B} C

The literal meaning of the DAC on the exhaustification account is Lewis's.

theorem ZaniCiardelliSanfelici2026.distributive_of_exh {W : Type u_1} {ord : W → Preorder W} {A B : Finset W} (C : Set W) {w : W} [DecidableEq W] (htot : ∀ (w : W), Std.Total LE.le) (h₁ : ∃ v ∈ Conditional.closestImp ord (↑A ∪ ↑B) C, v ∉ Conditional.closestImp ord (↑B) C ∪ Conditional.closestImp ord (↑A ∩ ↑B) C) (h₂ : ∃ v ∈ Conditional.closestImp ord (↑A ∪ ↑B) C, v ∉ Conditional.closestImp ord (↑A) C ∪ Conditional.closestImp ord (↑A ∩ ↑B) C) (h : ∃ v ∈ Conditional.closestImp ord (↑A) C ∩ Conditional.closestImp ord (↑B) C, v ∉ Conditional.closestImp ord (↑A ∩ ↑B) C) (hw : w ∈ Exhaustification.exhIEII (BarLevFox2020.sdaAlts ord (↑A) (↑B) C) (Conditional.closestImp ord (↑A ∪ ↑B) C)) : w ∈ Conditional.distributiveImp ord {A, B} C

Exhaustification with innocent inclusion strengthens the literal DAC to SDA, under the model conditions of [BLF20]'s derivation.

The closeness evaluation item (§4)

theorem ZaniCiardelliSanfelici2026.moreRealistic_of_closeness {W : Type u_1} {ord : W → Preorder W} {w : W} [Fintype W] (htot : ∀ (w : W), Std.Total LE.le) {H S T : Finset W} (hclose : w ∈ Conditional.closestImp ord (↑H)ᶜ ↑S) (hS : S.Nonempty) (hT : ∀ t ∈ T, t ∉ H) (hST : ∀ t ∈ T, t ∉ S) : MoreRealistic ord (↑S) (↑T) w

Accepting if not H, S reveals that S is more realistic than any T disjoint from S within the H-free worlds, since every closest H-free world is an S-world, and a closest T-world as close as a closest S-world would be one of them.

The race scenario and Table 3

inductive ZaniCiardelliSanfelici2026.Competitor : Type

The competitors of a scenario, in order of speed.

• hare : Competitor
• squirrel : Competitor
• tortoise : Competitor

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableEqCompetitor : DecidableEq Competitor

Equations

• ZaniCiardelliSanfelici2026.instDecidableEqCompetitor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instFintypeCompetitor : Fintype Competitor

Equations

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

def ZaniCiardelliSanfelici2026.instReprCompetitor.repr : Competitor → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instReprCompetitor : Repr Competitor

Equations

• ZaniCiardelliSanfelici2026.instReprCompetitor = { reprPrec := ZaniCiardelliSanfelici2026.instReprCompetitor.repr }

inductive ZaniCiardelliSanfelici2026.Prize : Type

The prizes; each competitor's prize is fixed by the scenario.

• carrot : Prize
• hazelnut : Prize
• lettuce : Prize

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableEqPrize : DecidableEq Prize

Equations

• ZaniCiardelliSanfelici2026.instDecidableEqPrize x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ZaniCiardelliSanfelici2026.instReprPrize.repr : Prize → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instReprPrize : Repr Prize

Equations

• ZaniCiardelliSanfelici2026.instReprPrize = { reprPrec := ZaniCiardelliSanfelici2026.instReprPrize.repr }

def ZaniCiardelliSanfelici2026.Competitor.prize : Competitor → Prize

Each competitor's prize.

Equations

• ZaniCiardelliSanfelici2026.Competitor.hare.prize = ZaniCiardelliSanfelici2026.Prize.carrot
• ZaniCiardelliSanfelici2026.Competitor.squirrel.prize = ZaniCiardelliSanfelici2026.Prize.hazelnut
• ZaniCiardelliSanfelici2026.Competitor.tortoise.prize = ZaniCiardelliSanfelici2026.Prize.lettuce

def ZaniCiardelliSanfelici2026.Competitor.speed : Competitor → ℕ

Speed rank, the hare fastest.

Equations

• ZaniCiardelliSanfelici2026.Competitor.hare.speed = 0
• ZaniCiardelliSanfelici2026.Competitor.squirrel.speed = 1
• ZaniCiardelliSanfelici2026.Competitor.tortoise.speed = 2

@[reducible, inline]

abbrev ZaniCiardelliSanfelici2026.nonEqual : Competitor → Preorder Competitor

In Figure 3(a), the non-equally realistic condition, a faster competitor is a more realistic winner.

Equations

• ZaniCiardelliSanfelici2026.nonEqual x✝ = Preorder.lift ZaniCiardelliSanfelici2026.Competitor.speed

@[reducible, inline]

abbrev ZaniCiardelliSanfelici2026.equal : Competitor → Preorder Competitor

In Figure 3(b), the equally realistic condition, the squirrel and the tortoise tie.

Equations

• ZaniCiardelliSanfelici2026.equal x✝ = Preorder.lift fun (v : ZaniCiardelliSanfelici2026.Competitor) => min v.speed 1

theorem ZaniCiardelliSanfelici2026.nonEqual_total (w₀ : Competitor) : Std.Total LE.le

structure ZaniCiardelliSanfelici2026.Item : Type

A target item (9) reads if first or second wins, it will get prize.

• first : Competitor
• second : Competitor
• prize : Prize

def ZaniCiardelliSanfelici2026.items : List Item

The four target items (9a)–(9d).

Equations

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

def ZaniCiardelliSanfelici2026.Item.sda (it : Item) : Prop

The SDA verdict on an item in the actual world, where the hare won.

Equations

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

def ZaniCiardelliSanfelici2026.Item.dcr (it : Item) : Prop

The DCR verdict on an item.

Equations

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

def ZaniCiardelliSanfelici2026.Item.ar (it : Item) : Prop

Lewis's verdict on an item in the non-equally realistic condition is the asymmetric reading.

Equations

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

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableSda (it : Item) : Decidable it.sda

Equations

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

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableDcr (it : Item) : Decidable it.dcr

Equations

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

@[instance_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableAr (it : Item) : Decidable it.ar

Equations

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

theorem ZaniCiardelliSanfelici2026.table3_sda : List.map (fun (it : Item) => decide it.sda) items = [false, false, false, false]

On SDA in Table 3 every target item is false, since one simplification always fails.

theorem ZaniCiardelliSanfelici2026.table3_dcr : List.map (fun (it : Item) => decide it.dcr) items = [true, true, true, true]

On DCR in Table 3 every target item is true, since one simplification always holds.

theorem ZaniCiardelliSanfelici2026.table3_ar : List.map (fun (it : Item) => decide it.ar) items = [true, true, false, false]

On AR in Table 3 the items naming the squirrel's prize are true and the others false.

theorem ZaniCiardelliSanfelici2026.table3_equal : List.map (fun (it : Item) => decide (Competitor.hare ∈ Conditional.disjunctiveImp equal {{it.first}, {it.second}} {v : Competitor | v.prize = it.prize})) items = [false, false, false, false]

In the equally realistic condition, Lewis's verdicts coincide with SDA on every item.

theorem ZaniCiardelliSanfelici2026.closeness_item : Competitor.hare ∈ Conditional.closestImp nonEqual {Competitor.hare}ᶜ {Competitor.squirrel} ∧ Competitor.hare ∉ Conditional.closestImp equal {Competitor.hare}ᶜ {Competitor.squirrel}

The closeness evaluation item if the hare doesn't win, the squirrel will win holds in the non-equally realistic condition and fails in the equally realistic one.

theorem ZaniCiardelliSanfelici2026.squirrel_moreRealistic : MoreRealistic nonEqual {Competitor.squirrel} {Competitor.tortoise} Competitor.hare

Accepting the closeness evaluation item makes the squirrel the more realistic winner, which is what licenses the asymmetric pattern of Table 3.