Huang, Spelke and Snedeker (2013): What exactly do numbers mean?

Huang, Spelke and Snedeker ask whether number words have exact or lower-bounded semantics by cancelling the scalar implicature that would otherwise supply the upper bound. A trial shows two visible boxes and a covered one, and the instruction is a definite description such as the box with two fish. Its referent under a reading of the term is the visible box satisfying it when exactly one does, the covered box when none does, and no box when both do (choice). Adults and two- to three-year-olds took the total set for some and the covered box for two.

Two-knowers, children who give one and two but a handful for larger numerals in Wynn's Give-N task, are the population for which the lower-bounded account has no implicature to offer, the developmental strategy of Musolino.

Main results

• choice_exact_covered, choice_atLeast_visible: in the critical trials an exact two sends the participant to the covered box and a lower-bounded two to the visible one.
• some_none_all_literal, some_none_all_strengthened: literal some picks the box where Cookie Monster has all of the cookies, strengthened some the covered box.
• exhKnown_last, exhKnown_of_lt: exhaustifying two against a known count list leaves it lower-bounded when it is the top of the list and makes it exact otherwise.
• atLeast_diff_moreThan_eq_bare: an implicit alternative more than two recovers exactness.

Implementation notes

• Scalar trials are typed by the vertices of the triangle of opposition (Aristotelian.Triangle), a box showing Cookie Monster with none, some but not all, or all of the cookies; number trials by the cardinality of a box.
• The choice proportions and the statistics stay in prose: the paradigm's predictions are categorical, and the paper's argument is that the majority choice identifies the reading.

References

• [HSS13]
• [Wyn92]
• [Mus04]

The covered-box task

structure HuangSpelkeSnedeker2013.Trial (α : Type u_1) : Type u_1

A covered-box trial shows two visible boxes with contents of type α beside a covered box.

• left : α
• right : α

inductive HuangSpelkeSnedeker2013.Choice (α : Type u_1) : Type u_1

What the participant hands over.

• visible {α : Type u_1} (x : α) : Choice α
• covered {α : Type u_1} : Choice α

def HuangSpelkeSnedeker2013.instDecidableEqChoice.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Choice α✝) : Decidable (x✝ = x✝¹)

Equations

