Chemla and Spector (2011): Experimental evidence for embedded scalar implicatures

Chemla and Spector argue, against Geurts and Pouscoulous, that scalar inferences computed in embedded position are detectable. A graded truth-value judgment rates a picture higher when it satisfies more of a sentence's available readings (§3.2), and the readings a theory makes available are those its mechanism can derive. A restricted globalist computes the inference at the speech-act level only, a localist anywhere, and an unrestricted globalist wherever the result entails the literal reading. Under a universal the local reading entails the literal one, so Experiment 1 separates only the restricted globalist; under exactly one it does not, so Experiment 2 separates the localist from both globalists.

Main results

• exp1_monotone: in Experiment 1 the ratings rise with the number of true readings.
• restrictedGlobalist_strong_eq_weak, localist_weak_ssubset_strong: only the localist predicts the gap between STRONG and WEAK.
• unrestrictedGlobalist_local_eq_false, exp2_false_lt_local: the globalists predict LOCAL to be rated like FALSE, and it is rated far above.
• local_isReinforceable: the local reading passes Sadock's reinforceability diagnostic.
• de_qLocal_lt_both, de_agrees_with_geurts_pouscoulous: the marginal local reading under negation is rated far below the baseline, in line with the fourth experiment of Geurts and Pouscoulous (GeurtsPouscoulous2009.rows_construals_conflict).

Implementation notes

• The unrestricted globalist's reach is the semantic condition that a reading entail the literal one, so its environment-dependence is derived rather than tabulated.
• Section and figure numbers follow the preprint of December 2010 on the Semantics Archive.

References

• [CS11]
• [GP09]
• [Sad78]

Readings and theories (§1)

inductive ChemlaSpector2011.ReadingLabel : Type

The three readings the two experiments cross; their entailments differ between the experiments, which the design exploits.

• literal : ReadingLabel
• global : ReadingLabel
• local_ : ReadingLabel

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqReadingLabel : DecidableEq ReadingLabel

Equations

• ChemlaSpector2011.instDecidableEqReadingLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChemlaSpector2011.instReprReadingLabel : Repr ReadingLabel

Equations

• ChemlaSpector2011.instReprReadingLabel = { reprPrec := ChemlaSpector2011.instReprReadingLabel.repr }

def ChemlaSpector2011.instReprReadingLabel.repr : ReadingLabel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChemlaSpector2011.instFintypeReadingLabel : Fintype ReadingLabel

Equations

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

inductive ChemlaSpector2011.Theory : Type

The three families of theory compute the implicature at the speech-act level only (T1), in embedded position (T2), or globally but with alternatives that need not be stronger than the sentence (T3).

• restrictedGlobalist : Theory
• localist : Theory
• unrestrictedGlobalist : Theory

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqTheory : DecidableEq Theory

Equations

• ChemlaSpector2011.instDecidableEqTheory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChemlaSpector2011.instReprTheory.repr : Theory → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChemlaSpector2011.instReprTheory : Repr Theory

Equations

• ChemlaSpector2011.instReprTheory = { reprPrec := ChemlaSpector2011.instReprTheory.repr }

def ChemlaSpector2011.GloballyDerivable {P : Type u_1} (readings : ReadingLabel → P → Prop) (ℓ : ReadingLabel) : Prop

A globalist derivation reaches a reading exactly when it entails the literal one, since strengthening the matrix meaning never yields something the literal reading does not follow from.

Equations

• ChemlaSpector2011.GloballyDerivable readings ℓ = ∀ (p : P), readings ℓ p → readings ChemlaSpector2011.ReadingLabel.literal p

@[instance_reducible]

instance ChemlaSpector2011.instDecidableGloballyDerivable {P : Type u_1} [Fintype P] (readings : ReadingLabel → P → Prop) [(ℓ : ReadingLabel) → (p : P) → Decidable (readings ℓ p)] (ℓ : ReadingLabel) : Decidable (GloballyDerivable readings ℓ)

Equations

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

def ChemlaSpector2011.Theory.admits {P : Type u_1} (readings : ReadingLabel → P → Prop) : Theory → ReadingLabel → Prop

The readings each theory's mechanism admits.

Equations

