Schwab (2023): Lexical variation in NPI illusions

This file formalizes the paper's scalar account of the negative polarity illusion. Two speeded acceptability experiments on German contrast the strengthening NPI jemals 'ever' with the attenuating NPI so recht 'really' in a 2 × 3 design crossing the item with the position of a negative quantifier: in the matrix clause, where it licenses the item, inside a relative clause, where it cannot, or absent (Data/Examples/Schwab2023). Only jemals is illusorily licensed by the relative-clause quantifier, an asymmetry that the cue-based retrieval, quantifier-scope and pragmatic-rescuing accounts of the illusion do not foresee: the paper reads its Bayes factors (Data/Experiments/Schwab2023) as evidence for the jemals illusion in both experiments and for the so recht illusion in neither (illusion_attested), and for the difference between the two in the second experiment only (interaction_attested_iff). Its readings rank the Bayes factors consistently (verdictRank_monotone).

The account builds on the scalar theories of polarity sensitivity of [Kri95b], [KL93], [Chi06] and [Isr96]. A strengthening item is assertable only where the proposition is stronger than every alternative it evokes, [Kri95b]'s scalar assertion in the form of [Con10] (scalAssert); an attenuating item where some compatible alternative would have been more informative, the condition of Schwab and Liu (attenAssert). The two conditions are opposed: when the proposition entails its alternatives, scalar assertion is the plain update while the attenuating condition is contradictory (scalAssert_eq_of_isStrongest, attenAssert_eq_empty_of_isStrongest), and an existential under negation or an attenuating degree modifier under negation instantiates the licensed case of each (scalAssert_not_ever, attenAssert_not_atLeast), while in the affirmative the existential is covered by its more specific alternatives (scalAssert_ever_eq_empty) and the degree modifier entails its lower ones (isStrongest_atLeast). The illusion arises, on the paper's proposal after the environment-based account of [MP20], when the parser feeds the mechanism the still-active relative-clause proposition and its Horn-scale alternatives instead of the main clause: a negative quantifier is the strongest point of its scale, so the strengthening mechanism accepts it and the attenuating one rejects it (illusion_asymmetry).

Implementation notes

• Propositions are sets of worlds and the context is a set of worlds; an alternative is informative after the assertion when the context updated with the assertion does not entail it (Informative), the paper's c + p + p' ≠ c + p. Alternatives are an arbitrary set of propositions, so the lexical scales are hypotheses on it: the specific times of an existential and the lower degrees of a degree modifier.
• The Bayes factors and the paper's readings of them are Data/Experiments/Schwab2023; an effect counts as attested when the paper reads its Bayes factor as at least moderate evidence for it, since the paper states no threshold. The posterior estimates are not recorded. The parser's activation story that selects the relative-clause proposition is not modeled, only what each mechanism returns once it is selected.

References

• [Sch23]
• [Kri95b]
• [Con10]
• [Isr96]
• [MP20]

The two scalar licensing conditions (§1.2)