• HuangSpelkeSnedeker2013.instDecidableEqChoice.decEq (HuangSpelkeSnedeker2013.Choice.visible a) (HuangSpelkeSnedeker2013.Choice.visible b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• HuangSpelkeSnedeker2013.instDecidableEqChoice.decEq (HuangSpelkeSnedeker2013.Choice.visible x_2) HuangSpelkeSnedeker2013.Choice.covered = isFalse ⋯
• HuangSpelkeSnedeker2013.instDecidableEqChoice.decEq HuangSpelkeSnedeker2013.Choice.covered (HuangSpelkeSnedeker2013.Choice.visible x_2) = isFalse ⋯
• HuangSpelkeSnedeker2013.instDecidableEqChoice.decEq HuangSpelkeSnedeker2013.Choice.covered HuangSpelkeSnedeker2013.Choice.covered = isTrue ⋯

@[instance_reducible]

instance HuangSpelkeSnedeker2013.instDecidableEqChoice {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Choice α✝)

Equations

• HuangSpelkeSnedeker2013.instDecidableEqChoice = HuangSpelkeSnedeker2013.instDecidableEqChoice.decEq

def HuangSpelkeSnedeker2013.choice {α : Type u_1} (R : α → Prop) [DecidablePred R] (t : Trial α) : Option (Choice α)

The referent of the definite description under a reading R of the term is the visible box satisfying R when exactly one does, the covered box when none does, and no box when both do, since the description presupposes a unique referent.

Equations

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

theorem HuangSpelkeSnedeker2013.choice_eq_none_iff {α : Type u_1} (R : α → Prop) [DecidablePred R] (t : Trial α) : choice R t = none ↔ R t.left ∧ R t.right

theorem HuangSpelkeSnedeker2013.choice_eq_covered_iff {α : Type u_1} (R : α → Prop) [DecidablePred R] (t : Trial α) : choice R t = some Choice.covered ↔ ¬R t.left ∧ ¬R t.right

The covered box is chosen exactly when no visible box satisfies the description.

theorem HuangSpelkeSnedeker2013.choice_eq_visible_left_iff {α : Type u_1} (R : α → Prop) [DecidablePred R] (t : Trial α) : choice R t = some (Choice.visible t.left) ↔ R t.left ∧ ¬R t.right

theorem HuangSpelkeSnedeker2013.choice_eq_visible_right_iff {α : Type u_1} (R : α → Prop) [DecidablePred R] (t : Trial α) : choice R t = some (Choice.visible t.right) ↔ ¬R t.left ∧ R t.right

theorem HuangSpelkeSnedeker2013.choice_covered_of_le {α : Type u_1} (R : α → Prop) [DecidablePred R] (t : Trial α) {R' : α → Prop} [DecidablePred R'] (h : ∀ (x : α), R' x → R x) (hc : choice R t = some Choice.covered) : choice R' t = some Choice.covered

Strengthening the reading can only move the referent to the covered box or resolve a tie, which is the design of Section 1.4.

Number trials

theorem HuangSpelkeSnedeker2013.choice_exact_covered {m a b : ℕ} (ha : a < m) (hb : m < b) : choice (fun (x : ℕ) => x ∈ Degree.Comparison.eq.interval m) { left := a, right := b } = some Choice.covered

The critical trials show a smaller and a larger set, so an exact numeral has no visible referent and the covered box is chosen.

theorem HuangSpelkeSnedeker2013.choice_atLeast_visible {m a b : ℕ} (ha : a < m) (hb : m ≤ b) : choice (fun (x : ℕ) => x ∈ Degree.Comparison.ge.interval m) { left := a, right := b } = some (Choice.visible b)

A lower-bounded numeral refers to the larger set.

theorem HuangSpelkeSnedeker2013.choice_exhNumeral_covered {m a b : ℕ} (ha : a < m) (hb : m < b) : choice (fun (x : ℕ) => x ∈ Numerals.exhNumeral m) { left := a, right := b } = some Choice.covered

The lower-bounded numeral strengthened against the full number scale chooses like the exact one, so the critical trials separate the two semantics only where the implicature is cancelled.

theorem HuangSpelkeSnedeker2013.choice_one_two_bare : choice (fun (x : ℕ) => x ∈ Degree.Comparison.eq.interval 2) { left := 1, right := 2 } = some (Choice.visible 2)

In two(1,2) an exact match is visible against a smaller set, and both readings pick it.

theorem HuangSpelkeSnedeker2013.choice_one_two_atLeast : choice (fun (x : ℕ) => x ∈ Degree.Comparison.ge.interval 2) { left := 1, right := 2 } = some (Choice.visible 2)

theorem HuangSpelkeSnedeker2013.choice_two_three_bare : choice (fun (x : ℕ) => x ∈ Degree.Comparison.eq.interval 2) { left := 2, right := 3 } = some (Choice.visible 2)

In two(2,3∨5) the lower-bounded reading leaves the description without a unique referent against a larger set, and it is the implicature that restores the exact match.

theorem HuangSpelkeSnedeker2013.choice_two_three_atLeast : choice (fun (x : ℕ) => x ∈ Degree.Comparison.ge.interval 2) { left := 2, right := 3 } = none

theorem HuangSpelkeSnedeker2013.choice_two_three_exh : choice (fun (x : ℕ) => x ∈ Numerals.exhNumeral 2) { left := 2, right := 3 } = some (Choice.visible 2)

theorem HuangSpelkeSnedeker2013.choice_one_three_bare : choice (fun (x : ℕ) => x ∈ Degree.Comparison.eq.interval 2) { left := 1, right := 3 } = some Choice.covered

In the critical trials two(1,3∨5) adults and two-knowers chose the covered box.

theorem HuangSpelkeSnedeker2013.choice_one_three_atLeast : choice (fun (x : ℕ) => x ∈ Degree.Comparison.ge.interval 2) { left := 1, right := 3 } = some (Choice.visible 3)

theorem HuangSpelkeSnedeker2013.choice_one_five_atLeast : choice (fun (x : ℕ) => x ∈ Degree.Comparison.ge.interval 2) { left := 1, right := 5 } = some (Choice.visible 5)

Scalar trials

A box's vertex of the triangle of opposition records whether Cookie Monster has none of the cookies (E), some but not all of them (IO), or all (A). On the scale the vertices form, literal some holds above the bottom, all at the top, and some strengthened by its implicature not all strictly between.

@[reducible, inline]

abbrev HuangSpelkeSnedeker2013.someLiteral : Aristotelian.Triangle → Prop

Literal some holds above the bottom vertex.

Equations

• HuangSpelkeSnedeker2013.someLiteral x✝ = (⊥ < x✝)

@[reducible, inline]

abbrev HuangSpelkeSnedeker2013.allLiteral : Aristotelian.Triangle → Prop

All holds at the top vertex.

Equations

• HuangSpelkeSnedeker2013.allLiteral x✝ = (x✝ = ⊤)

@[reducible, inline]

abbrev HuangSpelkeSnedeker2013.someStrengthened : Aristotelian.Triangle → Prop

Some strengthened by not all holds strictly between the bottom and top vertices.

Equations

• HuangSpelkeSnedeker2013.someStrengthened t = (⊥ < t ∧ t < ⊤)

theorem HuangSpelkeSnedeker2013.some_none_some : choice someLiteral { left := Aristotelian.Triangle.E, right := Aristotelian.Triangle.IO } = some (Choice.visible Aristotelian.Triangle.IO)

In some(NONE,SOME) either reading picks the subset.

theorem HuangSpelkeSnedeker2013.some_some_all_literal : choice someLiteral { left := Aristotelian.Triangle.IO, right := Aristotelian.Triangle.A } = none

In some(SOME,ALL) the literal meaning fits both visible boxes and the implicature selects the subset, which adults chose and children split on.

theorem HuangSpelkeSnedeker2013.some_some_all_strengthened : choice someStrengthened { left := Aristotelian.Triangle.IO, right := Aristotelian.Triangle.A } = some (Choice.visible Aristotelian.Triangle.IO)

theorem HuangSpelkeSnedeker2013.some_none_all_literal : choice someLiteral { left := Aristotelian.Triangle.E, right := Aristotelian.Triangle.A } = some (Choice.visible Aristotelian.Triangle.A)

In some(NONE,ALL), the control for implicature cancellation, the literal meaning picks the total set, which adults and children chose, and the strengthened meaning the covered box.

theorem HuangSpelkeSnedeker2013.some_none_all_strengthened : choice someStrengthened { left := Aristotelian.Triangle.E, right := Aristotelian.Triangle.A } = some Choice.covered

theorem HuangSpelkeSnedeker2013.all_none_all : choice allLiteral { left := Aristotelian.Triangle.E, right := Aristotelian.Triangle.A } = some (Choice.visible Aristotelian.Triangle.A)

In Experiment 3 all selects the total set when visible and the covered box otherwise, so the children's choices tracked the quantifier rather than the character.

theorem HuangSpelkeSnedeker2013.all_some_all : choice allLiteral { left := Aristotelian.Triangle.IO, right := Aristotelian.Triangle.A } = some (Choice.visible Aristotelian.Triangle.A)

theorem HuangSpelkeSnedeker2013.all_some_none : choice allLiteral { left := Aristotelian.Triangle.IO, right := Aristotelian.Triangle.E } = some Choice.covered

Two-knowers

def HuangSpelkeSnedeker2013.exhKnown (k : ℕ) (i : Fin (k + 1)) (n : ℕ) : Prop

A child at knower level k has the numerals up to k as a count list; the numeral i of that list exhaustified against its known stronger alternatives.

Equations

• HuangSpelkeSnedeker2013.exhKnown k i n = Exhaustification.exhAgainst (fun (x1 x2 : Fin (k + 1)) => x1 < x2) (fun (j : Fin (k + 1)) => n ∈ Degree.Comparison.ge.interval ↑j) i

@[instance_reducible]

instance HuangSpelkeSnedeker2013.instDecidablePredNatExhKnown (k : ℕ) (i : Fin (k + 1)) : DecidablePred (exhKnown k i)

Equations

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

theorem HuangSpelkeSnedeker2013.exhKnown_last (k n : ℕ) : exhKnown k (Fin.last k) n ↔ n ∈ Degree.Comparison.ge.interval k

The top of the count list has no stronger known alternative, so exhaustification leaves its lower-bounded meaning as it is.

theorem HuangSpelkeSnedeker2013.exhKnown_of_lt {k : ℕ} {i : Fin (k + 1)} (hi : i < Fin.last k) (n : ℕ) : exhKnown k i n ↔ n ∈ Degree.Comparison.eq.interval ↑i

A numeral below the top is exhaustified to its exact meaning.

theorem HuangSpelkeSnedeker2013.twoKnower_lowerBounded : choice (exhKnown 2 (Fin.last 2)) { left := 1, right := 3 } = some (Choice.visible 3)

A two-knower's count list is one, two, so under lower-bounded semantics two stays lower-bounded and the child should hand over the visible box with three fish, contrary to the covered-box choices of Experiments 2 and 4.

theorem HuangSpelkeSnedeker2013.threeKnower_exact : choice (exhKnown 3 2) { left := 1, right := 3 } = some Choice.covered

A three-knower could reach the covered box through the implicature.

theorem HuangSpelkeSnedeker2013.atLeast_diff_moreThan_eq_bare (m : ℕ) : Degree.Comparison.ge.interval m \ Degree.Comparison.gt.interval m = Degree.Comparison.eq.interval m

An implicit alternative more than two would exhaustify two to its exact meaning, the route Section 6.1 leaves logically open.