• ChemlaSpector2011.Theory.admits readings ChemlaSpector2011.Theory.restrictedGlobalist x✝ = (x✝ = ChemlaSpector2011.ReadingLabel.literal ∨ x✝ = ChemlaSpector2011.ReadingLabel.global)
• ChemlaSpector2011.Theory.admits readings ChemlaSpector2011.Theory.localist x✝ = True
• ChemlaSpector2011.Theory.admits readings ChemlaSpector2011.Theory.unrestrictedGlobalist x✝ = ChemlaSpector2011.GloballyDerivable readings x✝

@[instance_reducible]

instance ChemlaSpector2011.instDecidableAdmits {P : Type u_1} [Fintype P] (readings : ReadingLabel → P → Prop) [(ℓ : ReadingLabel) → (p : P) → Decidable (readings ℓ p)] (t : Theory) (ℓ : ReadingLabel) : Decidable (Theory.admits readings t ℓ)

Equations

• One or more equations did not get rendered due to their size.
• ChemlaSpector2011.instDecidableAdmits readings ChemlaSpector2011.Theory.localist x✝ = { decide := true, reflects_decide := ⋯ }

def ChemlaSpector2011.availableAt {P : Type u_1} [Fintype P] (readings : ReadingLabel → P → Prop) [(ℓ : ReadingLabel) → (p : P) → Decidable (readings ℓ p)] (t : Theory) (p : P) : Finset ReadingLabel

The readings a theory leaves available at a picture are those true there and within its reach; by the conjecture of §3.2 the rating reflects this set.

Equations

• ChemlaSpector2011.availableAt readings t p = {ℓ : ChemlaSpector2011.ReadingLabel | readings ℓ p ∧ ChemlaSpector2011.Theory.admits readings t ℓ}

@[reducible, inline]

abbrev ChemlaSpector2011.RatingsMonotone (data : List (ℕ × ℕ)) : Prop

The conjecture of §3.2 says that where strictly more of a sentence's available readings are true, the rating is higher; it is stated over pairs of a rating and a reading count.

Equations

• ChemlaSpector2011.RatingsMonotone data = List.Pairwise (fun (d₁ d₂ : ℕ × ℕ) => d₁.2 < d₂.2 → d₁.1 < d₂.1) data

Pictures (§3, Appendix 2)

@[reducible, inline]

abbrev ChemlaSpector2011.Picture6 : Type

A six-letter picture places each letter at a vertex of the triangle of opposition, a falsifier being connected to none of its circles (E), a strong verifier to some but not all (IO), and a weak verifier to all (A) (Figure 14).

Equations

• ChemlaSpector2011.Picture6 = (Fin 6 → Aristotelian.Triangle)

@[reducible, inline]

abbrev ChemlaSpector2011.Picture3 : Type

A three-letter picture.

Equations

• ChemlaSpector2011.Picture3 = (Fin 3 → Aristotelian.Triangle)

Experiment 1: scalar items under a universal (§4)

def ChemlaSpector2011.Exp1Some.reading {ι : Type u_1} : ReadingLabel → (ι → Aristotelian.Triangle) → Prop

The three readings of (8) over any domain of letters are (10a), each letter is connected with at least one of its circles, (10b), that and not every letter with all of them, and (10c), every letter with some but not all of them.

Equations

• ChemlaSpector2011.Exp1Some.reading ChemlaSpector2011.ReadingLabel.literal = fun (p : ι → Aristotelian.Triangle) => ∀ (i : ι), ⊥ < p i
• ChemlaSpector2011.Exp1Some.reading ChemlaSpector2011.ReadingLabel.global = fun (p : ι → Aristotelian.Triangle) => (∀ (i : ι), ⊥ < p i) ∧ ¬∀ (i : ι), p i = ⊤
• ChemlaSpector2011.Exp1Some.reading ChemlaSpector2011.ReadingLabel.local_ = fun (p : ι → Aristotelian.Triangle) => ∀ (i : ι), p i = Aristotelian.Triangle.IO

@[instance_reducible]

instance ChemlaSpector2011.Exp1Some.instDecidableReadingOfFintype {ι : Type u_1} [Fintype ι] (ℓ : ReadingLabel) (p : ι → Aristotelian.Triangle) : Decidable (reading ℓ p)

Equations

