@cite{denic-homer-rothschild-chemla-2021}

The influence of polarity items on inferential judgments. Cognition 215, 104791.

The puzzle

The standard story is unidirectional: monotonicity determines where PIs are grammatical. If the arrow goes only from monotonicity to PIs, then PI presence should be inert — it shouldn't change how listeners perceive the monotonicity of the environment. This paper shows it does.

Design

Four experiments (§3–§7):

• Environments: UE, DE, NM (Exps 1–4); DN added in Exps 3–4
• PI conditions: NPI (any/ever/at all), PPI (some), no-PI

Participants rated sentence pairs (related by a narrowing substitution) for both UE-ness and DE-ness on 7-point scales. The directional rating (UE − DE) gives a single bipolar measure.

Core findings

1. NPI in NM: directional ratings shift toward DE (significant across all exps)
2. PPI in DN: directional ratings shift toward UE (significant in Exp 3)
3. UE and DE: no PI effects (ceiling/floor)
4. Scalar side-effect not the sole mechanism: the NPI effect holds across NPIs with heterogeneous scalar properties (e.g., "ever" lacks domain widening; §10.2)

Significance for linglib

The finding that PIs distinguish DN from UE challenges ContextPolarity, which maps both to .upward. The full EntailmentSig preserves the distinction (DN = addMult, simple UE = mono), suggesting PI-sensitive code should use EntailmentSig paths rather than ContextPolarity.

inductive DenicEtAl2021.MonotonicityEnv : Type

The four monotonicity environments tested.

A refinement of Core.NaturalLogic.ContextPolarity that keeps DN distinct from UE. ContextPolarity maps both to .upward; the paper shows PIs distinguish them empirically.

• UE : MonotonicityEnv
• DE : MonotonicityEnv
• NM : MonotonicityEnv
• DN : MonotonicityEnv

@[implicit_reducible]

instance DenicEtAl2021.instDecidableEqMonotonicityEnv : DecidableEq MonotonicityEnv

Equations

• DenicEtAl2021.instDecidableEqMonotonicityEnv x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DenicEtAl2021.instReprMonotonicityEnv.repr : MonotonicityEnv → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DenicEtAl2021.instReprMonotonicityEnv : Repr MonotonicityEnv

Equations

• DenicEtAl2021.instReprMonotonicityEnv = { reprPrec := DenicEtAl2021.instReprMonotonicityEnv.repr }

@[implicit_reducible]

instance DenicEtAl2021.instInhabitedMonotonicityEnv : Inhabited MonotonicityEnv

Equations

• DenicEtAl2021.instInhabitedMonotonicityEnv = { default := DenicEtAl2021.instInhabitedMonotonicityEnv.default }

def DenicEtAl2021.instInhabitedMonotonicityEnv.default : MonotonicityEnv

Equations

• DenicEtAl2021.instInhabitedMonotonicityEnv.default = DenicEtAl2021.MonotonicityEnv.UE

def DenicEtAl2021.MonotonicityEnv.isGloballyUE : MonotonicityEnv → Bool

Whether an environment is globally upward-entailing. DN and UE both return true — the crux of the coarsening problem.

Equations

• DenicEtAl2021.MonotonicityEnv.UE.isGloballyUE = true
• DenicEtAl2021.MonotonicityEnv.DN.isGloballyUE = true
• DenicEtAl2021.MonotonicityEnv.DE.isGloballyUE = false
• DenicEtAl2021.MonotonicityEnv.NM.isGloballyUE = false

inductive DenicEtAl2021.PICondition : Type

The four PI conditions in the experimental design.

• npi : PICondition
• ppi : PICondition
• noPISimple : PICondition
• noPIComplex : PICondition

@[implicit_reducible]

instance DenicEtAl2021.instDecidableEqPICondition : DecidableEq PICondition

Equations

• DenicEtAl2021.instDecidableEqPICondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DenicEtAl2021.instReprPICondition.repr : PICondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DenicEtAl2021.instReprPICondition : Repr PICondition

Equations

• DenicEtAl2021.instReprPICondition = { reprPrec := DenicEtAl2021.instReprPICondition.repr }

