Tieu, Križ & Chemla (2019): Children's Acquisition of Homogeneity

@cite{tieu-kriz-chemla-2019}

Children's acquisition of homogeneity in plural definite descriptions. Frontiers in Psychology 10, 2329.

Core Contribution

Two experiments testing French-speaking children (ages 4--6) on their interpretations of plural definite descriptions in GAP contexts (where some but not all individuals satisfy the predicate), alongside scalar implicature controls. The experiments test predictions of the scalar implicature account of homogeneity (@cite{magri-2014}).

Three Interpretive Patterns

Children presented with "The trucks are blue" / "The trucks aren't blue" in a GAP context (2 of 4 trucks blue) could respond in three ways:

1. Homogeneous (adult-like): reject both positive and negative
2. Existential: accept positive ("some are blue"), reject negative
3. Universal: reject positive, accept negative ("not all are blue")

Key Finding

Three groups of children emerge:

• EXI/−SI: Existential interpretation, no scalar implicatures (the literal existential meaning predicted by @cite{magri-2014})
• HOM/+SI: Homogeneous with implicatures (adult-like, consistent with @cite{magri-2014})
• HOM/−SI: Homogeneous WITHOUT scalar implicatures (problematic for @cite{magri-2014})

The existence of the HOM/−SI group contradicts @cite{magri-2014}'s prediction that homogeneity requires the not-all scalar implicature as a subcomputation. The data suggest that homogeneity and scalar implicatures are independent, with homogeneity acquired earlier.

Connection to Linglib

• Imports Homogeneity.lean for the empirical gap pattern
• Imports Magri2014.lean to test the double-strengthening prediction (end-to-end: inner EXH → double-EXH → ALL → falsified by HOM/−SI data)

inductive Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading : Type

The three possible interpretations a speaker can assign to a plural definite description like "the trucks."

• existential : DefinitePluralReading

  THE ≈ SOME: existential interpretation

• homogeneous : DefinitePluralReading

  THE shows a truth-value gap: homogeneous interpretation

• universal : DefinitePluralReading

  THE ≈ ALL: universal interpretation

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDefinitePluralReading : Repr DefinitePluralReading

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDefinitePluralReading = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDefinitePluralReading.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDefinitePluralReading.repr : DefinitePluralReading → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqDefinitePluralReading : DecidableEq DefinitePluralReading

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqDefinitePluralReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDefinitePluralReading.beq : DefinitePluralReading → DefinitePluralReading → Bool

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDefinitePluralReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDefinitePluralReading : BEq DefinitePluralReading

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDefinitePluralReading = { beq := Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDefinitePluralReading.beq }

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instInhabitedDefinitePluralReading : Inhabited DefinitePluralReading

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instInhabitedDefinitePluralReading = { default := Phenomena.Plurals.Studies.TieuKrizChemla2019.instInhabitedDefinitePluralReading.default }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instInhabitedDefinitePluralReading.default : DefinitePluralReading

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instInhabitedDefinitePluralReading.default = Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.existential

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.GapPrediction : Type

What each interpretive pattern predicts for positive and negative definite descriptions in a GAP context (some but not all satisfy).

• reading : DefinitePluralReading
• acceptPositiveGap : Bool

  Accept "The Xs are P" when only some Xs are P?

• acceptNegativeGap : Bool

  Accept "The Xs aren't P" when only some Xs are P?

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprGapPrediction.repr : GapPrediction → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprGapPrediction : Repr GapPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprGapPrediction = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprGapPrediction.repr }

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqGapPrediction : DecidableEq GapPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqGapPrediction = Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqGapPrediction.decEq

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqGapPrediction.decEq (x✝ x✝¹ : GapPrediction) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqGapPrediction : BEq GapPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqGapPrediction = { beq := Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqGapPrediction.beq }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqGapPrediction.beq : GapPrediction → GapPrediction → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqGapPrediction.beq x✝¹ x✝ = false

def Phenomena.Plurals.Studies.TieuKrizChemla2019.existentialGap : GapPrediction

Existential: accept positive (some are P), reject negative.

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.homogeneousGap : GapPrediction

Homogeneous: reject both positive and negative (the gap).

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.universalGap : GapPrediction

Universal: reject positive (not all are P), accept negative.

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.allGapPredictions : List GapPrediction