• One or more equations did not get rendered due to their size.
• ChemlaSpector2011.Exp1Some.instDecidableReadingOfFintype ChemlaSpector2011.ReadingLabel.literal x✝ = { decide := decide (∀ a ∈ Finset.univ, (fun (x : ι) => ⊥ < x✝ x) a), reflects_decide := ⋯ }
• ChemlaSpector2011.Exp1Some.instDecidableReadingOfFintype ChemlaSpector2011.ReadingLabel.global x✝ = { decide := decide (∀ (i : ι), ⊥ < x✝ i) && decide ¬∀ (i : ι), x✝ i = ⊤, reflects_decide := ⋯ }

theorem ChemlaSpector2011.Exp1Some.reading_local_iff {ι : Type u_1} (p : ι → Aristotelian.Triangle) : reading ReadingLabel.local_ p ↔ reading ReadingLabel.literal p ∧ ∀ (i : ι), p i < ⊤

The local reading is the literal one with all denied of every letter.

theorem ChemlaSpector2011.Exp1Some.local_globallyDerivable {ι : Type u_1} : GloballyDerivable reading ReadingLabel.local_

Under the universal the local reading entails the literal one, which keeps the unrestricted globalist abreast of the localist throughout Experiment 1.

inductive ChemlaSpector2011.Exp1Condition : Type

The target conditions of Experiment 1 (§4.2.1) make no reading true, only the literal one, the literal and global ones, or all three.

• false_ : Exp1Condition
• literal : Exp1Condition
• weak : Exp1Condition
• strong : Exp1Condition

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqExp1Condition : DecidableEq Exp1Condition

Equations

• ChemlaSpector2011.instDecidableEqExp1Condition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChemlaSpector2011.instReprExp1Condition : Repr Exp1Condition

Equations

• ChemlaSpector2011.instReprExp1Condition = { reprPrec := ChemlaSpector2011.instReprExp1Condition.repr }

def ChemlaSpector2011.instReprExp1Condition.repr : Exp1Condition → ℕ → Std.Format

Equations

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

def ChemlaSpector2011.Exp1Condition.witness : Exp1Condition → Picture6

The picture of each condition (Figure 4) has six falsifiers, six weak verifiers, four weak and two strong verifiers, or six strong verifiers.

Equations

• ChemlaSpector2011.Exp1Condition.false_.witness = fun (x : Fin 6) => Aristotelian.Triangle.E
• ChemlaSpector2011.Exp1Condition.literal.witness = fun (x : Fin 6) => Aristotelian.Triangle.A
• ChemlaSpector2011.Exp1Condition.weak.witness = fun (i : Fin 6) => if ↑i < 4 then Aristotelian.Triangle.A else Aristotelian.Triangle.IO
• ChemlaSpector2011.Exp1Condition.strong.witness = fun (x : Fin 6) => Aristotelian.Triangle.IO

def ChemlaSpector2011.Exp1Condition.truthSet (c : Exp1Condition) : Finset ReadingLabel

The readings true at a condition, read off its witness.

Equations

• c.truthSet = {x : ChemlaSpector2011.ReadingLabel | ChemlaSpector2011.Exp1Some.reading x c.witness}

def ChemlaSpector2011.Exp1Condition.key : Exp1Condition → String

The row key of a condition.

Equations

• ChemlaSpector2011.Exp1Condition.false_.key = "false"
• ChemlaSpector2011.Exp1Condition.literal.key = "literal"
• ChemlaSpector2011.Exp1Condition.weak.key = "weak"
• ChemlaSpector2011.Exp1Condition.strong.key = "strong"

Experiment 2: scalar items under exactly one (§5)

@[reducible, inline]

abbrev ChemlaSpector2011.Exp2Some.literal (p : Picture3) : Prop

Reading (19a) says that exactly one letter is connected with some or all of its circles, the others with none.

Equations

• ChemlaSpector2011.Exp2Some.literal p = ∃ (i : Fin 3), ⊥ < p i ∧ ∀ (j : Fin 3), j ≠ i → p j = Aristotelian.Triangle.E

@[reducible, inline]

abbrev ChemlaSpector2011.Exp2Some.global (p : Picture3) : Prop

Reading (19b) says that exactly one letter is connected with some but not all of its circles, the others with none.

Equations

• ChemlaSpector2011.Exp2Some.global p = ((∃ (i : Fin 3), p i = Aristotelian.Triangle.IO ∧ ∀ (j : Fin 3), j ≠ i → p j = Aristotelian.Triangle.E) ∧ ∀ (i : Fin 3), p i ≠ Aristotelian.Triangle.A)

@[reducible, inline]

