Geurts and Pouscoulous (2009): Embedded implicatures?!?

This file formalizes the theoretical frame of [GP09]'s experimental case against conventionalist theories of scalar implicature ([Chi04b], [Fox07], [CFS08]), which posit a silent exhaustivity operator adjoinable to any clause and predict local scalar inferences systematically. The operator so negates every stronger alternative of its prejacent; under a belief verb the parse with so below the verb yields the local reading, that the agent believes some but not all, and the parse above it the global reading, that the agent believes some and does not believe all (local_reading, so_pair). The paper's Gricean reply is that the local reading follows from the global one whenever the agent is opinionated on the stronger alternative (local_of_global_of_opinionated), while the analogous derivation for a universal quantifier needs a uniformity assumption across the domain (all_not_all_of_uniform) that is far less plausible, so seemingly local inferences are expected under believe and nowhere else.

Mainstream conventionalism predicts the local construal wherever the embedding scope is not downward entailing (PredictsLocalSI, weakly PredictsLocalSIWeak). The third experiment's verification items are reconstructed as situations in which the classical and the local construal of each sentence conflict (rows_construals_conflict); participants answered by the classical construal throughout (rows_observed_classical), against the prediction derived from the scope monotonicity of the five quantifiers (rows_predicted_mainstream).

Implementation notes

• The experiments' response rates (Tables 2–5) are recorded as features of the rows, with the verification and bracketed prediction rates turned into majority responses; the paper's statistical tests and its methodological argument that the inference paradigm inflates rates stay in prose.
• The verification situations are three squares and three circles; the exact figures of the stimuli are not given in the paper, only the conditions they satisfy, which the three situations here meet.
• The paper's remark that lexicalist conventionalism reaches only the local reading is not formalized; so is the syntax-based variant's operator.

References

• [GP09]
• [Chi04b]
• [Fox07]
• [CFS08]
• [Sau04]

The silent exhaustivity operator

def GeurtsPouscoulous2009.so {W : Type u_1} (φ : Set W) (A : Set (Set W)) : Set W

The silent operator of syntax-based conventionalism conjoins the prejacent with the negation of every stronger alternative.

Equations

• GeurtsPouscoulous2009.so φ A = {w : W | w ∈ φ ∧ ∀ ψ ∈ A, ψ ⊂ φ → w ∉ ψ}

theorem GeurtsPouscoulous2009.so_pair {W : Type u_1} {φ ψ : Set W} (h : ψ ⊂ φ) : so φ {φ, ψ} = φ \ ψ

Against the two-membered scale of some and all, the operator returns some but not all.

theorem GeurtsPouscoulous2009.local_reading {W : Type u_1} (R : SetRel W W) {some all : Set W} (h : all ⊂ some) : R.core (so some {some, all}) = R.core some ∩ R.core allᶜ

The parse with the operator below the belief verb, on which the agent believes some and believes not all.

theorem GeurtsPouscoulous2009.local_of_global_of_opinionated {W : Type u_1} (R : SetRel W W) {some all : Set W} (h : all ⊂ some) {w : W} (h₃₁ : w ∈ R.core some) (h₃₂ : w ∉ R.core all) (h₃₃ : w ∈ R.core all ∨ w ∈ R.core allᶜ) : w ∈ R.core (so some {some, all})

The Gricean derivation of a seemingly local inference, on which the parse with the operator above the belief verb says the agent believes some and does not believe all, and an agent opinionated on all then believes not all, which is the local reading.

theorem GeurtsPouscoulous2009.all_not_all_of_uniform {C : Type u_2} {S : Type u_3} (Shot : C → S → Prop) (h₃₆ : ¬∀ (c : C) (s : S), Shot c s) (h₃₈ : (∀ (c : C) (s : S), Shot c s) ∨ ∀ (c : C), ¬∀ (s : S), Shot c s) (c : C) : ¬∀ (s : S), Shot c s

The same derivation for a universal quantifier, where the global implicature that not every customer shot at every salesman yields that none did only under the uniformity assumption that either all or none did.

Monotonicity and the mainstream prediction

def GeurtsPouscoulous2009.PredictsLocalSI {α : Type u_2} (Q : Quantifier.GQ α) : Prop

The stronger mainstream prediction, that a local scalar inference is preferred in every scope that is not downward entailing.

Equations

• GeurtsPouscoulous2009.PredictsLocalSI Q = ¬Q.ScopeAntitone

def GeurtsPouscoulous2009.PredictsLocalSIWeak {α : Type u_2} (Q : Quantifier.GQ α) : Prop

The weaker prediction, that a local scalar inference is preferred in upward-entailing scopes.

Equations

• GeurtsPouscoulous2009.PredictsLocalSIWeak Q = Q.ScopeMonotone

inductive GeurtsPouscoulous2009.Quant : Type

The quantifiers over squares of the third experiment's sentences.

• all : Quant
• moreThanOne : Quant
• exactlyTwo : Quant
• notAll : Quant
• notMoreThanOne : Quant

@[instance_reducible]

