@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 AlternativeSensitive.lean (@cite{santorio-2018}): homogeneityEval, sdaEval, dcrEval
• SDA/DCR correspond to conjunctive/disjunctive ProjectionType
• Developmental trajectory parallels @cite{tieu-kriz-chemla-2019}'s existential→homogeneous shift

inductive Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.DACReading : Type

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

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprDACReading : Repr DACReading

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprDACReading = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprDACReading.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprDACReading.repr : DACReading → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instDecidableEqDACReading : DecidableEq DACReading

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqDACReading : BEq DACReading

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqDACReading = { beq := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqDACReading.beq }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqDACReading.beq : DACReading → DACReading → Bool

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqDACReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.DACReading.strength : DACReading → ℕ

Logical strength ordering: SDA ≥ AR ≥ DCR.

Equations

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

theorem Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.sda_entails_ar : DACReading.sda.strength ≥ DACReading.ar.strength

theorem Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.ar_entails_dcr : DACReading.ar.strength ≥ DACReading.dcr.strength

def Phenomena.Conditionals.Studies.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-santorio-2025}.

Equations

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

theorem Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.alt_semantics_validates_sda {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (domain : List W) (A B C : W → Bool) (w : W) : Semantics.Conditionals.AlternativeSensitive.sdaEval closer domain [A, B] C w = (((Semantics.Conditionals.Counterfactual.closestWorldsB closer domain w (List.filter A domain)).isEmpty || (Semantics.Conditionals.Counterfactual.closestWorldsB closer domain w (List.filter A domain)).all C) && ((Semantics.Conditionals.Counterfactual.closestWorldsB closer domain w (List.filter B domain)).isEmpty || (Semantics.Conditionals.Counterfactual.closestWorldsB closer domain w (List.filter B domain)).all C))

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 Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.ConditionalMode : Type

Conditional mode (indicative vs counterfactual).

• indicative : ConditionalMode
• counterfactual : ConditionalMode

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprConditionalMode.repr : ConditionalMode → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprConditionalMode : Repr ConditionalMode

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprConditionalMode = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprConditionalMode.repr }

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instDecidableEqConditionalMode : DecidableEq ConditionalMode

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqConditionalMode.beq : ConditionalMode → ConditionalMode → Bool

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqConditionalMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqConditionalMode : BEq ConditionalMode

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqConditionalMode = { beq := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqConditionalMode.beq }

inductive Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.AgeGroup : Type

Age groups in the study. Table 1.

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprAgeGroup : Repr AgeGroup

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprAgeGroup = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprAgeGroup.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprAgeGroup.repr : AgeGroup → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instDecidableEqAgeGroup : DecidableEq AgeGroup

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqAgeGroup : BEq AgeGroup

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqAgeGroup = { beq := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqAgeGroup.beq }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqAgeGroup.beq : AgeGroup → AgeGroup → Bool

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqAgeGroup.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.AgeGroup.n : AgeGroup → ℕ

Number of eligible participants per age group. Table 1.

Equations

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.total_children : AgeGroup.age4.n + AgeGroup.age5.n + AgeGroup.age6.n + AgeGroup.age7.n + AgeGroup.age8.n + AgeGroup.age9.n = 148

structure Phenomena.Conditionals.Studies.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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprTargetItem.repr : TargetItem → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprTargetItem : Repr TargetItem

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprTargetItem = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprTargetItem.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.targetItems : List TargetItem

Equations

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

structure Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.PatternRates : Type

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

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprPatternRates : Repr PatternRates

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprPatternRates = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprPatternRates.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprPatternRates.repr : PatternRates → ℕ → Std.Format

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.childrenOverall : PatternRates

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

Equations

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

def Phenomena.Conditionals.Studies.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

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.ar_nearly_absent : childrenOverall.ar < 5 ∧ adultsOverall.ar < 5

Finding 2: AR is nearly absent.

structure Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.ModeRates : Type

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

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprModeRates : Repr ModeRates

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprModeRates = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprModeRates.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprModeRates.repr : ModeRates → ℕ → Std.Format

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.childrenByMode : ModeRates

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.adultsByMode : ModeRates

Equations

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.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

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.halfTrueRefusalRate = 96 / 10

theorem Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.halfTrue_nontrivial : halfTrueRefusalRate > 5

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

structure Phenomena.Conditionals.Studies.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 : ℕ

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprProfileCounts : Repr ProfileCounts

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprProfileCounts = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprProfileCounts.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprProfileCounts.repr : ProfileCounts → ℕ → Std.Format

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.childProfiles : ProfileCounts

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.adultProfiles : ProfileCounts

Equations

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.adults_sda_dominant : adultProfiles.sdaSda = 26

Adults are almost all SDA-consistent.

structure Phenomena.Conditionals.Studies.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 : ℚ

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprNonEquallyRealisticRates : Repr NonEquallyRealisticRates

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprNonEquallyRealisticRates.repr : NonEquallyRealisticRates → ℕ → Std.Format

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.nonEquallyRealistic : NonEquallyRealisticRates

Equations

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.pluralToDACParallel : Plurals.Studies.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

• One or more equations did not get rendered due to their size.
• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.pluralToDACParallel Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.universal = none

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.dacDevelopmentalStage : DACReading → Option Plurals.Studies.TieuKrizChemla2019.DevelopmentalStage

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

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.dacDevelopmentalStage Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.DACReading.ar = none

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

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

theorem Phenomena.Conditionals.Studies.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 Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.SDATheory : Type

Theories of SDA and their predictions about developmental trajectory.

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprSDATheory : Repr SDATheory

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprSDATheory = { reprPrec := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprSDATheory.repr }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instReprSDATheory.repr : SDATheory → ℕ → Std.Format

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instDecidableEqSDATheory : DecidableEq SDATheory

Equations

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

instance Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqSDATheory : BEq SDATheory

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqSDATheory = { beq := Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqSDATheory.beq }

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqSDATheory.beq : SDATheory → SDATheory → Bool

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.instBEqSDATheory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.SDATheory.predictedPreSDA : SDATheory → Option DACReading

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

Equations

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

def Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.observedPreSDA : DACReading

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

Equations

• Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.observedPreSDA = Phenomena.Conditionals.Studies.ZaniCiardelliSanfelici2026.DACReading.dcr

theorem Phenomena.Conditionals.Studies.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.