def DenicEtAl2021.instInhabitedPICondition.default : PICondition

Equations

• DenicEtAl2021.instInhabitedPICondition.default = DenicEtAl2021.PICondition.npi

@[implicit_reducible]

instance DenicEtAl2021.instInhabitedPICondition : Inhabited PICondition

Equations

• DenicEtAl2021.instInhabitedPICondition = { default := DenicEtAl2021.instInhabitedPICondition.default }

structure DenicEtAl2021.PIInfluence : Type

A finding about PI influence on directional ratings within an environment. The key observable: does PI presence significantly shift ratings relative to the no-PI baseline, and in which direction?

• experiment : ℕ
• environment : MonotonicityEnv
• piCondition : PICondition
• significant : Bool

  Significant difference from no-PI baseline?

• shiftDirection : Option MonotonicityEnv

  Direction of shift: .UE if toward UE, .DE if toward DE, none if n.s.

• evidence : String

def DenicEtAl2021.instReprPIInfluence.repr : PIInfluence → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DenicEtAl2021.instReprPIInfluence : Repr PIInfluence

Equations

• DenicEtAl2021.instReprPIInfluence = { reprPrec := DenicEtAl2021.instReprPIInfluence.repr }

def DenicEtAl2021.exp1_npi_NM : PIInfluence

NPI in NM: shifts directional ratings toward DE.

Equations

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

def DenicEtAl2021.exp1_ppi_DN : PIInfluence

PPI in DN: shifts directional ratings toward UE (Exp 3, §6.3).

Equations

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

def DenicEtAl2021.exp1_npi_UE : PIInfluence

NPI in UE: no effect (ceiling).

Equations

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

def DenicEtAl2021.exp1_npi_DE : PIInfluence

NPI in DE: no effect (floor).

Equations

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

def DenicEtAl2021.exp1_ppi_UE : PIInfluence

PPI in UE: no effect.

Equations

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

def DenicEtAl2021.exp1_ppi_DE : PIInfluence

PPI in DE: no effect.

Equations

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

def DenicEtAl2021.exp1_npi_DN : PIInfluence

NPI in DN: no significant effect (Exp 3, §6.3).

Equations

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

def DenicEtAl2021.exp1_ppi_NM : PIInfluence

PPI in NM: no significant effect.

Equations

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

def DenicEtAl2021.experiment1 : List PIInfluence

Equations

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

def DenicEtAl2021.exp3_npi_NM_controlled : PIInfluence

NPI effect in NM replicates in Experiment 3 (§6.3). The NPI effect holds across NPIs with heterogeneous scalar properties (any = domain widening, ever = non-domain-widening), which argues against scalar side-effects as the sole mechanism (§10.2).

Equations

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

theorem DenicEtAl2021.complementary_pattern : exp1_npi_NM.significant = true ∧ exp1_npi_DN.significant = false ∧ exp1_ppi_NM.significant = false ∧ exp1_ppi_DN.significant = true

The complementary pattern observed in Experiment 1: each PI type affects exactly the environment where its associated polarity is ambiguous.

• NPIs (associated with DE) affect NM but not DN
• PPIs (associated with UE) affect DN but not NM

inductive DenicEtAl2021.Mechanism : Type

The three proposed mechanisms for PI influence on monotonicity.

• priming : Mechanism
• scalarSideEffect : Mechanism
• statisticalTracking : Mechanism

@[implicit_reducible]

instance DenicEtAl2021.instDecidableEqMechanism : DecidableEq Mechanism

Equations

• DenicEtAl2021.instDecidableEqMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DenicEtAl2021.instReprMechanism : Repr Mechanism

Equations

• DenicEtAl2021.instReprMechanism = { reprPrec := DenicEtAl2021.instReprMechanism.repr }

def DenicEtAl2021.instReprMechanism.repr : Mechanism → ℕ → Std.Format

Equations

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

structure DenicEtAl2021.MechanismVerdict : Type

Experiment 3 rules out the scalar side-effect as the sole mechanism.