Equations

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

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.patterns_distinct_responses : existentialGap.acceptPositiveGap ≠ homogeneousGap.acceptPositiveGap ∧ homogeneousGap.acceptNegativeGap ≠ universalGap.acceptNegativeGap

The three patterns are mutually exclusive: no two agree on both responses.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.homogeneous_matches_gap_data : homogeneousGap.acceptPositiveGap = false ∧ homogeneousGap.acceptNegativeGap = false ∧ Homogeneity.switchesExample.positiveInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse ∧ Homogeneity.switchesExample.negativeInGap = Homogeneity.HomogeneityJudgment.neitherTrueNorFalse

The homogeneous pattern matches the empirical gap data in Homogeneity.lean: both positive and negative are judged "neither true nor false."

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.ParticipantGroup : Type

A participant group defined by their definite plural interpretation and whether they compute scalar implicatures.

• reading : DefinitePluralReading

  How they interpret the definite plural

• computesImplicatures : Bool

  Whether they compute the "not-all" scalar implicature

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprParticipantGroup.repr : ParticipantGroup → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprParticipantGroup : Repr ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprParticipantGroup = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprParticipantGroup.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqParticipantGroup.decEq (x✝ x✝¹ : ParticipantGroup) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqParticipantGroup : DecidableEq ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqParticipantGroup = Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqParticipantGroup.decEq

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqParticipantGroup.beq : ParticipantGroup → ParticipantGroup → Bool

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqParticipantGroup.beq { reading := a, computesImplicatures := a_1 } { reading := b, computesImplicatures := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqParticipantGroup.beq x✝¹ x✝ = false

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqParticipantGroup : BEq ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqParticipantGroup = { beq := Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqParticipantGroup.beq }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.allGroups : List ParticipantGroup

The six logically possible groups.

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exiMinusSI : ParticipantGroup

Shorthand for the key groups.

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exiMinusSI = { reading := Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.existential, computesImplicatures := false }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exiPlusSI : ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exiPlusSI = { reading := Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.existential, computesImplicatures := true }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.homMinusSI : ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.homMinusSI = { reading := Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.homogeneous, computesImplicatures := false }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.homPlusSI : ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.homPlusSI = { reading := Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.homogeneous, computesImplicatures := true }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.uniMinusSI : ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.uniMinusSI = { reading := Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.universal, computesImplicatures := false }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.uniPlusSI : ParticipantGroup

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.uniPlusSI = { reading := Phenomena.Plurals.Studies.TieuKrizChemla2019.DefinitePluralReading.universal, computesImplicatures := true }

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.ImplicatureAccountPrediction : Type

The scalar implicature account of homogeneity (@cite{magri-2014}) makes specific predictions about the developmental trajectory.

Since homogeneity is derived via double exhaustification, and the inner EXH computes the "not-all" scalar implicature, two predictions follow:

1. SI-prerequisite: Children who cannot compute the "not-all" implicature cannot derive homogeneous readings. Therefore the HOM/−SI group should not exist.

2. SI-not-rarer: The "not-all" implicature is a subcomputation of the homogeneity implicature. So homogeneous readings should not be more frequent than scalar implicatures.

• siPrerequisite : Bool

  SI is a prerequisite for homogeneity

• homWithoutSIPossible : Bool

  Therefore HOM/−SI should not exist

• siNotRarerThanHom : Bool

  SI should not be rarer than homogeneity

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureAccountPrediction.repr : ImplicatureAccountPrediction → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureAccountPrediction : Repr ImplicatureAccountPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureAccountPrediction = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureAccountPrediction.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqImplicatureAccountPrediction.decEq (x✝ x✝¹ : ImplicatureAccountPrediction) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqImplicatureAccountPrediction : DecidableEq ImplicatureAccountPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqImplicatureAccountPrediction = Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqImplicatureAccountPrediction.decEq

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqImplicatureAccountPrediction.beq : ImplicatureAccountPrediction → ImplicatureAccountPrediction → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqImplicatureAccountPrediction.beq x✝¹ x✝ = false

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqImplicatureAccountPrediction : BEq ImplicatureAccountPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqImplicatureAccountPrediction = { beq := Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqImplicatureAccountPrediction.beq }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.magriPrediction : ImplicatureAccountPrediction

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.magriPrediction = { siPrerequisite := true, homWithoutSIPossible := false, siNotRarerThanHom := true }

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.Exp1GroupCounts : Type

Experiment 1: Truth Value Judgment Task with binary (yes/no) responses.

Participants: 24 French-speaking children (ages 4;04–5;03, M = 4;09) and 22 adults. Children tested at preschools in Paris.

Materials: 6 homogeneity targets (3 positive + 3 negative THE-sentences in GAP contexts), 8 definite description controls, 6 universal quantification controls, 4 scalar implicature targets.

• group : String

  Group label

• adults : Nat

  Number of adults in this group

• children : Nat

  Number of children in this group

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1GroupCounts.repr : Exp1GroupCounts → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1GroupCounts : Repr Exp1GroupCounts

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1GroupCounts = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1GroupCounts.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1_table1 : List Exp1GroupCounts

Experiment 1, Table 1: Distribution of participants by homogeneity pattern and implicature status.

Categories defined by majority response (≥2/3 trials).

Equations

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

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.Exp1BayesianGroups : Type

Experiment 1, Table 3: Bayesian model group assignments for children.

The model confirmed the descriptive categorization: children were unambiguously assigned to groups with posterior probability > 0.92.

• homMinusSI : Nat

  HOM/−SI children

• homPlusSI : Nat

  HOM/+SI children

• exiMinusSI : Nat

  EXI/−SI children

• exiPlusSI : Nat

  EXI/+SI children

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1BayesianGroups : Repr Exp1BayesianGroups

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1BayesianGroups = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1BayesianGroups.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp1BayesianGroups.repr : Exp1BayesianGroups → Nat → Std.Format

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1Children : Exp1BayesianGroups

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1Children = { homMinusSI := 6, homPlusSI := 10, exiMinusSI := 7, exiPlusSI := 1 }

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1_total_children : exp1Children.homMinusSI + exp1Children.homPlusSI + exp1Children.exiMinusSI + exp1Children.exiPlusSI = 24

Total children in Experiment 1.

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.Exp2GroupCounts : Type

Experiment 2: Ternary reward task (minimal / intermediate / maximal).

The ternary paradigm distinguishes truly homogeneous readings from wide-scope universals: a homogeneous reading yields intermediate rewards for both positive and negative GAP sentences, while a wide-scope universal yields minimal for both.

Participants: 24 French-speaking children (ages 4;07–6;04, M = 5;03) and 25 adults. Additional controls for incomplete description, partial truth, and scope ambiguity effects.

Categorization criteria (ternary):

• EXISTENTIAL: maximal for ≥2/3 positive GAP, minimal for ≥2/3 negative GAP
• HOMOGENEOUS: ≤ intermediate for ≥2/3 positive AND ≥2/3 negative GAP
• UNIVERSAL: minimal for ≥2/3 positive GAP, maximal for ≥2/3 negative GAP

• group : String

  Group label

• adults : Nat

  Number of adults

• children : Nat

  Number of children

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp2GroupCounts : Repr Exp2GroupCounts

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp2GroupCounts = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp2GroupCounts.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprExp2GroupCounts.repr : Exp2GroupCounts → Nat → Std.Format

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2_table6 : List Exp2GroupCounts

Experiment 2, Table 6: Distribution of participants by homogeneity pattern and implicature status.

Equations

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

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2_table7 : List Exp2GroupCounts

Experiment 2, Table 7: After conservative exclusions (eliminating participants with potential biases for incomplete description, partial truth, or scope ambiguity).

Equations

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

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.ThreeGroupFinding : Type

The central empirical finding, replicated across both experiments: three distinct groups of children.

• existentialNoSI : Nat

  EXI/−SI: existential, no implicatures (literal meaning)

• homogeneousPlusSI : Nat

  HOM/+SI: homogeneous with implicatures (adult-like)

• homogeneousNoSI : Nat

  HOM/−SI: homogeneous WITHOUT implicatures (problematic for Magri)

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprThreeGroupFinding.repr : ThreeGroupFinding → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprThreeGroupFinding : Repr ThreeGroupFinding

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprThreeGroupFinding = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprThreeGroupFinding.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1Finding : ThreeGroupFinding

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1Finding = { existentialNoSI := 7, homogeneousPlusSI := 10, homogeneousNoSI := 6 }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2Finding : ThreeGroupFinding

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2Finding = { existentialNoSI := 10, homogeneousPlusSI := 7, homogeneousNoSI := 5 }

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1_findings_consistent : exp1Finding.homogeneousNoSI = exp1Children.homMinusSI ∧ exp1Finding.homogeneousPlusSI = exp1Children.homPlusSI ∧ exp1Finding.existentialNoSI = exp1Children.exiMinusSI

Cross-consistency: ThreeGroupFinding (Section 6) matches BayesianGroups (Table 3). Changing either without updating the other will break this theorem.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2_total_categorized : exp2Finding.existentialNoSI + exp2Finding.homogeneousPlusSI + exp2Finding.homogeneousNoSI = 22

Total categorized children in Experiment 2 (2 children gave inconsistent responses and are excluded).

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.hom_without_si_exists_exp1 : exp1Finding.homogeneousNoSI > 0

The HOM/−SI group exists in BOTH experiments.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.hom_without_si_exists_exp2 : exp2Finding.homogeneousNoSI > 0

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.hom_without_si_nontrivial : exp1Finding.homogeneousNoSI ≥ 5 ∧ exp2Finding.homogeneousNoSI ≥ 5

The HOM/−SI group is non-trivial (not a single outlier). Table 4 confirms this: removing HOM/−SI from the Bayesian model degrades fit by Δ_elpd = 50.79 (se = 9.87), over 5 SEs.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.three_groups_cover_exp1 : exp1Finding.existentialNoSI + exp1Finding.homogeneousPlusSI + exp1Finding.homogeneousNoSI = 23

The three key groups (EXI/−SI, HOM/+SI, HOM/−SI) account for 23 of 24 children in Exp 1 (the remaining child was EXI/+SI). No child showed the UNIVERSAL pattern in either experiment, ruling out children simply assigning universal meaning to the definite plural.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.magri_prediction_falsified : magriPrediction.homWithoutSIPossible = false ∧ exp1Finding.homogeneousNoSI > 0 ∧ exp2Finding.homogeneousNoSI > 0

Magri's prediction: homogeneity requires the "not-all" scalar implicature as a subcomputation. Therefore the HOM/−SI group should not exist.

The data falsify this: HOM/−SI children exist in both experiments.

structure Phenomena.Plurals.Studies.TieuKrizChemla2019.ImplicatureHomogeneityRates : Type

The second prediction — that SI should not be rarer than homogeneity — is also challenged. Among children, homogeneous readings are more prevalent than implicature computation:

• Exp 1: 16 homogeneous vs 11 +SI
• Exp 2: 12 homogeneous vs 7 +SI

The implication between SI and homogeneity is unidirectional in development: implicatures imply homogeneity, but not vice versa.

• totalHomogeneous : Nat

  Total children with homogeneous readings

• totalPlusSI : Nat

  Total children computing implicatures

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureHomogeneityRates.repr : ImplicatureHomogeneityRates → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureHomogeneityRates : Repr ImplicatureHomogeneityRates

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureHomogeneityRates = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprImplicatureHomogeneityRates.repr }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1Rates : ImplicatureHomogeneityRates

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exp1Rates = { totalHomogeneous := 16, totalPlusSI := 11 }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2Rates : ImplicatureHomogeneityRates

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.exp2Rates = { totalHomogeneous := 12, totalPlusSI := 7 }

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.homogeneity_more_prevalent : exp1Rates.totalHomogeneous > exp1Rates.totalPlusSI ∧ exp2Rates.totalHomogeneous > exp2Rates.totalPlusSI