abbrev ChemlaSpector2011.Exp2Some.local_ (p : Picture3) : Prop

Reading (19c) says that exactly one letter is connected with some but not all of its circles, the others with none or all.

Equations

• ChemlaSpector2011.Exp2Some.local_ p = ∃ (i : Fin 3), p i = Aristotelian.Triangle.IO ∧ ∀ (j : Fin 3), j ≠ i → p j ≠ Aristotelian.Triangle.IO

def ChemlaSpector2011.Exp2Some.reading : ReadingLabel → Picture3 → Prop

The three readings of (21).

Equations

• ChemlaSpector2011.Exp2Some.reading ChemlaSpector2011.ReadingLabel.literal = ChemlaSpector2011.Exp2Some.literal
• ChemlaSpector2011.Exp2Some.reading ChemlaSpector2011.ReadingLabel.global = ChemlaSpector2011.Exp2Some.global
• ChemlaSpector2011.Exp2Some.reading ChemlaSpector2011.ReadingLabel.local_ = ChemlaSpector2011.Exp2Some.local_

@[instance_reducible]

instance ChemlaSpector2011.Exp2Some.instDecidableReading (ℓ : ReadingLabel) (p : Picture3) : Decidable (reading ℓ p)

Equations

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

theorem ChemlaSpector2011.Exp2Some.local_not_globallyDerivable : ¬GloballyDerivable reading ReadingLabel.local_

Under exactly one the local reading no longer entails the literal one, since a strong verifier among weak verifiers makes it true and the literal reading false, which puts it beyond a globalist derivation's reach (§5.1).

inductive ChemlaSpector2011.Exp2Condition : Type

The target conditions of Experiment 2 (§5.3.1) make no reading true, only the literal one, only the local one, or all three.

• false_ : Exp2Condition
• literal : Exp2Condition
• local_ : Exp2Condition
• all : Exp2Condition

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqExp2Condition : DecidableEq Exp2Condition

Equations

• ChemlaSpector2011.instDecidableEqExp2Condition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChemlaSpector2011.instReprExp2Condition.repr : Exp2Condition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChemlaSpector2011.instReprExp2Condition : Repr Exp2Condition

Equations

• ChemlaSpector2011.instReprExp2Condition = { reprPrec := ChemlaSpector2011.instReprExp2Condition.repr }

def ChemlaSpector2011.Exp2Condition.witness : Exp2Condition → Picture3

A picture of each condition (Figure 11).

Equations

• ChemlaSpector2011.Exp2Condition.false_.witness = fun (x : Fin 3) => Aristotelian.Triangle.E
• ChemlaSpector2011.Exp2Condition.literal.witness = fun (i : Fin 3) => if ↑i = 0 then Aristotelian.Triangle.A else Aristotelian.Triangle.E
• ChemlaSpector2011.Exp2Condition.local_.witness = fun (i : Fin 3) => if ↑i = 0 then Aristotelian.Triangle.IO else Aristotelian.Triangle.A
• ChemlaSpector2011.Exp2Condition.all.witness = fun (i : Fin 3) => if ↑i = 0 then Aristotelian.Triangle.IO else Aristotelian.Triangle.E

def ChemlaSpector2011.Exp2Condition.truthSet (c : Exp2Condition) : Finset ReadingLabel

The readings true at a condition, read off its witness.

Equations

• c.truthSet = {x : ChemlaSpector2011.ReadingLabel | ChemlaSpector2011.Exp2Some.reading x c.witness}

def ChemlaSpector2011.Exp2Condition.key : Exp2Condition → String

The row key of a condition.

Equations

• ChemlaSpector2011.Exp2Condition.false_.key = "false"
• ChemlaSpector2011.Exp2Condition.literal.key = "literal"
• ChemlaSpector2011.Exp2Condition.local_.key = "local"
• ChemlaSpector2011.Exp2Condition.all.key = "all"

inductive ChemlaSpector2011.DEControlCondition : Type

The downward-entailing controls (12) and (13) at the end of each experiment (§4.2.2) make no reading true, only the marginal local reading, or both readings.

• false_ : DEControlCondition
• qLocal : DEControlCondition
• both : DEControlCondition

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqDEControlCondition : DecidableEq DEControlCondition

Equations

• ChemlaSpector2011.instDecidableEqDEControlCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChemlaSpector2011.instReprDEControlCondition.repr : DEControlCondition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ChemlaSpector2011.instReprDEControlCondition : Repr DEControlCondition