• mechanism : Mechanism
• ruledOutAsSole : Bool
• evidence : String

def DenicEtAl2021.instReprMechanismVerdict.repr : MechanismVerdict → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DenicEtAl2021.instReprMechanismVerdict : Repr MechanismVerdict

Equations

• DenicEtAl2021.instReprMechanismVerdict = { reprPrec := DenicEtAl2021.instReprMechanismVerdict.repr }

def DenicEtAl2021.exp3_verdict : MechanismVerdict

Equations

• DenicEtAl2021.exp3_verdict = { mechanism := DenicEtAl2021.Mechanism.scalarSideEffect, ruledOutAsSole := true, evidence := "NPI effect persists for non-domain-widening NPIs (Exp 3)" }

def DenicEtAl2021.npiItemsTested : List String

Equations

• DenicEtAl2021.npiItemsTested = ["any", "ever", "at all"]

def DenicEtAl2021.ppiItemTested : String

Equations

• DenicEtAl2021.ppiItemTested = "some"

def DenicEtAl2021.envSignature : MonotonicityEnv → Option Core.NaturalLogic.EntailmentSig

Map the paper's environments to canonical entailment signatures.

Equations

• DenicEtAl2021.envSignature DenicEtAl2021.MonotonicityEnv.UE = some Core.NaturalLogic.EntailmentSig.mono
• DenicEtAl2021.envSignature DenicEtAl2021.MonotonicityEnv.DE = some Core.NaturalLogic.EntailmentSig.antiAdd
• DenicEtAl2021.envSignature DenicEtAl2021.MonotonicityEnv.DN = some Core.NaturalLogic.EntailmentSig.addMult
• DenicEtAl2021.envSignature DenicEtAl2021.MonotonicityEnv.NM = none

theorem DenicEtAl2021.de_env_is_de : Core.NaturalLogic.EntailmentSig.antiAdd.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward

The DE environment maps to a DE-side signature.

theorem DenicEtAl2021.isGloballyUE_from_signature (env : MonotonicityEnv) : env.isGloballyUE = match envSignature env with | some sig => sig.toContextPolarity == Core.NaturalLogic.ContextPolarity.upward | none => false

isGloballyUE is derived from the signature map, not stipulated.

theorem DenicEtAl2021.de_composed_is_ue (φ ψ : Core.NaturalLogic.EntailmentSig) (hφ : φ.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward) (hψ : ψ.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward) : (φ * ψ).toContextPolarity = Core.NaturalLogic.ContextPolarity.upward

Any composition of two DE-side signatures is UE under ContextPolarity.

theorem DenicEtAl2021.contextPolarity_blind_to_dn (φ ψ : Core.NaturalLogic.EntailmentSig) (hφ : φ.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward) (hψ : ψ.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward) : (φ * ψ).toContextPolarity = Core.NaturalLogic.EntailmentSig.mono.toContextPolarity

ContextPolarity cannot distinguish ANY doubly-negative environment from simple UE.

theorem DenicEtAl2021.dn_signatures_vary : Core.NaturalLogic.EntailmentSig.antiAddMult.compose Core.NaturalLogic.EntailmentSig.antiAddMult ≠ Core.NaturalLogic.EntailmentSig.antiAdd.compose Core.NaturalLogic.EntailmentSig.antiMult

EntailmentSig preserves DN–UE distinctions that ContextPolarity erases.

theorem DenicEtAl2021.ue_strength_distinguishes_dn_ue : Core.NaturalLogic.EntailmentSig.addMult.toUEStrength = some Core.NaturalLogic.UEStrength.additive ∧ Core.NaturalLogic.EntailmentSig.mono.toUEStrength = some Core.NaturalLogic.UEStrength.weak

UE strength distinguishes DN from UE.

theorem DenicEtAl2021.dn_has_no_de_strength : Core.NaturalLogic.EntailmentSig.addMult.toDEStrength = none

DN has no DE strength.

