Macuch Silva, Lorson, Franke, Cummins and Rohde (2024): Strategic Use of English Quantifiers

This file formalizes the argumentative-difficulty account of [MSLF+24]. Two experiments have English speakers describe exam results, a number of correct answers out of a total, under the goal of presenting the outcome as a success or as a failure, with the four quantifiers all, most, some and none in Experiment 1. The difficulty of framing a result toward a goal is the distance of its proportion of correct answers from the goal's ideal: the proportion itself for a failure framing and its complement for a success framing (difficulty), so the two difficulties of one table sum to one (difficulty_add). The account predicts that as difficulty grows the speaker retreats to informationally weaker quantifiers, all giving way to most and then to some, those truthful over broader ranges of outcomes: truth is inherited down the lexical scale (Truthful.of_le), the strongest truthful quantifier for the goal-congruent adjective is monotone in the count it describes (strongest_mono), and difficulty orders those counts the other way, so the strongest truthful quantifier weakens with difficulty (weakening_with_difficulty). The paper thereby extends the argumentative strength of [CF21] from a property of the speaker's utterance to a property of the situation.

Implementation notes

Proportions and difficulties are rationals. The positive quantifiers form the scale ⟨some, most, all⟩, ordered by rank, and none is the bottom adjoined to it (WithBot): the strongest truthful quantifier is none exactly when the count is zero. The paper's refined difficulty, which also counts the students scoring zero, and the response probabilities of Figure 5 are described in prose.

References

• [MSLF+24]
• [CF21]

inductive MacuchSilvaEtAl2024.Goal : Type

The framing goal: present the results as a success or as a failure.

• highSuccess : Goal
• lowSuccess : Goal

@[instance_reducible]

instance MacuchSilvaEtAl2024.instDecidableEqGoal : DecidableEq Goal

Equations

• MacuchSilvaEtAl2024.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive MacuchSilvaEtAl2024.Adjective : Type

The adjective of the description frame, N students got some questions right/wrong.

• right : Adjective
• wrong : Adjective

@[instance_reducible]

instance MacuchSilvaEtAl2024.instDecidableEqAdjective : DecidableEq Adjective

Equations

• MacuchSilvaEtAl2024.instDecidableEqAdjective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MacuchSilvaEtAl2024.Goal.adjective : Goal → Adjective

The adjective congruent with a goal: right for a success framing, wrong for a failure framing.

Equations

• MacuchSilvaEtAl2024.Goal.highSuccess.adjective = MacuchSilvaEtAl2024.Adjective.right
• MacuchSilvaEtAl2024.Goal.lowSuccess.adjective = MacuchSilvaEtAl2024.Adjective.wrong

structure MacuchSilvaEtAl2024.ExamStimulus : Type

An exam table: the number of correct answers out of the total.

• nCorrect : ℕ
• nTotal : ℕ
• nCorrect_le : self.nCorrect ≤ self.nTotal
• nTotal_pos : 0 < self.nTotal

def MacuchSilvaEtAl2024.ExamStimulus.proportion (s : ExamStimulus) : ℚ

The proportion of correct answers.

Equations

• s.proportion = ↑s.nCorrect / ↑s.nTotal

def MacuchSilvaEtAl2024.ExamStimulus.count (s : ExamStimulus) : Adjective → ℕ

The number of answers the adjective counts.

Equations

• s.count MacuchSilvaEtAl2024.Adjective.right = s.nCorrect
• s.count MacuchSilvaEtAl2024.Adjective.wrong = s.nTotal - s.nCorrect

theorem MacuchSilvaEtAl2024.ExamStimulus.count_le (s : ExamStimulus) (a : Adjective) : s.count a ≤ s.nTotal

No adjective counts more than the total.

theorem MacuchSilvaEtAl2024.ExamStimulus.proportion_le_proportion_iff {s₁ s₂ : ExamStimulus} (h : s₁.nTotal = s₂.nTotal) : s₁.proportion ≤ s₂.proportion ↔ s₁.nCorrect ≤ s₂.nCorrect

def MacuchSilvaEtAl2024.difficulty (s : ExamStimulus) : Goal → ℚ

Argumentative difficulty: the distance of the proportion from the goal's ideal, the proportion itself under a failure framing and its complement under a success framing.

Equations

• MacuchSilvaEtAl2024.difficulty s MacuchSilvaEtAl2024.Goal.highSuccess = 1 - s.proportion
• MacuchSilvaEtAl2024.difficulty s MacuchSilvaEtAl2024.Goal.lowSuccess = s.proportion

theorem MacuchSilvaEtAl2024.difficulty_add (s : ExamStimulus) : difficulty s Goal.highSuccess + difficulty s Goal.lowSuccess = 1