instance GeurtsPouscoulous2009.instDecidableEqQuant : DecidableEq Quant

Equations

• GeurtsPouscoulous2009.instDecidableEqQuant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GeurtsPouscoulous2009.instReprQuant.repr : Quant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GeurtsPouscoulous2009.instReprQuant : Repr Quant

Equations

• GeurtsPouscoulous2009.instReprQuant = { reprPrec := GeurtsPouscoulous2009.instReprQuant.repr }

noncomputable def GeurtsPouscoulous2009.Quant.sem {α : Type u_2} [Fintype α] : Quant → Quantifier.GQ α

Equations

• GeurtsPouscoulous2009.Quant.all.sem = Quantifier.GQ.every
• GeurtsPouscoulous2009.Quant.moreThanOne.sem = Quantifier.GQ.atLeast 2
• GeurtsPouscoulous2009.Quant.exactlyTwo.sem = Quantifier.GQ.exactly 2
• GeurtsPouscoulous2009.Quant.notAll.sem = Quantifier.GQ.everyᶜ
• GeurtsPouscoulous2009.Quant.notMoreThanOne.sem = Quantifier.GQ.atMost 1

theorem GeurtsPouscoulous2009.all_predictsLocalSIWeak {α : Type u_2} [Fintype α] : PredictsLocalSIWeak Quant.all.sem

theorem GeurtsPouscoulous2009.moreThanOne_predictsLocalSIWeak {α : Type u_2} [Fintype α] : PredictsLocalSIWeak Quant.moreThanOne.sem

theorem GeurtsPouscoulous2009.notAll_not_predictsLocalSI {α : Type u_2} [Fintype α] : ¬PredictsLocalSI Quant.notAll.sem

theorem GeurtsPouscoulous2009.notMoreThanOne_not_predictsLocalSI {α : Type u_2} [Fintype α] : ¬PredictsLocalSI Quant.notMoreThanOne.sem

The verification situations

@[reducible, inline]

abbrev GeurtsPouscoulous2009.Situation : Type

A situation of the third experiment records which squares are connected with which circles.

Equations

• GeurtsPouscoulous2009.Situation = (Fin 3 → Fin 3 → Prop)

@[reducible, inline]

abbrev GeurtsPouscoulous2009.allSome : Situation

The situation for all, more than one and the two downward-entailing sentences, in which every square is connected with some circle and two of them with all.

Equations

• GeurtsPouscoulous2009.allSome s c = (s ≠ 0 ∨ c = 0)

@[reducible, inline]

abbrev GeurtsPouscoulous2009.onePartial : Situation

One square connected with some but not all circles, one with all, one with none.

Equations

• GeurtsPouscoulous2009.onePartial s c = (s = 1 ∨ s = 0 ∧ c = 0)

@[reducible, inline]

abbrev GeurtsPouscoulous2009.twoPartial : Situation

Two squares connected with some but not all circles, one with all.

Equations

• GeurtsPouscoulous2009.twoPartial s c = (s = 2 ∨ c = 0)

@[reducible, inline]

abbrev GeurtsPouscoulous2009.someC (R : Situation) (s : Fin 3) : Prop

Connected with some of the circles.

Equations

• GeurtsPouscoulous2009.someC R s = ∃ (c : Fin 3), R s c

@[reducible, inline]

abbrev GeurtsPouscoulous2009.someNotAllC (R : Situation) (s : Fin 3) : Prop

The local construal, connected with some but not all of the circles.

Equations

• GeurtsPouscoulous2009.someNotAllC R s = ((∃ (c : Fin 3), R s c) ∧ ¬∀ (c : Fin 3), R s c)

inductive GeurtsPouscoulous2009.Trial : Type

The two verification trials of exactly two; the other sentences had one.

• none : Trial
• a : Trial
• b : Trial

@[instance_reducible]

instance GeurtsPouscoulous2009.instDecidableEqTrial : DecidableEq Trial

Equations

• GeurtsPouscoulous2009.instDecidableEqTrial x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GeurtsPouscoulous2009.instReprTrial : Repr Trial

Equations

• GeurtsPouscoulous2009.instReprTrial = { reprPrec := GeurtsPouscoulous2009.instReprTrial.repr }

def GeurtsPouscoulous2009.instReprTrial.repr : Trial → ℕ → Std.Format

Equations

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

def GeurtsPouscoulous2009.situation : Quant → Trial → Situation

Equations

• GeurtsPouscoulous2009.situation GeurtsPouscoulous2009.Quant.exactlyTwo GeurtsPouscoulous2009.Trial.a = GeurtsPouscoulous2009.onePartial
• GeurtsPouscoulous2009.situation GeurtsPouscoulous2009.Quant.exactlyTwo GeurtsPouscoulous2009.Trial.b = GeurtsPouscoulous2009.twoPartial
• GeurtsPouscoulous2009.situation x✝¹ x✝ = GeurtsPouscoulous2009.allSome

def GeurtsPouscoulous2009.Classical (q : Quant) (t : Trial) : Prop