theorem DenicEtAl2021.ppi_reveals_coarsening_failure : (∀ (φ ψ : Core.NaturalLogic.EntailmentSig), φ.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward → ψ.toContextPolarity = Core.NaturalLogic.ContextPolarity.downward → (φ * ψ).toContextPolarity = Core.NaturalLogic.EntailmentSig.mono.toContextPolarity) ∧ Core.NaturalLogic.EntailmentSig.addMult.toUEStrength ≠ Core.NaturalLogic.EntailmentSig.mono.toUEStrength ∧ exp1_ppi_DN.significant = true ∧ exp1_ppi_UE.significant = false

Central theorem: PPI effect reveals a distinction that ContextPolarity provably cannot make.

theorem DenicEtAl2021.npi_targets_signatureless_env : envSignature MonotonicityEnv.NM = none ∧ exp1_npi_NM.significant = true ∧ exp1_npi_DN.significant = false ∧ exp1_npi_UE.significant = false ∧ exp1_npi_DE.significant = false

NPI effects target environments with no determinate signature.

theorem DenicEtAl2021.ppi_targets_composite_ue_env : envSignature MonotonicityEnv.DN = some Core.NaturalLogic.EntailmentSig.addMult ∧ Core.NaturalLogic.EntailmentSig.addMult ≠ Core.NaturalLogic.EntailmentSig.mono ∧ Core.NaturalLogic.EntailmentSig.addMult.toUEStrength ≠ Core.NaturalLogic.EntailmentSig.mono.toUEStrength ∧ exp1_ppi_DN.significant = true ∧ exp1_ppi_UE.significant = false ∧ exp1_ppi_DE.significant = false ∧ exp1_ppi_NM.significant = false

PPI effects target environments with composite UE signatures.

theorem DenicEtAl2021.tested_npis_are_npis : Fragments.English.PolarityItems.any.isNPI ∧ Fragments.English.PolarityItems.ever.isNPI ∧ Fragments.English.PolarityItems.atAll.isNPI

The NPIs tested are classified as NPIs in the Fragment lexicon.

theorem DenicEtAl2021.tested_ppi_is_ppi : Fragments.English.PolarityItems.some_ppi.isPPI

The PPI tested is classified as a PPI in the Fragment lexicon.

theorem DenicEtAl2021.tested_npis_all_strengthening : Fragments.English.PolarityItems.any.scalarDirection = Typology.PolarityItem.ScalarDirection.strengthening ∧ Fragments.English.PolarityItems.ever.scalarDirection = Typology.PolarityItem.ScalarDirection.strengthening ∧ Fragments.English.PolarityItems.atAll.scalarDirection = Typology.PolarityItem.ScalarDirection.strengthening

The tested NPIs are all strengthening (@cite{israel-2001} Figure 1) but have heterogeneous semantic bases — the mechanism isn't purely about domain widening (§10.2).

theorem DenicEtAl2021.mechanism_constraints : exp1_npi_NM.significant = true ∧ Fragments.English.PolarityItems.atAll.baseForce ≠ Fragments.English.PolarityItems.any.baseForce ∧ exp3_npi_NM_controlled.significant = true ∧ Fragments.English.PolarityItems.ever.baseForce ≠ Fragments.English.PolarityItems.any.baseForce

Mechanism constraints: effect persists across semantically heterogeneous NPIs (different base forces) and without domain widening. The heterogeneity that matters for the non-scalar argument is in baseForce (existential vs temporal vs degree), not in scalar direction — all three are strengthening per @cite{israel-2001}.

def DenicEtAl2021.PredictsNPIEffect (env : MonotonicityEnv) : Prop

Predict NPI significance from signature: true exactly when the environment has no determinate signature.

Equations

• DenicEtAl2021.PredictsNPIEffect env = (DenicEtAl2021.envSignature env = none)

@[implicit_reducible]

instance DenicEtAl2021.instDecidablePredictsNPIEffect (env : MonotonicityEnv) : Decidable (PredictsNPIEffect env)

Equations

• DenicEtAl2021.instDecidablePredictsNPIEffect env = id inferInstance

def DenicEtAl2021.PredictsPPIEffect (env : MonotonicityEnv) : Prop

Predict PPI significance from signature: true exactly when the environment's signature has a non-weak UE strength.