Equations

• ChemlaSpector2011.instReprDEControlCondition = { reprPrec := ChemlaSpector2011.instReprDEControlCondition.repr }

def ChemlaSpector2011.DEControlCondition.key : DEControlCondition → String

The row key of a condition.

Equations

• ChemlaSpector2011.DEControlCondition.false_.key = "false"
• ChemlaSpector2011.DEControlCondition.qLocal.key = "qlocal"
• ChemlaSpector2011.DEControlCondition.both.key = "both"

The rows

inductive ChemlaSpector2011.Experiment : Type

The two experiments.

• one : Experiment
• two : Experiment

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqExperiment : DecidableEq Experiment

Equations

• ChemlaSpector2011.instDecidableEqExperiment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChemlaSpector2011.instReprExperiment : Repr Experiment

Equations

• ChemlaSpector2011.instReprExperiment = { reprPrec := ChemlaSpector2011.instReprExperiment.repr }

def ChemlaSpector2011.instReprExperiment.repr : Experiment → ℕ → Std.Format

Equations

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

def ChemlaSpector2011.Experiment.key : Experiment → String

Equations

• ChemlaSpector2011.Experiment.one.key = "1"
• ChemlaSpector2011.Experiment.two.key = "2"

inductive ChemlaSpector2011.Item : Type

The two scalar items, certains and ou.

• some : Item
• or : Item

@[instance_reducible]

instance ChemlaSpector2011.instDecidableEqItem : DecidableEq Item

Equations

• ChemlaSpector2011.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChemlaSpector2011.instReprItem : Repr Item

Equations

• ChemlaSpector2011.instReprItem = { reprPrec := ChemlaSpector2011.instReprItem.repr }

def ChemlaSpector2011.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

def ChemlaSpector2011.Item.key : Item → String

Equations

• ChemlaSpector2011.Item.some.key = "some"
• ChemlaSpector2011.Item.or.key = "or"

def ChemlaSpector2011.rating (e : Experiment) (i : Item) (env cond : String) : Option ℕ

The mean rating, in per-mille, of an item in a condition of an experiment.

Equations

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

def ChemlaSpector2011.rating₁ (i : Item) (c : Exp1Condition) : Option ℕ

The rating of a target condition of Experiment 1.

Equations

• ChemlaSpector2011.rating₁ i c = ChemlaSpector2011.rating ChemlaSpector2011.Experiment.one i "universal" c.key

def ChemlaSpector2011.rating₂ (i : Item) (c : Exp2Condition) : Option ℕ

The rating of a target condition of Experiment 2.

Equations

• ChemlaSpector2011.rating₂ i c = ChemlaSpector2011.rating ChemlaSpector2011.Experiment.two i "exactlyOne" c.key

def ChemlaSpector2011.ratingDE (e : Experiment) (i : Item) (c : DEControlCondition) : Option ℕ

The rating of a downward-entailing control.

Equations

• ChemlaSpector2011.ratingDE e i c = ChemlaSpector2011.rating e i "de" c.key

Experiment 1

theorem ChemlaSpector2011.exp1_monotone (i : Item) : ∃ r₀ ∈ rating₁ i Exp1Condition.false_, ∃ r₁ ∈ rating₁ i Exp1Condition.literal, ∃ r₂ ∈ rating₁ i Exp1Condition.weak, ∃ r₃ ∈ rating₁ i Exp1Condition.strong, RatingsMonotone [(r₀, Exp1Condition.false_.truthSet.card), (r₁, Exp1Condition.literal.truthSet.card), (r₂, Exp1Condition.weak.truthSet.card), (r₃, Exp1Condition.strong.truthSet.card)]

In Figure 5 the ratings of both items rise with the readings true at the condition's witness, the conjecture of §3.2 on Experiment 1, which subsumes the contrast between STRONG and WEAK that only the truth of the local reading separates.

theorem ChemlaSpector2011.restrictedGlobalist_strong_eq_weak : availableAt Exp1Some.reading Theory.restrictedGlobalist Exp1Condition.strong.witness = availableAt Exp1Some.reading Theory.restrictedGlobalist Exp1Condition.weak.witness

The restricted globalist leaves the same readings available at STRONG as at WEAK, the local reading being true at STRONG but beyond a matrix-only mechanism, so it predicts equal ratings.