In both experiments, homogeneous readings outnumber implicatures.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.unidirectional_implication : exp1Children.homPlusSI = 10 ∧ exp1Children.exiPlusSI = 1 ∧ exp2Finding.homogeneousPlusSI = 7

The implication is unidirectional: all +SI children are homogeneous (with one exception in Exp 1), but not all homogeneous children compute SI.

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.magri_derivation_requires_si : (∀ (s : Magri2014.Scenario), Magri2014.exh Magri2014.Role.weak s = (Magri2014.someMeaning s && !Magri2014.allMeaning s)) ∧ (∀ (s : Magri2014.Scenario), Magri2014.exh Magri2014.Role.mystery s = Magri2014.someMeaning s) ∧ (∀ (s : Magri2014.Scenario), s.total ≥ 1 → Magri2014.doubleExh Magri2014.Role.mystery s = Magri2014.allMeaning s) ∧ exp1Finding.homogeneousNoSI > 0 ∧ exp2Finding.homogeneousNoSI > 0

End-to-end argumentation chain connecting @cite{magri-2014}'s theory (formalized in Magri2014.lean) to the empirical data in this file.

The derivation (examples 10-11 in the paper):

EXH(SOME) = SOME ∧ ¬ALL -- inner EXH: the "not-all" SI EXH(THE) = THE = SOME -- inner EXH: vacuous (no excludable mates) EXH(EXH(THE)) = SOME ∧ ¬(SOME ∧ ¬ALL) = ALL -- outer EXH: negates the SI