def Schwab2023.Informative {W : Type u_1} (c p p' : Set W) : Prop

An alternative p' is informative after asserting p in the context c when the context updated with p does not already entail it, the c + p + p' ≠ c + p of (5) and (6).

Equations

• Schwab2023.Informative c p p' = ¬c ∩ p ⊆ p'

theorem Schwab2023.informative_iff {W : Type u_1} (c p p' : Set W) : Informative c p p' ↔ c ∩ p ∩ p' ≠ c ∩ p

def Schwab2023.scalAssert {W : Type u_1} (c p : Set W) (alts : Set (Set W)) : Set W

(5): scalar assertion. The worlds of the context where p holds and no alternative holds that would have been informative after p; a strengthening item is licensed where this is not contradictory.

Equations

• Schwab2023.scalAssert c p alts = {w : W | w ∈ c ∧ w ∈ p ∧ ¬∃ p' ∈ alts, w ∈ p' ∧ Schwab2023.Informative c p p'}

def Schwab2023.attenAssert {W : Type u_1} (c p : Set W) (alts : Set (Set W)) : Set W

(6): the licensing condition for attenuating items. The worlds of the context where p holds and some alternative compatible with the context would have been informative after p.

Equations

• Schwab2023.attenAssert c p alts = {w : W | w ∈ c ∧ w ∈ p ∧ ∃ p' ∈ alts, (c ∩ p').Nonempty ∧ Schwab2023.Informative c p p'}

def Schwab2023.IsStrongest {W : Type u_1} (c p : Set W) (alts : Set (Set W)) : Prop

The assertion is the strongest of its alternatives in the context: it entails each of them.

Equations

• Schwab2023.IsStrongest c p alts = ∀ p' ∈ alts, c ∩ p ⊆ p'

theorem Schwab2023.scalAssert_eq_of_isStrongest {W : Type u_1} {c p : Set W} {alts : Set (Set W)} (h : IsStrongest c p alts) : scalAssert c p alts = c ∩ p

An assertion stronger than all its alternatives passes scalar assertion as the plain update: the licensed case of a strengthening item.

theorem Schwab2023.attenAssert_eq_empty_of_isStrongest {W : Type u_1} {c p : Set W} {alts : Set (Set W)} (h : IsStrongest c p alts) : attenAssert c p alts = ∅

An assertion stronger than all its alternatives fails the attenuating condition outright.

theorem Schwab2023.scalAssert_eq_empty_of_cover {W : Type u_1} {c p : Set W} {alts : Set (Set W)} (h : ∀ w ∈ c ∩ p, ∃ p' ∈ alts, w ∈ p' ∧ Informative c p p') : scalAssert c p alts = ∅

When every context world of the assertion falls under some informative alternative, scalar assertion is contradictory: the unlicensed case of a strengthening item.

theorem Schwab2023.attenAssert_eq_of_exists {W : Type u_1} {c p : Set W} {alts : Set (Set W)} (h : ∃ p' ∈ alts, (c ∩ p').Nonempty ∧ Informative c p p') : attenAssert c p alts = c ∩ p

One compatible informative alternative licenses an attenuating item: the condition is the plain update.

The lexical scales (4)

def Schwab2023.ever {W : Type u_1} {T : Type u_2} (at' : T → Set W) : Set W

ever: at some time; its alternatives are the specific times (4a).

Equations

• Schwab2023.ever at' = ⋃ (t : T), at' t

def Schwab2023.everAlts {W : Type u_1} {T : Type u_2} (at' : T → Set W) : Set (Set W)

The alternatives of ever.

Equations

• Schwab2023.everAlts at' = Set.range at'

theorem Schwab2023.isStrongest_not_ever {W : Type u_1} {T : Type u_2} (at' : T → Set W) (c : Set W) : IsStrongest c (ever at')ᶜ (compl '' everAlts at')

Under negation the existential is the strongest of its alternatives: not ever entails not at any specific time.

theorem Schwab2023.scalAssert_not_ever {W : Type u_1} {T : Type u_2} (at' : T → Set W) (c : Set W) : scalAssert c (ever at')ᶜ (compl '' everAlts at') = c ∩ (ever at')ᶜ

(2a), (4a): under negation ever is licensed, scalar assertion being the plain update.

theorem Schwab2023.scalAssert_ever_eq_empty {W : Type u_1} {T : Type u_2} (at' : T → Set W) (c : Set W) (hinf : ∀ (t : T), Informative c (ever at') (at' t)) : scalAssert c (ever at') (everAlts at') = ∅

(2a): in the affirmative ever is covered by its specific times, each informative after it, so scalar assertion is contradictory and the item unlicensed.

def Schwab2023.atLeast {W : Type u_1} {D : Type u_3} [Preorder D] (μ : W → D) (d : D) : Set W

The degree reaches d.

Equations

• Schwab2023.atLeast μ d = {w : W | d ≤ μ w}

theorem Schwab2023.atLeast_antitone {W : Type u_1} {D : Type u_3} [Preorder D] (μ : W → D) : Antitone (atLeast μ)

def Schwab2023.lowerAlts {W : Type u_1} {D : Type u_3} [Preorder D] (μ : W → D) (d : D) : Set (Set W)

The alternatives of an attenuating degree modifier at d are the lower degrees ([Isr96]).

Equations

• Schwab2023.lowerAlts μ d = {p : Set W | ∃ d' < d, p = Schwab2023.atLeast μ d'}

theorem Schwab2023.isStrongest_atLeast {W : Type u_1} {D : Type u_3} [Preorder D] (μ : W → D) (c : Set W) (d : D) : IsStrongest c (atLeast μ d) (lowerAlts μ d)

In the affirmative a degree modifier entails its lower alternatives, so the attenuating condition fails and the item is unlicensed, although the assertion is the most informative of the scale, which the paper takes to explain the higher acceptance of the unlicensed baseline with so recht.

theorem Schwab2023.attenAssert_not_atLeast {W : Type u_1} {D : Type u_3} [Preorder D] (μ : W → D) (c : Set W) {d d' : D} (hd : d' < d) (hne : (c ∩ (atLeast μ d')ᶜ).Nonempty) (hi : Informative c (atLeast μ d)ᶜ (atLeast μ d')ᶜ) : attenAssert c (atLeast μ d)ᶜ (compl '' lowerAlts μ d) = c ∩ (atLeast μ d)ᶜ

(4b): under negation a lower degree is the stronger alternative, and one that is compatible with the context and informative licenses the attenuating item.

The illusion (§4)

theorem Schwab2023.illusion_asymmetry {W : Type u_1} {c q : Set W} {alts : Set (Set W)} (hq : IsStrongest c q alts) : scalAssert c q alts = c ∩ q ∧ attenAssert c q alts = ∅

The scalar account of the illusion: fed the relative clause's proposition, a negative quantifier at the strongest point of its Horn scale, the strengthening mechanism accepts it as the plain update while the attenuating one rejects it, whatever the main clause.

The experiments

def Schwab2023.verdictRank : Verdict → ℕ

The paper's readings of a Bayes factor, ranked from the strongest evidence for the null to the strongest for the effect.

Equations

• Schwab2023.verdictRank Schwab2023.Verdict.moderateForNull = 0
• Schwab2023.verdictRank Schwab2023.Verdict.slightlyForNull = 1
• Schwab2023.verdictRank Schwab2023.Verdict.inconclusive = 2
• Schwab2023.verdictRank Schwab2023.Verdict.moderateForEffect = 3
• Schwab2023.verdictRank Schwab2023.Verdict.veryStrongForEffect = 4

theorem Schwab2023.verdictRank_monotone (e₁ : Experiment) (f₁ : Effect) (e₂ : Experiment) (f₂ : Effect) : (bayesFactors e₁ f₁).bf10.toRat < (bayesFactors e₂ f₂).bf10.toRat → verdictRank (bayesFactors e₁ f₁).verdict ≤ verdictRank (bayesFactors e₂ f₂).verdict

The paper's readings are monotone in the Bayes factor: a larger BF10 is never read as weaker evidence for its effect.

def Schwab2023.Attested (e : Experiment) (f : Effect) : Prop

An effect is attested in an experiment when the paper reads its Bayes factor as at least moderate evidence for it.

Equations

• Schwab2023.Attested e f = (Schwab2023.verdictRank Schwab2023.Verdict.moderateForEffect ≤ Schwab2023.verdictRank (Schwab2023.bayesFactors e f).verdict)

@[instance_reducible]

instance Schwab2023.instDecidableAttested (e : Experiment) (f : Effect) : Decidable (Attested e f)

Equations

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

theorem Schwab2023.illusion_attested (e : Experiment) : Attested e Effect.illusionJemals ∧ ¬Attested e Effect.illusionSoRecht

The asymmetry illusion_asymmetry derives: the strengthening jemals is illusorily licensed in both experiments, the attenuating so recht in neither.

theorem Schwab2023.interaction_attested_iff (e : Experiment) : Attested e Effect.interaction ↔ e = Experiment.exp2

The difference between the two illusions is attested in the second experiment only, whose object-extracted relative clauses and faster presentation the paper introduced after the first was inconclusive.