Equations

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

@[implicit_reducible]

instance DenicEtAl2021.instDecidablePredictsPPIEffect (env : MonotonicityEnv) : Decidable (PredictsPPIEffect env)

Equations

• DenicEtAl2021.instDecidablePredictsPPIEffect DenicEtAl2021.MonotonicityEnv.UE = isFalse not_false
• DenicEtAl2021.instDecidablePredictsPPIEffect DenicEtAl2021.MonotonicityEnv.DE = isFalse not_false
• DenicEtAl2021.instDecidablePredictsPPIEffect DenicEtAl2021.MonotonicityEnv.NM = isFalse not_false
• DenicEtAl2021.instDecidablePredictsPPIEffect DenicEtAl2021.MonotonicityEnv.DN = isTrue trivial

theorem DenicEtAl2021.npi_prediction_matches_data : (PredictsNPIEffect MonotonicityEnv.NM ↔ exp1_npi_NM.significant = true) ∧ (PredictsNPIEffect MonotonicityEnv.DN ↔ exp1_npi_DN.significant = true) ∧ (PredictsNPIEffect MonotonicityEnv.UE ↔ exp1_npi_UE.significant = true) ∧ (PredictsNPIEffect MonotonicityEnv.DE ↔ exp1_npi_DE.significant = true)

NPI prediction matches all 4 experimental environments.

theorem DenicEtAl2021.ppi_prediction_matches_data : (PredictsPPIEffect MonotonicityEnv.NM ↔ exp1_ppi_NM.significant = true) ∧ (PredictsPPIEffect MonotonicityEnv.DN ↔ exp1_ppi_DN.significant = true) ∧ (PredictsPPIEffect MonotonicityEnv.UE ↔ exp1_ppi_UE.significant = true) ∧ (PredictsPPIEffect MonotonicityEnv.DE ↔ exp1_ppi_DE.significant = true)

PPI prediction matches all 4 experimental environments.

theorem DenicEtAl2021.experiment1_predictions_match (f : PIInfluence) : f ∈ experiment1 → (match f.piCondition with | PICondition.npi => decide (PredictsNPIEffect f.environment) | PICondition.ppi => decide (PredictsPPIEffect f.environment) | x => f.significant) = f.significant

Algebraic predictions agree with all 8 empirical data points.

theorem DenicEtAl2021.observed_pattern_matches_predictions : (PredictsNPIEffect MonotonicityEnv.NM ↔ exp1_npi_NM.significant = true) ∧ (¬PredictsNPIEffect MonotonicityEnv.DN ↔ exp1_npi_DN.significant = false) ∧ (¬PredictsPPIEffect MonotonicityEnv.NM ↔ exp1_ppi_NM.significant = false) ∧ (PredictsPPIEffect MonotonicityEnv.DN ↔ exp1_ppi_DN.significant = true)

Observed pattern (from complementary_pattern) matches signature-based predictions.

theorem DenicEtAl2021.shift_directions_match_pi_polarity : exp1_npi_NM.shiftDirection = some MonotonicityEnv.DE ∧ exp1_npi_NM.piCondition = PICondition.npi ∧ exp1_ppi_DN.shiftDirection = some MonotonicityEnv.UE ∧ exp1_ppi_DN.piCondition = PICondition.ppi

Shift directions match PI polarity.

theorem DenicEtAl2021.significant_findings_environments : exp1_npi_NM.environment = MonotonicityEnv.NM ∧ exp1_ppi_DN.environment = MonotonicityEnv.DN

Significant findings' environments match predicted environments.

theorem DenicEtAl2021.mechanism_verdict_linked : exp3_verdict.mechanism = Mechanism.scalarSideEffect ∧ exp3_verdict.ruledOutAsSole = true

Mechanism verdict linked to data file.

theorem DenicEtAl2021.npi_items_match_fragment : npiItemsTested = [Fragments.English.PolarityItems.any.form, Fragments.English.PolarityItems.ever.form, Fragments.English.PolarityItems.atAll.form]

NPI items match Fragment lexicon entries by surface form.