The two framings of one table are complementary in difficulty.

theorem MacuchSilvaEtAl2024.count_le_of_difficulty_le {s₁ s₂ : ExamStimulus} (g : Goal) (h : s₁.nTotal = s₂.nTotal) (hd : difficulty s₁ g ≤ difficulty s₂ g) : s₂.count g.adjective ≤ s₁.count g.adjective

Difficulty orders the goal-congruent counts the other way: the harder the framing, the fewer answers the congruent adjective has to describe.

The quantifier scale

inductive MacuchSilvaEtAl2024.Quantifier : Type

The positive quantifiers of the experiment, the Horn scale ⟨some, most, all⟩.

• some_ : Quantifier
• most : Quantifier
• all : Quantifier

@[instance_reducible]

instance MacuchSilvaEtAl2024.instDecidableEqQuantifier : DecidableEq Quantifier

Equations

• MacuchSilvaEtAl2024.instDecidableEqQuantifier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MacuchSilvaEtAl2024.instFintypeQuantifier : Fintype Quantifier

Equations

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

def MacuchSilvaEtAl2024.Quantifier.rank : Quantifier → ℕ

The position of a quantifier on the scale.

Equations

• MacuchSilvaEtAl2024.Quantifier.some_.rank = 0
• MacuchSilvaEtAl2024.Quantifier.most.rank = 1
• MacuchSilvaEtAl2024.Quantifier.all.rank = 2

@[instance_reducible]

instance MacuchSilvaEtAl2024.instLinearOrderQuantifier : LinearOrder Quantifier

The scale order: some below most below all.

Equations

• MacuchSilvaEtAl2024.instLinearOrderQuantifier = LinearOrder.lift' MacuchSilvaEtAl2024.Quantifier.rank MacuchSilvaEtAl2024.instLinearOrderQuantifier._proof_1

def MacuchSilvaEtAl2024.Truthful (s : ExamStimulus) (a : Adjective) : Quantifier → Prop

The quantifier is truthful of the count the adjective describes.

Equations

• MacuchSilvaEtAl2024.Truthful s a MacuchSilvaEtAl2024.Quantifier.all = (s.count a = s.nTotal)
• MacuchSilvaEtAl2024.Truthful s a MacuchSilvaEtAl2024.Quantifier.most = (s.nTotal < 2 * s.count a)
• MacuchSilvaEtAl2024.Truthful s a MacuchSilvaEtAl2024.Quantifier.some_ = (0 < s.count a)

@[instance_reducible]

instance MacuchSilvaEtAl2024.instDecidablePredQuantifierTruthful (s : ExamStimulus) (a : Adjective) : DecidablePred (Truthful s a)

Equations

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

theorem MacuchSilvaEtAl2024.Truthful.of_le {s : ExamStimulus} {a : Adjective} {q q' : Quantifier} (h : q' ≤ q) (hq : Truthful s a q) : Truthful s a q'

Truth is inherited down the scale: a quantifier below a truthful one is truthful.

def MacuchSilvaEtAl2024.strongest (s : ExamStimulus) (a : Adjective) : WithBot Quantifier

The strongest truthful quantifier: all of a full count, most of a majority, some of any positive count, and none, the bottom of the scale, otherwise.

Equations

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

theorem MacuchSilvaEtAl2024.strongest_eq_bot_iff (s : ExamStimulus) (a : Adjective) : strongest s a = ⊥ ↔ s.count a = 0

None is the strongest description exactly of a zero count.

theorem MacuchSilvaEtAl2024.strongest_truthful (s : ExamStimulus) (a : Adjective) {q : Quantifier} (h : strongest s a = ↑q) : Truthful s a q

theorem MacuchSilvaEtAl2024.Truthful.le_strongest {s : ExamStimulus} {a : Adjective} {q : Quantifier} (hq : Truthful s a q) : ↑q ≤ strongest s a

Every truthful quantifier lies below the strongest one.

theorem MacuchSilvaEtAl2024.strongest_mono {s₁ s₂ : ExamStimulus} (a : Adjective) (h : s₁.nTotal = s₂.nTotal) (hc : s₁.count a ≤ s₂.count a) : strongest s₁ a ≤ strongest s₂ a

The strongest truthful quantifier is monotone in the count: more of the described answers, a stronger quantifier.

theorem MacuchSilvaEtAl2024.weakening_with_difficulty {s₁ s₂ : ExamStimulus} (g : Goal) (h : s₁.nTotal = s₂.nTotal) (hd : difficulty s₁ g ≤ difficulty s₂ g) : strongest s₂ g.adjective ≤ strongest s₁ g.adjective

Weakening with difficulty: between two tables of one size, the harder the framing toward a goal, the weaker the strongest quantifier truthful of the goal-congruent count.