The classical construal of a verification item.

Equations

• GeurtsPouscoulous2009.Classical q t = q.sem (fun (x : Fin 3) => True) (GeurtsPouscoulous2009.someC (GeurtsPouscoulous2009.situation q t))

def GeurtsPouscoulous2009.Local (q : Quant) (t : Trial) : Prop

The local-implicature construal of a verification item.

Equations

• GeurtsPouscoulous2009.Local q t = q.sem (fun (x : Fin 3) => True) (GeurtsPouscoulous2009.someNotAllC (GeurtsPouscoulous2009.situation q t))

def GeurtsPouscoulous2009.Mainstream (q : Quant) (t : Trial) : Prop

What mainstream conventionalism predicts of an item, the local construal outside downward-entailing scopes and the classical one within them.

Equations

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

theorem GeurtsPouscoulous2009.all_predictsLocalSI : PredictsLocalSI Quant.all.sem

theorem GeurtsPouscoulous2009.moreThanOne_predictsLocalSI : PredictsLocalSI Quant.moreThanOne.sem

theorem GeurtsPouscoulous2009.exactlyTwo_predictsLocalSI : PredictsLocalSI Quant.exactlyTwo.sem

theorem GeurtsPouscoulous2009.classical_all : Classical Quant.all Trial.none

theorem GeurtsPouscoulous2009.not_local_all : ¬Local Quant.all Trial.none

theorem GeurtsPouscoulous2009.classical_moreThanOne : Classical Quant.moreThanOne Trial.none

theorem GeurtsPouscoulous2009.not_local_moreThanOne : ¬Local Quant.moreThanOne Trial.none

theorem GeurtsPouscoulous2009.classical_exactlyTwo_a : Classical Quant.exactlyTwo Trial.a

theorem GeurtsPouscoulous2009.not_local_exactlyTwo_a : ¬Local Quant.exactlyTwo Trial.a

theorem GeurtsPouscoulous2009.not_classical_exactlyTwo_b : ¬Classical Quant.exactlyTwo Trial.b

theorem GeurtsPouscoulous2009.local_exactlyTwo_b : Local Quant.exactlyTwo Trial.b

theorem GeurtsPouscoulous2009.not_classical_notAll : ¬Classical Quant.notAll Trial.none

theorem GeurtsPouscoulous2009.local_notAll : Local Quant.notAll Trial.none

theorem GeurtsPouscoulous2009.not_classical_notMoreThanOne : ¬Classical Quant.notMoreThanOne Trial.none

theorem GeurtsPouscoulous2009.local_notMoreThanOne : Local Quant.notMoreThanOne Trial.none

The verification rows

structure GeurtsPouscoulous2009.Row : Type

A verification item with the majority response and the majority the stronger mainstream prediction expects.

• quant : Quant
• trial : Trial
• observed : Bool
• predicted : Bool

@[instance_reducible]

instance GeurtsPouscoulous2009.instDecidableEqRow : DecidableEq Row

Equations

• GeurtsPouscoulous2009.instDecidableEqRow = GeurtsPouscoulous2009.instDecidableEqRow.decEq

def GeurtsPouscoulous2009.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def GeurtsPouscoulous2009.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GeurtsPouscoulous2009.instReprRow : Repr Row

Equations

• GeurtsPouscoulous2009.instReprRow = { reprPrec := GeurtsPouscoulous2009.instReprRow.repr }

def GeurtsPouscoulous2009.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def GeurtsPouscoulous2009.rows : List Row

Equations

• GeurtsPouscoulous2009.rows = List.filterMap GeurtsPouscoulous2009.Row.ofDatum GeurtsPouscoulous2009.Examples.all

theorem GeurtsPouscoulous2009.rows_eq : rows = [{ quant := Quant.all, trial := Trial.none, observed := true, predicted := false }, { quant := Quant.moreThanOne, trial := Trial.none, observed := true, predicted := false }, { quant := Quant.exactlyTwo, trial := Trial.a, observed := true, predicted := false }, { quant := Quant.exactlyTwo, trial := Trial.b, observed := false, predicted := true }, { quant := Quant.notAll, trial := Trial.none, observed := false, predicted := false }, { quant := Quant.notMoreThanOne, trial := Trial.none, observed := false, predicted := false }]

theorem GeurtsPouscoulous2009.rows_construals_conflict (r : Row) : r ∈ rows → (Classical r.quant r.trial ↔ ¬Local r.quant r.trial)

Each item's situation makes its two construals conflict.

theorem GeurtsPouscoulous2009.rows_observed_classical (r : Row) : r ∈ rows → (r.observed = true ↔ Classical r.quant r.trial)

Participants' verification responses track the classical construal throughout.

theorem GeurtsPouscoulous2009.rows_predicted_mainstream (r : Row) : r ∈ rows → (r.predicted = true ↔ Mainstream r.quant r.trial)

The bracketed predictions are the stronger mainstream construal, derived from the scope monotonicity of each quantifier; outside downward-entailing scopes they invert the responses.