The prediction: Since EXH(SOME) = SOME ∧ ¬ALL is a subcomputation of EXH(EXH(THE)) = ALL, a child who cannot compute the "not-all" SI cannot derive the universal reading. Without the SI to negate, double exhaustification is vacuous: EXH(EXH(THE)) = EXH(THE) = SOME. Such children should show the existential pattern, not the homogeneous pattern.

The falsification: HOM/−SI children exist in both experiments — they show homogeneity without computing the SI. This requires an alternative source of homogeneity independent of scalar implicatures.

This theorem imports three results from Magri2014.lean (the inner EXH identity, the vacuousness of single EXH for THE, and the main double- strengthening theorem) and combines them with the empirical data.

inductive Phenomena.Plurals.Studies.TieuKrizChemla2019.DevelopmentalStage : Type

The paper proposes the following developmental trajectory:

Stage 1: Children start with the literal existential meaning of the definite plural (EXI pattern). This is compatible with @cite{magri-2014}'s assumption that the plain meaning of THE is existential.

Stage 2: Children acquire homogeneous readings, possibly through a mechanism independent of scalar implicatures.

Stage 3: Children acquire scalar implicatures. Those who arrived at homogeneity through implicatures now have both; those who arrived through another mechanism also have both.

The key insight: stages 2 and 3 are INDEPENDENT. Homogeneity does not require scalar implicatures as a developmental prerequisite.