theorem ChemlaSpector2011.localist_weak_ssubset_strong : availableAt Exp1Some.reading Theory.localist Exp1Condition.weak.witness ⊂ availableAt Exp1Some.reading Theory.localist Exp1Condition.strong.witness

The localist leaves strictly more available at STRONG than at WEAK and so predicts the gap.

theorem ChemlaSpector2011.localist_eq_unrestrictedGlobalist_exp1 (c : Exp1Condition) : availableAt Exp1Some.reading Theory.localist c.witness = availableAt Exp1Some.reading Theory.unrestrictedGlobalist c.witness

The unrestricted globalist agrees with the localist on every condition of Experiment 1, the local reading being within its reach there, which is why the experiment cannot separate them.

theorem ChemlaSpector2011.local_isReinforceable : Implicature.IsReinforceable (Exp1Some.reading ReadingLabel.literal) (Exp1Some.reading ReadingLabel.local_)

The local reading is reinforceable over the literal one, since at WEAK the literal reading holds and the local one fails.

Experiment 2

theorem ChemlaSpector2011.exp2_local_gt_literal_some : ∃ l ∈ rating₂ Item.some Exp2Condition.local_, ∃ t ∈ rating₂ Item.some Exp2Condition.literal, t < l

In Figure 12 the condition where only the local reading of certains is true is rated above the one where only the literal reading is, though the literal reading is false there.

theorem ChemlaSpector2011.exp2_false_lt_local (i : Item) : ∃ f ∈ rating₂ i Exp2Condition.false_, ∃ l ∈ rating₂ i Exp2Condition.local_, f < l

In Figure 12 the local condition is rated far above the false one for both items.

theorem ChemlaSpector2011.unrestrictedGlobalist_local_eq_false : availableAt Exp2Some.reading Theory.unrestrictedGlobalist Exp2Condition.local_.witness = availableAt Exp2Some.reading Theory.unrestrictedGlobalist Exp2Condition.false_.witness

The unrestricted globalist collapses at the diagnostic condition, where the one reading true at LOCAL is beyond its reach, so it leaves nothing available there, as at FALSE, and predicts equal ratings.

theorem ChemlaSpector2011.localist_false_ssubset_local : availableAt Exp2Some.reading Theory.localist Exp2Condition.false_.witness ⊂ availableAt Exp2Some.reading Theory.localist Exp2Condition.local_.witness

The localist keeps the two apart and predicts the observed gap.

theorem ChemlaSpector2011.localist_ne_unrestrictedGlobalist_local : availableAt Exp2Some.reading Theory.unrestrictedGlobalist Exp2Condition.local_.witness ≠ availableAt Exp2Some.reading Theory.localist Exp2Condition.local_.witness

Where Experiment 1 could not separate the two theories, Experiment 2 does.

The downward-entailing controls (§4.4.4, §5.5.4)

theorem ChemlaSpector2011.de_qLocal_lt_both (e : Experiment) (i : Item) : ∃ q ∈ ratingDE e i DEControlCondition.qLocal, ∃ b ∈ ratingDE e i DEControlCondition.both, q < b

In Figures 6 and 13 the condition where only the marginal local reading is true is rated far below the one where both readings are, in both experiments and for both items.

theorem ChemlaSpector2011.de_qLocal_priming (i : Item) : ∃ a ∈ ratingDE Experiment.one i DEControlCondition.qLocal, ∃ b ∈ ratingDE Experiment.two i DEControlCondition.qLocal, a < b

The same controls are rated higher after the non-monotonic items of Experiment 2 than after Experiment 1, which §5.5.4 attributes to exposure to salient local readings.

theorem ChemlaSpector2011.de_qLocal_lt_local (i : Item) : ∃ q ∈ ratingDE Experiment.two i DEControlCondition.qLocal, ∃ l ∈ rating₂ i Exp2Condition.local_, q < l

Even primed, the local reading under negation stays below the local reading under exactly one (§5.5.4).

theorem ChemlaSpector2011.de_agrees_with_geurts_pouscoulous (i : Item) : ∃ q ∈ ratingDE Experiment.one i DEControlCondition.qLocal, ∃ b ∈ ratingDE Experiment.one i DEControlCondition.both, q < b

The marginal local reading under negation is rated far below the baseline, as the responses consistent with a local implicature fall far below the genuine-ambiguity baseline in the fourth experiment of Geurts and Pouscoulous.