@cite{zani-ciardelli-sanfelici-2026} — SDA from Acquisition

Simplification of disjunctive antecedents: Insights from acquisition. Semantics and Pragmatics 19(3).

Core Contribution

Experimental study of 148 Italian children (ages 4;1–9;11) and 28 adults on disjunctive antecedent conditionals (DACs), testing three readings:

1. SDA (Simplification, @cite{mckay-vaninwagen-1977}): "if A or B, C" ≡ "(if A, C) and (if B, C)"
2. DCR (Disjunctive Conditional Reading): "if A or B, C" ≡ "(if A, C) or (if B, C)"
3. AR (Asymmetric Reading): only the more realistic disjunct matters

Key Findings

1. SDA is the preferred reading at all ages, already dominant at age 4–5
2. AR is nearly absent (2.3% of children's responses)
3. DCR decreases with age while SDA increases — a DCR→SDA developmental shift strictly parallel to the existential→universal shift in plural definites (@cite{tieu-kriz-chemla-2019})
4. No indicative/counterfactual difference (Mode non-significant, p = 0.869)
5. SDA does not require equally realistic disjuncts (contra @cite{lewis-1973})

Theoretical Implications

The DCR→SDA trajectory supports homogeneity-based accounts (@cite{santorio-2018}, @cite{cariani-goldstein-2020}) over:

• @cite{lewis-1973}: predicts AR when disjuncts differ in realism; AR is absent
• @cite{bar-lev-fox-2020}: predicts AR→SDA shift; observed shift is DCR→SDA

Connection to Linglib

• DAC readings use the alternative-sensitive conditional semantics from Phenomena/Conditionals/Studies/Santorio2018.lean: homogeneityEval, sdaEval
• The DCR (Disjunctive Conditional Reading) operator dcrEval is defined in this file. DCR is named here in @cite{zani-ciardelli-sanfelici-2026} (p. 10), not in @cite{santorio-2018} — Santorio's two readings are SDA (with the DIST_π operator) and the asymmetric Lewis reading (without DIST_π, via default existential closure of the antecedent alternatives).
• SDA/DCR correspond to conjunctive/disjunctive ProjectionType
• Developmental trajectory parallels @cite{tieu-kriz-chemla-2019}'s existential→homogeneous shift

def ZaniCiardelliSanfelici2026.dcrEval {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (alts : List (Phenomena.Conditionals.Studies.Santorio2018.DecAlt W)) (C : W → Prop) [DecidablePred C] (w : W) : Prop

DCR (Disjunctive Conditional Reading): existential resolution over per-alternative conditionals — "if A or B, C" iff some simplification (if A, C) ∨ (if B, C) holds.

Named in @cite{zani-ciardelli-sanfelici-2026} (p. 10): "We will refer to this reading of DACs as the disjunctive conditional reading." Lives in this file (rather than the @cite{santorio-2018} substrate) because DCR is not part of Santorio's framework.

Equations

• ZaniCiardelliSanfelici2026.dcrEval sim alts C w = ∃ a ∈ alts, Semantics.Conditionals.Counterfactual.universalCounterfactual sim a.pred C w

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableDcrEval {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (alts : List (Phenomena.Conditionals.Studies.Santorio2018.DecAlt W)) (C : W → Prop) [DecidablePred C] (w : W) : Decidable (dcrEval sim alts C w)

Equations

• ZaniCiardelliSanfelici2026.instDecidableDcrEval sim alts C w = ZaniCiardelliSanfelici2026.instDecidableDcrEval._aux_1 sim alts C w

inductive ZaniCiardelliSanfelici2026.DACReading : Type

The three theoretically predicted readings of disjunctive antecedent conditionals (DACs). Table 2 of the paper.

• sda : DACReading
• dcr : DACReading
• ar : DACReading

def ZaniCiardelliSanfelici2026.instReprDACReading.repr : DACReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprDACReading : Repr DACReading

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableEqDACReading : DecidableEq DACReading

Equations

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

def ZaniCiardelliSanfelici2026.DACReading.strength : DACReading → ℕ

Logical strength ordering: SDA ≥ AR ≥ DCR.

Equations

• ZaniCiardelliSanfelici2026.DACReading.sda.strength = 2
• ZaniCiardelliSanfelici2026.DACReading.ar.strength = 1
• ZaniCiardelliSanfelici2026.DACReading.dcr.strength = 0

theorem ZaniCiardelliSanfelici2026.sda_entails_ar : DACReading.sda.strength ≥ DACReading.ar.strength

theorem ZaniCiardelliSanfelici2026.ar_entails_dcr : DACReading.ar.strength ≥ DACReading.dcr.strength

def ZaniCiardelliSanfelici2026.dacProjection : DACReading → Core.Duality.ProjectionType

SDA = conjunctive projection over alternatives. DCR = disjunctive projection over alternatives. This is the same duality as quantifier strength in @cite{ramotowska-marty-romoli-santorio-2025}.

Equations

• ZaniCiardelliSanfelici2026.dacProjection ZaniCiardelliSanfelici2026.DACReading.sda = Core.Duality.ProjectionType.conjunctive
• ZaniCiardelliSanfelici2026.dacProjection ZaniCiardelliSanfelici2026.DACReading.dcr = Core.Duality.ProjectionType.disjunctive
• ZaniCiardelliSanfelici2026.dacProjection ZaniCiardelliSanfelici2026.DACReading.ar = Core.Duality.ProjectionType.disjunctive

theorem ZaniCiardelliSanfelici2026.alt_semantics_validates_sda {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (A B : Phenomena.Conditionals.Studies.Santorio2018.DecAlt W) (C : W → Prop) [DecidablePred C] (w : W) : Phenomena.Conditionals.Studies.Santorio2018.sdaEval sim [A, B] C w ↔ Semantics.Conditionals.Counterfactual.universalCounterfactual sim A.pred C w ∧ Semantics.Conditionals.Counterfactual.universalCounterfactual sim B.pred C w

Alternative semantics validates SDA universally (for two alternatives): "if {A,B}, C" ≡ ∀p ∈ {A,B}. min_w(p) ⊆ C ≡ (if A, C) ∧ (if B, C). Under Lewis, SDA is only contingently valid.

inductive ZaniCiardelliSanfelici2026.ConditionalMode : Type

Conditional mode (indicative vs counterfactual).

• indicative : ConditionalMode
• counterfactual : ConditionalMode

def ZaniCiardelliSanfelici2026.instReprConditionalMode.repr : ConditionalMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprConditionalMode : Repr ConditionalMode

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableEqConditionalMode : DecidableEq ConditionalMode

Equations

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

inductive ZaniCiardelliSanfelici2026.AgeGroup : Type

Age groups in the study. Table 1.

• age4 : AgeGroup
• age5 : AgeGroup
• age6 : AgeGroup
• age7 : AgeGroup
• age8 : AgeGroup
• age9 : AgeGroup
• adult : AgeGroup

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprAgeGroup : Repr AgeGroup

Equations

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

def ZaniCiardelliSanfelici2026.instReprAgeGroup.repr : AgeGroup → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableEqAgeGroup : DecidableEq AgeGroup

Equations

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

def ZaniCiardelliSanfelici2026.AgeGroup.n : AgeGroup → ℕ

Number of eligible participants per age group. Table 1.

Equations

• ZaniCiardelliSanfelici2026.AgeGroup.age4.n = 8
• ZaniCiardelliSanfelici2026.AgeGroup.age5.n = 28
• ZaniCiardelliSanfelici2026.AgeGroup.age6.n = 28
• ZaniCiardelliSanfelici2026.AgeGroup.age7.n = 28
• ZaniCiardelliSanfelici2026.AgeGroup.age8.n = 28
• ZaniCiardelliSanfelici2026.AgeGroup.age9.n = 28
• ZaniCiardelliSanfelici2026.AgeGroup.adult.n = 28

theorem ZaniCiardelliSanfelici2026.total_participants : AgeGroup.age4.n + AgeGroup.age5.n + AgeGroup.age6.n + AgeGroup.age7.n + AgeGroup.age8.n + AgeGroup.age9.n + AgeGroup.adult.n = 176

theorem ZaniCiardelliSanfelici2026.total_children : AgeGroup.age4.n + AgeGroup.age5.n + AgeGroup.age6.n + AgeGroup.age7.n + AgeGroup.age8.n + AgeGroup.age9.n = 148

structure ZaniCiardelliSanfelici2026.TargetItem : Type

The four target items per scenario. Table 3. Each item has a disjunctive antecedent where the consequent matches one disjunct's prize (making one simplification true, one false).

• label : String
• sdaPrediction : Bool
• dcrPrediction : Bool
• arPrediction : Bool

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprTargetItem : Repr TargetItem

Equations

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

def ZaniCiardelliSanfelici2026.instReprTargetItem.repr : TargetItem → ℕ → Std.Format

Equations

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

def ZaniCiardelliSanfelici2026.targetItems : List TargetItem

Equations

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

structure ZaniCiardelliSanfelici2026.PatternRates : Type

Overall pattern rates (percentages, one-decimal precision as reported).

• sda : ℚ
• dcr : ℚ
• ar : ℚ
• other : ℚ

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprPatternRates : Repr PatternRates

Equations

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

def ZaniCiardelliSanfelici2026.instReprPatternRates.repr : PatternRates → ℕ → Std.Format

Equations

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

def ZaniCiardelliSanfelici2026.childrenOverall : PatternRates

Children's overall rates (across modes and age groups).

Equations

• ZaniCiardelliSanfelici2026.childrenOverall = { sda := 450 / 10, dcr := 182 / 10, ar := 23 / 10, other := 345 / 10 }

def ZaniCiardelliSanfelici2026.adultsOverall : PatternRates

Adults' overall rates (across modes). From Table 6 profiles: 26 SDA, 1 DCR, 1 mixed (AR ctf / DCR ind). Scenario-level: SDA 92.9%, DCR 5.4%, AR 1.8%.

Equations

• ZaniCiardelliSanfelici2026.adultsOverall = { sda := 929 / 10, dcr := 54 / 10, ar := 18 / 10, other := 0 }

theorem ZaniCiardelliSanfelici2026.sda_most_frequent : childrenOverall.sda > childrenOverall.dcr ∧ childrenOverall.sda > childrenOverall.ar ∧ adultsOverall.sda > adultsOverall.dcr

Finding 1: SDA is the most frequent reading for both groups.

theorem ZaniCiardelliSanfelici2026.ar_nearly_absent : childrenOverall.ar < 5 ∧ adultsOverall.ar < 5

Finding 2: AR is nearly absent.

structure ZaniCiardelliSanfelici2026.ModeRates : Type

Rates per mode (from Figure 5). All four pattern categories.

• indicativeSDA : ℚ
• counterfactualSDA : ℚ
• indicativeDCR : ℚ
• counterfactualDCR : ℚ
• indicativeAR : ℚ
• counterfactualAR : ℚ
• indicativeOther : ℚ
• counterfactualOther : ℚ

def ZaniCiardelliSanfelici2026.instReprModeRates.repr : ModeRates → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprModeRates : Repr ModeRates

Equations

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

def ZaniCiardelliSanfelici2026.childrenByMode : ModeRates

Equations

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

def ZaniCiardelliSanfelici2026.adultsByMode : ModeRates

Equations

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

theorem ZaniCiardelliSanfelici2026.mode_nonsignificant : adultsByMode.indicativeSDA = adultsByMode.counterfactualSDA

Finding 4: No indicative/counterfactual difference. Adults show identical SDA rates; children are very similar. (Table 4: Mode coefficient p = 0.869 for DCR vs SDA.)

def ZaniCiardelliSanfelici2026.ratesByAge : AgeGroup → PatternRates

Per-age-group pattern rates (from Figure 4 bar chart annotations). This is the paper's core developmental data. Values are approximate (read from bar chart, not tabulated in paper).

Equations

• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.age4 = { sda := 344 / 10, dcr := 312 / 10, ar := 0, other := 344 / 10 }
• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.age5 = { sda := 330 / 10, dcr := 196 / 10, ar := 9 / 10, other := 464 / 10 }
• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.age6 = { sda := 357 / 10, dcr := 259 / 10, ar := 18 / 10, other := 366 / 10 }
• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.age7 = { sda := 482 / 10, dcr := 259 / 10, ar := 9 / 10, other := 250 / 10 }
• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.age8 = { sda := 482 / 10, dcr := 116 / 10, ar := 45 / 10, other := 357 / 10 }
• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.age9 = { sda := 598 / 10, dcr := 54 / 10, ar := 36 / 10, other := 312 / 10 }
• ZaniCiardelliSanfelici2026.ratesByAge ZaniCiardelliSanfelici2026.AgeGroup.adult = { sda := 929 / 10, dcr := 54 / 10, ar := 18 / 10, other := 0 }

theorem ZaniCiardelliSanfelici2026.sda_increases_from_age5 : (ratesByAge AgeGroup.age5).sda ≤ (ratesByAge AgeGroup.age6).sda ∧ (ratesByAge AgeGroup.age6).sda ≤ (ratesByAge AgeGroup.age7).sda ∧ (ratesByAge AgeGroup.age7).sda ≤ (ratesByAge AgeGroup.age8).sda ∧ (ratesByAge AgeGroup.age8).sda ≤ (ratesByAge AgeGroup.age9).sda ∧ (ratesByAge AgeGroup.age9).sda ≤ (ratesByAge AgeGroup.adult).sda

Core developmental finding: SDA rates increase monotonically from age 5 onward.

theorem ZaniCiardelliSanfelici2026.dcr_decreases_from_age7 : (ratesByAge AgeGroup.age7).dcr ≥ (ratesByAge AgeGroup.age8).dcr ∧ (ratesByAge AgeGroup.age8).dcr ≥ (ratesByAge AgeGroup.age9).dcr ∧ (ratesByAge AgeGroup.age9).dcr ≥ (ratesByAge AgeGroup.adult).dcr

Core developmental finding: DCR rates decrease from age 7 onward.

theorem ZaniCiardelliSanfelici2026.sda_dominates_dcr_at_all_ages (g : AgeGroup) : (ratesByAge g).sda ≥ (ratesByAge g).dcr

The developmental shift: SDA overtakes DCR. At every age, SDA ≥ DCR, and by adulthood SDA dominates completely.

theorem ZaniCiardelliSanfelici2026.ar_marginal_at_all_ages (g : AgeGroup) : (ratesByAge g).ar < 5

AR is marginal (< 5%) at every age group. This rules out Lewis's prediction that AR should be common in younger children.

def ZaniCiardelliSanfelici2026.halfTrueRefusalRate : ℚ

9.6% of children refused to judge DACs as true or false, saying they were "half true and half false." This is direct behavioral evidence for the truth-value gap predicted by homogeneity theory: when one simplification is true and the other false, the DAC lacks a definite truth value.

10 children showed this pattern consistently across all 4 scenarios; 6 more did so in at least one scenario.

Equations

• ZaniCiardelliSanfelici2026.halfTrueRefusalRate = 96 / 10

theorem ZaniCiardelliSanfelici2026.halfTrue_nontrivial : halfTrueRefusalRate > 5

The refusal rate is substantial — nearly 1 in 10 children.

structure ZaniCiardelliSanfelici2026.ProfileCounts : Type

Cross-mode consistency: children overwhelmingly derive the same reading in both indicative and counterfactual scenarios. Table 5 diagonal entries.

• sdaSda : ℕ
• dcrDcr : ℕ
• arAr : ℕ
• otherOther : ℕ

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprProfileCounts : Repr ProfileCounts

Equations

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

def ZaniCiardelliSanfelici2026.instReprProfileCounts.repr : ProfileCounts → ℕ → Std.Format

Equations

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

def ZaniCiardelliSanfelici2026.childProfiles : ProfileCounts

Equations

• ZaniCiardelliSanfelici2026.childProfiles = { sdaSda := 52, dcrDcr := 15, arAr := 2, otherOther := 29 }

def ZaniCiardelliSanfelici2026.adultProfiles : ProfileCounts

Equations

• ZaniCiardelliSanfelici2026.adultProfiles = { sdaSda := 26, dcrDcr := 1, arAr := 0, otherOther := 0 }

theorem ZaniCiardelliSanfelici2026.children_mostly_consistent : have diagonal := childProfiles.sdaSda + childProfiles.dcrDcr + childProfiles.arAr + childProfiles.otherOther; diagonal = 98

Children who are consistent across modes (on the diagonal).

theorem ZaniCiardelliSanfelici2026.adults_sda_dominant : adultProfiles.sdaSda = 26

Adults are almost all SDA-consistent.

structure ZaniCiardelliSanfelici2026.NonEquallyRealisticRates : Type

Rates among participants who accepted the closeness evaluation item (indicating they regard one disjunct as MORE realistic). Table 8. Lewis predicts AR for these participants.

• adultsSDA : ℚ
• childrenSDA : ℚ
• adultsAR : ℚ
• childrenAR : ℚ

def ZaniCiardelliSanfelici2026.instReprNonEquallyRealisticRates.repr : NonEquallyRealisticRates → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprNonEquallyRealisticRates : Repr NonEquallyRealisticRates

Equations

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

def ZaniCiardelliSanfelici2026.nonEquallyRealistic : NonEquallyRealisticRates

Equations

• ZaniCiardelliSanfelici2026.nonEquallyRealistic = { adultsSDA := 8776 / 100, childrenSDA := 3934 / 100, adultsAR := 408 / 100, childrenAR := 284 / 100 }

theorem ZaniCiardelliSanfelici2026.sda_without_equal_realism : nonEquallyRealistic.adultsSDA > nonEquallyRealistic.adultsAR ∧ nonEquallyRealistic.childrenSDA > nonEquallyRealistic.childrenAR

Finding 5: Even among participants who regard disjuncts as non-equally realistic, SDA dominates and AR is marginal. This directly falsifies Lewis's prediction.

def ZaniCiardelliSanfelici2026.pluralToDACParallel : TieuKrizChemla2019.DefinitePluralReading → Option DACReading

The developmental trajectory for DACs parallels the trajectory for plural definites (@cite{tieu-kriz-chemla-2019}):

Plural definites	DACs	Resolution
Existential (EXI)	DCR	∃ (some satisfy → true)
Homogeneous (HOM)	SDA	∀ (all must satisfy)
Universal (UNI)	—	—

Both phenomena show the same developmental pattern: younger children start existential (accepting when ANY element satisfies) and shift to universal/homogeneous (requiring ALL elements to satisfy).

Equations

• ZaniCiardelliSanfelici2026.pluralToDACParallel TieuKrizChemla2019.DefinitePluralReading.existential = some ZaniCiardelliSanfelici2026.DACReading.dcr
• ZaniCiardelliSanfelici2026.pluralToDACParallel TieuKrizChemla2019.DefinitePluralReading.homogeneous = some ZaniCiardelliSanfelici2026.DACReading.sda
• ZaniCiardelliSanfelici2026.pluralToDACParallel TieuKrizChemla2019.DefinitePluralReading.universal = none

def ZaniCiardelliSanfelici2026.dacDevelopmentalStage : DACReading → Option TieuKrizChemla2019.DevelopmentalStage

The developmental parallel: both trajectories go from existential-like to universal-like readings.

Equations

• ZaniCiardelliSanfelici2026.dacDevelopmentalStage ZaniCiardelliSanfelici2026.DACReading.dcr = some TieuKrizChemla2019.DevelopmentalStage.existential
• ZaniCiardelliSanfelici2026.dacDevelopmentalStage ZaniCiardelliSanfelici2026.DACReading.sda = some TieuKrizChemla2019.DevelopmentalStage.homogeneous
• ZaniCiardelliSanfelici2026.dacDevelopmentalStage ZaniCiardelliSanfelici2026.DACReading.ar = none

theorem ZaniCiardelliSanfelici2026.parallel_exact : dacDevelopmentalStage DACReading.dcr = some TieuKrizChemla2019.DevelopmentalStage.existential ∧ dacDevelopmentalStage DACReading.sda = some TieuKrizChemla2019.DevelopmentalStage.homogeneous

The parallel is structurally exact: DCR maps to the existential stage, SDA maps to the homogeneous stage.

theorem ZaniCiardelliSanfelici2026.shift_direction_matches : childrenOverall.dcr > adultsOverall.dcr ∧ adultsOverall.sda > childrenOverall.sda

Both phenomena show the same direction of shift. In TieuKrizChemla2019, the EXI/−SI group (existential, no implicatures) exists in young children and gives way to HOM groups. Here, DCR exists in young children and gives way to SDA.

inductive ZaniCiardelliSanfelici2026.SDATheory : Type

Theories of SDA and their predictions about developmental trajectory.

• lewis : SDATheory
• alternativeSem : SDATheory
• homogeneity : SDATheory
• exhaustification : SDATheory

def ZaniCiardelliSanfelici2026.instReprSDATheory.repr : SDATheory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instReprSDATheory : Repr SDATheory

Equations

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

@[implicit_reducible]

instance ZaniCiardelliSanfelici2026.instDecidableEqSDATheory : DecidableEq SDATheory

Equations

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

def ZaniCiardelliSanfelici2026.SDATheory.predictedPreSDA : SDATheory → Option DACReading

What each theory predicts as the pre-SDA reading in children.

Equations

• ZaniCiardelliSanfelici2026.SDATheory.lewis.predictedPreSDA = some ZaniCiardelliSanfelici2026.DACReading.ar
• ZaniCiardelliSanfelici2026.SDATheory.alternativeSem.predictedPreSDA = none
• ZaniCiardelliSanfelici2026.SDATheory.homogeneity.predictedPreSDA = some ZaniCiardelliSanfelici2026.DACReading.dcr
• ZaniCiardelliSanfelici2026.SDATheory.exhaustification.predictedPreSDA = some ZaniCiardelliSanfelici2026.DACReading.ar

def ZaniCiardelliSanfelici2026.observedPreSDA : DACReading

The observed pre-SDA reading is DCR, not AR.

Equations

• ZaniCiardelliSanfelici2026.observedPreSDA = ZaniCiardelliSanfelici2026.DACReading.dcr

theorem ZaniCiardelliSanfelici2026.homogeneity_fits_trajectory : SDATheory.homogeneity.predictedPreSDA = some observedPreSDA ∧ SDATheory.lewis.predictedPreSDA ≠ some observedPreSDA ∧ SDATheory.exhaustification.predictedPreSDA ≠ some observedPreSDA

Homogeneity theory correctly predicts the developmental trajectory. Lewis and exhaustification predict AR as the pre-SDA stage, but AR is nearly absent.

Answers to the Five Research Questions

Q1: At what age does SDA arise? Already at age 4–5, SDA is the most frequent non-deviant reading. This parallels the early emergence of free-choice inferences (@cite{tieu-etal-2016}).

Q2: Do children shift from AR to SDA? No. AR is nearly absent (2.3%). The two participants who consistently showed AR were aged 8;0 and 9;7 — not young children with undeveloped pragmatic skills. This is unexpected on @cite{bar-lev-fox-2020}'s account.

Q3: Do children shift from DCR to SDA? Yes. DCR is higher in younger children (~25% at ages 4–7) and decreases with age, while SDA increases. This DCR→SDA shift parallels the EXI→HOM shift in plural definites (@cite{tieu-kriz-chemla-2019}).

Q4: Does SDA arise earlier for indicatives than counterfactuals? No. Mode has no significant effect (p = 0.869). Children show the same reading in both modes (Table 5). This supports uniform accounts of conditionals.

Q5: Does SDA require equally realistic disjuncts? No. Among participants who regarded disjuncts as non-equally realistic, SDA still dominated (87.76% adults, 39.34% children) and AR was marginal (4.08% adults, 2.84% children). This falsifies Lewis's prediction that non-equally-realistic disjuncts should yield AR.

From enum stipulation to substrate derivation

The SDATheory.predictedPreSDA enum in §11 records each framework's predicted pre-SDA stage as a stipulation. The two SDA-deriving mature accounts (homogeneity / exhaustification) themselves coincide on the SDA inference proper — verifiable at the Lean substrate level via:

• @cite{santorio-2018}'s Santorio2018.sdaEval (per-alternative homogeneity, Phenomena/Conditionals/Studies/Santorio2018.lean)
• @cite{bar-lev-fox-2020}'s BarLevFox2020.bar_lev_fox_sda (Innocent Inclusion derivation, Phenomena/Modality/Studies/BarLevFox2020.lean)

The cross-mechanism agreement BarLevFox2020.bar_lev_fox_sda_implies_santorio_sda_inference proves that on the shared 4-world SDAWorld model, Bar-Lev/Fox's Exh^{IE+II} verdict entails Santorio's sdaEval verdict on the SDA inference proper. Bar-Lev/Fox is strictly stronger (also derives ¬((p∧q)□→r)); Santorio is silent on the conjunctive negation. They agree on the SDA inference itself — the empirical pattern this study measures.

The developmental contrast between the two accounts (Santorio: DCR→SDA via homogeneity-gap-then-resolution; Bar-Lev/Fox: AR→SDA via EXH-acquisition) is about different stages of the developmental trajectory, not about disagreement on the mature SDA prediction. The empirical finding (DCR→SDA, AR nearly absent) thus distinguishes the two only at the developmental level, not the mature-grammar level.

theorem ZaniCiardelliSanfelici2026.bar_lev_fox_and_santorio_agree_on_mature_sda (w : Phenomena.Modality.Studies.BarLevFox2020.SDAWorld) : Exhaustification.exhIEII Phenomena.Modality.Studies.BarLevFox2020.sdaALT Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent w → Phenomena.Conditionals.Studies.Santorio2018.sdaEval Phenomena.Modality.Studies.BarLevFox2020.sdaSim Phenomena.Modality.Studies.BarLevFox2020.sdaSantorioAlts Phenomena.Modality.Studies.BarLevFox2020.sdaR w

Substrate witness for the mature-grammar agreement: on the shared 4-world SDAWorld model from BarLevFox2020.lean, Bar-Lev/Fox's Exh^{IE+II} verdict at .actual entails Santorio's sdaEval verdict on the SDA inference. Direct re-export of the cross-framework theorem proved in BarLevFox2020.lean §7.

theorem ZaniCiardelliSanfelici2026.bar_lev_fox_strictly_stronger_than_santorio (w : Phenomena.Modality.Studies.BarLevFox2020.SDAWorld) : Exhaustification.exhIEII Phenomena.Modality.Studies.BarLevFox2020.sdaALT Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent w → ¬Phenomena.Modality.Studies.BarLevFox2020.sdaPandQbox w

Bar-Lev/Fox derives a STRICTLY STRONGER verdict than Santorio on the same model: in addition to the SDA inference proper, Bar-Lev/Fox's Exh^{IE+II} derives ¬((p∧q)□→r). This is the Innocent-Exclusion-of-the-conjunctive-alternative component (paper eqn 67 p. 206) that has no analogue in Santorio's homogeneity-based derivation.