• existential : DevelopmentalStage
• homogeneous : DevelopmentalStage
• adult : DevelopmentalStage

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDevelopmentalStage.repr : DevelopmentalStage → Nat → Std.Format

Equations

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

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDevelopmentalStage : Repr DevelopmentalStage

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDevelopmentalStage = { reprPrec := Phenomena.Plurals.Studies.TieuKrizChemla2019.instReprDevelopmentalStage.repr }

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqDevelopmentalStage : DecidableEq DevelopmentalStage

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instDecidableEqDevelopmentalStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDevelopmentalStage.beq : DevelopmentalStage → DevelopmentalStage → Bool

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDevelopmentalStage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDevelopmentalStage : BEq DevelopmentalStage

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDevelopmentalStage = { beq := Phenomena.Plurals.Studies.TieuKrizChemla2019.instBEqDevelopmentalStage.beq }

def Phenomena.Plurals.Studies.TieuKrizChemla2019.stageOrder : DevelopmentalStage → Nat

The developmental ordering: existential precedes homogeneous precedes full adult competence.

Equations

• Phenomena.Plurals.Studies.TieuKrizChemla2019.stageOrder Phenomena.Plurals.Studies.TieuKrizChemla2019.DevelopmentalStage.existential = 0
• Phenomena.Plurals.Studies.TieuKrizChemla2019.stageOrder Phenomena.Plurals.Studies.TieuKrizChemla2019.DevelopmentalStage.homogeneous = 1
• Phenomena.Plurals.Studies.TieuKrizChemla2019.stageOrder Phenomena.Plurals.Studies.TieuKrizChemla2019.DevelopmentalStage.adult = 2

def Phenomena.Plurals.Studies.TieuKrizChemla2019.groupToStage : ParticipantGroup → Option DevelopmentalStage

The three attested child groups map to developmental stages. Returns none for groups not attested in children (UNI/±SI, EXI/+SI with only 1 child).

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Plurals.Studies.TieuKrizChemla2019.groupToStage x✝ = none

theorem Phenomena.Plurals.Studies.TieuKrizChemla2019.attested_groups_ordered : groupToStage exiMinusSI = some DevelopmentalStage.existential ∧ groupToStage homMinusSI = some DevelopmentalStage.homogeneous ∧ groupToStage homPlusSI = some DevelopmentalStage.adult ∧ stageOrder DevelopmentalStage.existential ≤ stageOrder DevelopmentalStage.homogeneous ∧ stageOrder DevelopmentalStage.homogeneous ≤ stageOrder DevelopmentalStage.adult

The three attested groups map to the three developmental stages, and the stages form a monotonically increasing sequence.