Meyer and Feiman (2021): Priming Reveals Similarities and Differences Between Implicatures

This file formalizes the implicature spectrum that [MF21] propose to reconcile their structural-priming results. The core implicature mechanism has two sub-computations, generating alternatives and negating them, and each may run online or have its output stored; alternatives generated online cannot have been pre-negated, so the spectrum has three points (Spectrum, spectrum_iff): both steps online, the alternatives stored and negated online, or the enriched reading stored as a second lexical entry. Two readings prime each other when they share an online sub-computation that can be primed (Primes). Three experiments find that some and number words prime each other while free-choice disjunction primes neither; the paper places some at the fully online point and number words at the stored-alternatives point, so the shared computation behind the effect is the negation of alternatives (negate_primeable), and the free-choice data then rule out the recursive-implicature derivation of free choice, which negates alternatives, while admitting the alternative-asserting mechanism of [BLF17] exactly when generation cannot be primed and modal-specific accounts such as [Sim05] unconditionally (fits_iff).

Implementation notes

A derivation is represented by the finite set of sub-computations it runs online; the paper's hypothesis for some and number words with free choice left open is spectrum, and Fits compares an account's predicted between-category priming with the observed pattern. Within-category priming, the higher enrichment rate for number words, and the experiments' picture-similarity controls are not represented.

References

• [MF21]
• [BLF17]
• [Fox07]
• [Sim05]

inductive MeyerFeiman2021.Step : Type

The sub-computations an account of an enriched reading may run: generating alternatives, negating them, and, in the free-choice mechanism of [BLF17], asserting them.

• generate : Step
• negate : Step
• assert : Step

@[instance_reducible]

instance MeyerFeiman2021.instDecidableEqStep : DecidableEq Step

Equations

• MeyerFeiman2021.instDecidableEqStep x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MeyerFeiman2021.Spectrum (o : Finset Step) : Prop

A point on the implicature spectrum: the sub-computations of the core mechanism that run online, the others having their output stored, where alternatives generated online cannot have been pre-negated.

Equations

• MeyerFeiman2021.Spectrum o = (o ⊆ {MeyerFeiman2021.Step.generate, MeyerFeiman2021.Step.negate} ∧ (MeyerFeiman2021.Step.generate ∈ o → MeyerFeiman2021.Step.negate ∈ o))

@[instance_reducible]

instance MeyerFeiman2021.instDecidablePredFinsetStepSpectrum : DecidablePred Spectrum

Equations

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

theorem MeyerFeiman2021.spectrum_iff (o : Finset Step) : Spectrum o ↔ o = {Step.generate, Step.negate} ∨ o = {Step.negate} ∨ o = ∅

The spectrum has three points: both steps online, stored alternatives negated online, and a stored enriched reading.

def MeyerFeiman2021.Primes (primeable o o' : Finset Step) : Prop

Two derivations prime each other when some sub-computation that can be primed runs online in both.

Equations

• MeyerFeiman2021.Primes primeable o o' = ∃ s ∈ primeable, s ∈ o ∧ s ∈ o'

inductive MeyerFeiman2021.Category : Type

The three categories of enriched reading tested.

• some : Category
• number : Category
• freeChoice : Category

@[instance_reducible]

instance MeyerFeiman2021.instDecidableEqCategory : DecidableEq Category

Equations

• MeyerFeiman2021.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MeyerFeiman2021.primed : Category → Category → Bool

Between-category priming observed: some and number words prime each other in both directions, and free-choice disjunction primes neither and is primed by neither.

Equations

• MeyerFeiman2021.primed MeyerFeiman2021.Category.some MeyerFeiman2021.Category.number = true
• MeyerFeiman2021.primed MeyerFeiman2021.Category.number MeyerFeiman2021.Category.some = true
• MeyerFeiman2021.primed x✝¹ x✝ = false

def MeyerFeiman2021.Fits (primeable : Finset Step) (account : Category → Finset Step) : Prop

An account assigns each category the sub-computations its enriched reading runs online; it fits the data when it predicts between-category priming exactly where observed.

Equations

• MeyerFeiman2021.Fits primeable account = ∀ (a b : MeyerFeiman2021.Category), a ≠ b → (MeyerFeiman2021.primed a b = true ↔ MeyerFeiman2021.Primes primeable (account a) (account b))

def MeyerFeiman2021.spectrum (fc : Finset Step) : Category → Finset Step

The paper's hypothesis, with the free-choice derivation fc left open: some generates and negates its alternatives online, and number words store their alternatives, the count list, and negate them online.

Equations

• MeyerFeiman2021.spectrum fc MeyerFeiman2021.Category.some = {MeyerFeiman2021.Step.generate, MeyerFeiman2021.Step.negate}
• MeyerFeiman2021.spectrum fc MeyerFeiman2021.Category.number = {MeyerFeiman2021.Step.negate}
• MeyerFeiman2021.spectrum fc MeyerFeiman2021.Category.freeChoice = fc

theorem MeyerFeiman2021.negate_primeable {primeable fc : Finset Step} (h : Primes primeable (spectrum fc Category.some) (spectrum fc Category.number)) : Step.negate ∈ primeable

The only sub-computation online for both some and number words is negation, so the priming between them shows that negating alternatives can be primed.

theorem MeyerFeiman2021.fits_iff (primeable fc : Finset Step) : Fits primeable (spectrum fc) ↔ Step.negate ∈ primeable ∧ ¬Primes primeable (spectrum fc Category.some) fc

The hypothesis fits the data exactly when negation can be primed and the free-choice derivation shares no primeable sub-computation with some.

theorem MeyerFeiman2021.recursive_not_fits (primeable : Finset Step) : ¬Fits primeable (spectrum {Step.generate, Step.negate})

The recursive-implicature derivation of free choice ([Fox07]) negates alternatives, so it shares the primeable computation with some and number words and cannot fit the data.

theorem MeyerFeiman2021.inclusion_fits_iff (primeable : Finset Step) : Fits primeable (spectrum {Step.generate, Step.assert}) ↔ Step.negate ∈ primeable ∧ Step.generate ∉ primeable

The alternative-asserting mechanism of [BLF17] shares only generation with some, so it fits the data exactly when generation cannot be primed.

theorem MeyerFeiman2021.modal_fits_iff (primeable : Finset Step) : Fits primeable (spectrum ∅) ↔ Step.negate ∈ primeable

A mechanism specific to modals and disjunction ([Sim05]) runs no implicature sub-computation, so it fits the data whenever negation can be primed.