NPIs in Questions: Entropy as Strength

@cite{van-rooy-2003} @cite{krifka-1995a} @cite{kadmon-landman-1993} @cite{shannon-1948}

@cite{van-rooy-2003}: for assertions, strength = informativity; for questions, strength = entropy. NPIs are licensed when they increase entropy by reducing bias.

Architecture

All entropy definitions use ℝ-valued Real.negMulLog from Mathlib, which gives negMulLog(x) = -x * log(x) with negMulLog(0) = 0. Shannon entropy of a question H(Q) = ∑_cell negMulLog(P(cell)) where cell probabilities are computed via Fintype-based sums.

• @cite{van-rooy-2003}. Negative Polarity Items in Questions: Strength as Relevance.
• @cite{shannon-1948}. Mathematical Theory of Communication.
• @cite{krifka-1995a}. The semantics and pragmatics of polarity items.
• @cite{kadmon-landman-1993}. Any.

noncomputable def Semantics.Questions.EntropyNPIs.cellProb {W : Type u_1} [Fintype W] (prior : W → ℝ) (cell : W → Bool) : ℝ

Cell probability: P(cell) = ∑_{w ∈ cell} prior(w).

Equations

• Semantics.Questions.EntropyNPIs.cellProb prior cell = ∑ w : W, if cell w = true then prior w else 0

noncomputable def Semantics.Questions.EntropyNPIs.questionEntropy {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) : ℝ

Shannon entropy of a question: H(Q) = ∑_cell negMulLog(P(cell)).

Each cell contributes negMulLog(P(cell)) = -P(cell) · log(P(cell)) to the total. Degenerate cells (P = 0 or P = 1) contribute 0 by negMulLog boundary behavior.

Equations

• Semantics.Questions.EntropyNPIs.questionEntropy prior q = List.foldl (fun (acc : ℝ) (cell : W → Bool) => acc + (Semantics.Questions.EntropyNPIs.cellProb prior cell).negMulLog) 0 q

noncomputable def Semantics.Questions.EntropyNPIs.binaryEntropy (p : ℝ) : ℝ

Binary entropy function: H(p) = negMulLog(p) + negMulLog(1 - p).

Equations

• Semantics.Questions.EntropyNPIs.binaryEntropy p = p.negMulLog + (1 - p).negMulLog

def Semantics.Questions.EntropyNPIs.isMaximalEntropy {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) : Prop

A question is maximally entropic when answers are equiprobable.

Equations

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

def Semantics.Questions.EntropyNPIs.isSettled {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) : Prop

A question has zero entropy iff it is already settled (one cell has probability 1).

Equations

• Semantics.Questions.EntropyNPIs.isSettled prior q = ∃ c ∈ q, Semantics.Questions.EntropyNPIs.cellProb prior c = 1

theorem Semantics.Questions.EntropyNPIs.binaryEntropy_le_half (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : binaryEntropy p ≤ binaryEntropy (1 / 2)

Binary entropy is maximized at p = 1/2.

Proof: By strict concavity of negMulLog on [0, 1]. For any p ∈ [0, 1], negMulLog(p) + negMulLog(1-p) ≤ 2 · negMulLog(1/2) by Jensen's inequality, with equality iff p = 1/2.

theorem Semantics.Questions.EntropyNPIs.entropy_maximal_equiprobable {W : Type u_1} [Fintype W] (prior : W → ℝ) (pos neg : W → Bool) (hEqui : cellProb prior pos = cellProb prior neg) (hPartition : cellProb prior pos + cellProb prior neg = 1) (pos' neg' : W → Bool) (hPartition' : cellProb prior pos' + cellProb prior neg' = 1) (hBound' : 0 ≤ cellProb prior pos' ∧ cellProb prior pos' ≤ 1) : questionEntropy prior [pos, neg] ≥ questionEntropy prior [pos', neg']

Binary entropy is maximal at equiprobable: for any binary partition, H([½, ½]) ≥ H([p, 1−p]).

Proof: H([pos, neg]) = binaryEntropy(P(pos)) ≤ binaryEntropy(½) by concavity.

theorem Semantics.Questions.EntropyNPIs.binaryEntropy_mono_of_closer_to_half (p q : ℝ) (hp0 : 0 ≤ p) (hpq : p ≤ q) (hq1p : q ≤ 1 - p) (hp_half : p < 1 / 2) : p.negMulLog + (1 - p).negMulLog ≤ q.negMulLog + (1 - q).negMulLog

Binary entropy increases when probability moves closer to ½.

If p ≤ q ≤ 1 - p (q is between p and its "mirror" 1-p), then binaryEntropy(q) ≥ binaryEntropy(p). This is the mathematical core of van Rooy's argument: reducing bias increases entropy.

Proof: write q = (1−t)p + t(1−p) where t = (q−p)/(1−2p). By concavity of negMulLog, applied to both q and 1−q:

• negMulLog(q) ≥ (1−t)·negMulLog(p) + t·negMulLog(1−p)
• negMulLog(1−q) ≥ (1−t)·negMulLog(1−p) + t·negMulLog(p) Summing gives binaryEntropy(q) ≥ binaryEntropy(p).

def Semantics.Questions.EntropyNPIs.isBiasedNegative {W : Type u_1} [Fintype W] (prior : W → ℝ) (positive negative : W → Bool) : Prop

A polar question is biased toward negative if P(neg) > P(pos).

Equations

• Semantics.Questions.EntropyNPIs.isBiasedNegative prior positive negative = (Semantics.Questions.EntropyNPIs.cellProb prior negative > Semantics.Questions.EntropyNPIs.cellProb prior positive)

noncomputable def Semantics.Questions.EntropyNPIs.biasDegree {W : Type u_1} [Fintype W] (prior : W → ℝ) (positive negative : W → Bool) : ℝ

Degree of bias: |P(pos) - P(neg)|.

Equations

• Semantics.Questions.EntropyNPIs.biasDegree prior positive negative = |Semantics.Questions.EntropyNPIs.cellProb prior positive - Semantics.Questions.EntropyNPIs.cellProb prior negative|

structure Semantics.Questions.EntropyNPIs.NPIQuestionEffect (W : Type u_1) : Type u_1

NPI effect on a polar question: widens the positive answer's domain

• posWithoutNPI : W → Bool

  Positive answer without NPI (e.g., "someone called")

• posWithNPI : W → Bool

  Positive answer with NPI (e.g., "anyone called")

• widens (w : W) : self.posWithoutNPI w = true → self.posWithNPI w = true

  NPI widens domain: withNPI ⊇ withoutNPI

def Semantics.Questions.EntropyNPIs.NPIQuestionEffect.negWithoutNPI {W : Type u_1} (e : NPIQuestionEffect W) : W → Bool

Negative answer is complement of positive

Equations

• e.negWithoutNPI w = !e.posWithoutNPI w

def Semantics.Questions.EntropyNPIs.NPIQuestionEffect.negWithNPI {W : Type u_1} (e : NPIQuestionEffect W) : W → Bool

Equations

• e.negWithNPI w = !e.posWithNPI w

def Semantics.Questions.EntropyNPIs.NPIQuestionEffect.questionWithoutNPI {W : Type u_1} (e : NPIQuestionEffect W) : Question W

Question without NPI

Equations

• e.questionWithoutNPI = [e.posWithoutNPI, e.negWithoutNPI]

def Semantics.Questions.EntropyNPIs.NPIQuestionEffect.questionWithNPI {W : Type u_1} (e : NPIQuestionEffect W) : Question W

Question with NPI

Equations

• e.questionWithNPI = [e.posWithNPI, e.negWithNPI]

def Semantics.Questions.EntropyNPIs.npiIncreasesEntropy {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : NPIQuestionEffect W) : Prop

NPI increases entropy when question is negatively biased.

Equations

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

theorem Semantics.Questions.EntropyNPIs.npi_increases_entropy_when_negatively_biased {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : NPIQuestionEffect W) (hPriorNN : ∀ (w : W), 0 ≤ prior w) (hPartW : cellProb prior e.posWithoutNPI + cellProb prior e.negWithoutNPI = 1) (hPartN : cellProb prior e.posWithNPI + cellProb prior e.negWithNPI = 1) (hBiased : cellProb prior e.posWithoutNPI < 1 / 2) (hWider : cellProb prior e.posWithNPI ≥ cellProb prior e.posWithoutNPI) (hBoundedWidening : cellProb prior e.posWithNPI ≤ 1 - cellProb prior e.posWithoutNPI) : npiIncreasesEntropy prior e

Van Rooy's Key Result: When negatively biased, domain widening that reduces bias increases entropy.

The key hypotheses are:

• Partition: both questions' cells sum to 1 (proper probability distributions)
• Negative bias: P(pos) < ½ (negative answer is more likely)
• Widening increases positive prob: P(pos') ≥ P(pos)
• Bounded widening: P(pos') ≤ 1 - P(pos) (widening doesn't overshoot past the "mirror" of the original bias)

Under these conditions, |P(pos') - ½| ≤ |P(pos) - ½|, so by concavity of negMulLog, binaryEntropy(P(pos')) ≥ binaryEntropy(P(pos)).

The proof applies binaryEntropy_mono_of_closer_to_half: since P(pos) < ½ and P(pos) ≤ P(pos') ≤ 1 - P(pos), the widened question has higher binary entropy.

theorem Semantics.Questions.EntropyNPIs.ppi_increases_entropy_when_positively_biased {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : NPIQuestionEffect W) (hPriorNN : ∀ (w : W), 0 ≤ prior w) (hPartW : cellProb prior e.posWithoutNPI + cellProb prior e.negWithoutNPI = 1) (hPartN : cellProb prior e.posWithNPI + cellProb prior e.negWithNPI = 1) (hBiased : cellProb prior e.posWithoutNPI > 1 / 2) (hWider : cellProb prior e.posWithNPI ≥ cellProb prior e.posWithoutNPI) : questionEntropy prior e.questionWithNPI ≤ questionEntropy prior e.questionWithoutNPI

Converse: In positively biased questions, widening the positive cell moves further from balance, DECREASING entropy. NPIs are not licensed.

Proof: By symmetry of binaryEntropy, this reduces to the negatively biased case on the complementary probabilities. Since P(neg) < ½ and P(neg') ≤ P(neg), the neg probabilities move AWAY from ½, decreasing entropy.

Entropy Properties

Non-negativity and reduction to binary entropy.

Note: @cite{van-rooy-2003} shows that entropy equals expected utility for the log-scoring decision problem, grounding the entropy measure in decision theory. A formal bridge to the ℚ-valued questionUtility in Core.DecisionTheory requires ℝ-valued decision theory infrastructure.

theorem Semantics.Questions.EntropyNPIs.questionEntropy_nonneg {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) (hBound : ∀ c ∈ q, 0 ≤ cellProb prior c ∧ cellProb prior c ≤ 1) : 0 ≤ questionEntropy prior q

Question entropy is non-negative when cell probabilities are in [0, 1].

Each cell contributes negMulLog(P(c)) ≥ 0 by negMulLog_nonneg, and the foldl sum of non-negative terms is non-negative.

theorem Semantics.Questions.EntropyNPIs.questionEntropy_binary {W : Type u_1} [Fintype W] (prior : W → ℝ) (pos neg : W → Bool) (hPartition : cellProb prior pos + cellProb prior neg = 1) : questionEntropy prior [pos, neg] = binaryEntropy (cellProb prior pos)

For binary partitions, question entropy reduces to the binary entropy function.

H([pos, neg]) = binaryEntropy(P(pos)) when P(pos) + P(neg) = 1.

Rhetorical Questions and Even-NPIs

Strong NPIs (lift a finger, bat an eye) create rhetorical readings because:

1. They denote MINIMAL scalar values
2. They share a presupposition with EVEN: "For all non-minimal alternatives, the question is already settled"

Van Rooy's analysis:

• If alternatives are settled, only the minimal value is questionable
• But if minimal value is least likely to be true, only negative answer reasonable
• This creates rhetorical force

structure Semantics.Questions.EntropyNPIs.StrongNPIEffect (W : Type u_1) extends Semantics.Questions.EntropyNPIs.NPIQuestionEffect W : Type u_1

A strong NPI has EVEN-like presupposition.

• posWithoutNPI : W → Bool
• posWithNPI : W → Bool
• widens (w : W) : self.posWithoutNPI w = true → self.posWithNPI w = true
• isMinimal : True

  The NPI denotes a minimal scalar value

• alternatives : List (W → Bool)

  Set of non-minimal alternatives

• alternativesSettled (alt : W → Bool) : alt ∈ self.alternatives → ∀ (w : W), alt w = true ∨ ¬alt w = true

  Presupposition: all alternatives are settled (known false or true)

def Semantics.Questions.EntropyNPIs.isRhetorical {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) (threshold : ℝ := 1 / 10) : Prop

A question is rhetorical if it has near-zero entropy.

Equations

• Semantics.Questions.EntropyNPIs.isRhetorical prior q threshold = (Semantics.Questions.EntropyNPIs.questionEntropy prior q < threshold)

theorem Semantics.Questions.EntropyNPIs.strong_npi_creates_rhetorical {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : StrongNPIEffect W) (ε : ℝ) (hPartition : cellProb prior e.posWithNPI + cellProb prior e.negWithNPI = 1) (hPosProb : cellProb prior e.posWithNPI ≤ ε) (hPosNN : 0 ≤ cellProb prior e.posWithNPI) (hεhalf : ε ≤ 1 / 2) : questionEntropy prior e.questionWithNPI ≤ binaryEntropy ε

Theorem: Strong NPIs create rhetorical readings.

When a strong NPI is used in a question and the positive cell has probability P(pos) ≤ ε ≤ ½, the question entropy is bounded by binaryEntropy(ε). Since binaryEntropy(0) = 0 and binaryEntropy is continuous and increasing on [0, ½], small ε gives small entropy — a rhetorical reading.

The proof reduces to binaryEntropy being monotone on [0, ½]: questionEntropy [pos, neg] = binaryEntropy(P(pos)) ≤ binaryEntropy(ε).

The proof applies binaryEntropy_mono_of_closer_to_half when P(pos) < ½, and handles the degenerate case P(pos) = ½ (forcing ε = ½) separately.

K&L's Question Strengthening

@cite{kadmon-landman-1990} propose that stressed "any" strengthens questions:

Q' strengthens Q iff Q is already answered but Q' is still unanswered.

Van Rooy: This is a special case of entropy increase.

• If Q is settled (entropy 0) but Q' is not (entropy > 0)
• Then Q' has higher entropy
• Domain widening achieves this when Q is biased toward negative

def Semantics.Questions.EntropyNPIs.klStrengthens {W : Type u_1} [Fintype W] (prior : W → ℝ) (q q' : Question W) : Prop

K&L's notion: Q' strengthens Q if Q is settled but Q' is open.

Equations

• Semantics.Questions.EntropyNPIs.klStrengthens prior q q' = (Semantics.Questions.EntropyNPIs.isSettled prior q ∧ ¬Semantics.Questions.EntropyNPIs.isSettled prior q')

theorem Semantics.Questions.EntropyNPIs.settled_entropy_zero {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) (_hSettled : isSettled prior q) (_hPriorNN : ∀ (w : W), 0 ≤ prior w) (hCellBound : ∀ c ∈ q, cellProb prior c = 0 ∨ cellProb prior c = 1) : questionEntropy prior q = 0

theorem Semantics.Questions.EntropyNPIs.kl_strengthens_implies_higher_entropy {W : Type u_1} [Fintype W] (prior : W → ℝ) (q q' : Question W) (hStrengthens : klStrengthens prior q q') (hPriorNN : ∀ (w : W), 0 ≤ prior w) (hSettledCells : ∀ c ∈ q, cellProb prior c = 0 ∨ cellProb prior c = 1) (hOpenCell : ∃ c ∈ q', 0 < cellProb prior c ∧ cellProb prior c < 1) (hCellBound : ∀ c ∈ q', 0 ≤ cellProb prior c ∧ cellProb prior c ≤ 1) : questionEntropy prior q' > questionEntropy prior q

K&L strengthening implies higher entropy.

When Q is settled (all cells have P ∈ {0,1}), its entropy is 0. When Q' is not settled, it has some cell with 0 < P < 1, giving entropy > 0.

theorem Semantics.Questions.EntropyNPIs.stressed_any_achieves_kl_strengthening {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : NPIQuestionEffect W) (hSettledWithout : isSettled prior e.questionWithoutNPI) (hProperWidening : ∃ (w : W), e.posWithNPI w = true ∧ (!e.posWithoutNPI w) = true) (hPriorPos : ∀ (w : W), e.posWithNPI w = true → ¬e.posWithoutNPI w = true → 0 < prior w) (hPriorNN : ∀ (w : W), 0 ≤ prior w) (hPriorSum : ∑ w : W, prior w = 1) (hNotAllPos : ∃ (w : W), e.negWithNPI w = true ∧ 0 < prior w) : klStrengthens prior e.questionWithoutNPI e.questionWithNPI

Stressed "any" achieves K&L strengthening via domain widening.

If the question without NPI is settled, and widening adds a new world to the positive cell, then the question with NPI is not settled (the new world moves probability mass, breaking the P = 1 condition).

Strength as Relevance: The Unification

Van Rooy's key contribution: a UNIFIED notion of strength.

Speech Act	Strength Measure	NPI Effect
Assertion	Informativity (entailment)	Wider domain → stronger in DE
Question	Entropy (avg informativity)	Wider domain → less biased

Both are instances of utility maximization:

• Assertions: direct informativity maximization
• Questions: expected informativity (entropy) maximization

The connection to decision theory (Section 5.3) shows this is rational: agents should choose utterances that maximize expected utility.

inductive Semantics.Questions.EntropyNPIs.SpeechAct : Type

The unified strength measure.

• assertion : SpeechAct
• question : SpeechAct

noncomputable def Semantics.Questions.EntropyNPIs.assertionStrength {W : Type u_1} [Fintype W] (prior : W → ℝ) (p : W → Bool) : ℝ

Strength for assertions: surprisal = −log P(φ).

@cite{van-rooy-2003}: informativity of an assertion is its surprisal, -log P(φ). In DE contexts, the assertion is negated, so strength should be computed on the negated form. Surprisal is strictly decreasing for P > 0, so narrower propositions (lower probability) have higher informativity.

Equations

• Semantics.Questions.EntropyNPIs.assertionStrength prior p = -Real.log (Semantics.Questions.EntropyNPIs.cellProb prior p)

noncomputable def Semantics.Questions.EntropyNPIs.questionStrength {W : Type u_1} [Fintype W] (prior : W → ℝ) (q : Question W) : ℝ

Strength for questions: entropy.

Equations

• Semantics.Questions.EntropyNPIs.questionStrength prior q = Semantics.Questions.EntropyNPIs.questionEntropy prior q

def Semantics.Questions.EntropyNPIs.npiLicensed {W : Type u_1} [Fintype W] (prior : W → ℝ) (act : SpeechAct) (e : NPIQuestionEffect W) (polarity : Bool) : Prop

NPI licensing condition: increases strength under appropriate polarity/bias.

For assertions in DE contexts (polarity = false), strength is computed on the NEGATED form: wider domain under negation = narrower negation = more informative. For questions with negative bias (polarity = false), wider domain increases entropy.

Equations

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

theorem Semantics.Questions.EntropyNPIs.npi_assertion_licensed_de {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : NPIQuestionEffect W) (hNarrowsNeg : cellProb prior e.negWithNPI ≤ cellProb prior e.negWithoutNPI) (hNegPos : 0 < cellProb prior e.negWithNPI) : assertionStrength prior e.negWithNPI ≥ assertionStrength prior e.negWithoutNPI

NPI assertion licensing in DE contexts: wider domain under negation narrows the negated proposition, making it more informative (higher surprisal).

Proof: Since cellProb negWithNPI ≤ cellProb negWithoutNPI and -log is order-reversing on (0, ∞), the narrower negation has higher surprisal.

theorem Semantics.Questions.EntropyNPIs.unified_npi_licensing {W : Type u_1} [Fintype W] (prior : W → ℝ) (e : NPIQuestionEffect W) (act : SpeechAct) (hPriorNN : ∀ (w : W), 0 ≤ prior w) (hPartW : cellProb prior e.posWithoutNPI + cellProb prior e.negWithoutNPI = 1) (hPartN : cellProb prior e.posWithNPI + cellProb prior e.negWithNPI = 1) (hBiased : cellProb prior e.posWithoutNPI < 1 / 2) (hWider : cellProb prior e.posWithNPI ≥ cellProb prior e.posWithoutNPI) (hBoundedWidening : cellProb prior e.posWithNPI ≤ 1 - cellProb prior e.posWithoutNPI) (hNegPos : 0 < cellProb prior e.negWithNPI) : npiLicensed prior act e false

The Grand Unification: NPI licensing follows the same principle for assertions and questions—maximize strength under current polarity/bias.

For assertions: DE context → wider domain under negation is MORE informative → NPI licensed. Wider positive domain ⟹ narrower negation ⟹ lower P(neg) ⟹ higher surprisal. For questions: Negative bias → wider domain increases entropy → NPI licensed.

The hypotheses suffice for both cases:

• Assertion: hNegPos and hWider + partition give cellProb neg↓ ≤ cellProb neg, then npi_assertion_licensed_de applies.
• Question: npi_increases_entropy_when_negatively_biased applies directly.

Wh-Questions (Section 3.1)

Van Rooy notes that wh-questions ARE downward entailing in subject position:

"Who of John, Mary and Sue are sick?" entails "Who of John and Mary are sick?"

(Every complete answer to the wider question entails an answer to the narrower.)

But this DOESN'T explain NPI licensing in predicate position or polar questions. That's why we need the entropy-based account.

structure Semantics.Questions.EntropyNPIs.WhQuestion (W : Type u_1) (Entity : Type u_2) : Type (max u_1 u_2)

Wh-question with domain D and predicate P.

• domain : List Entity
• predicate : Entity → W → Bool

def Semantics.Questions.EntropyNPIs.whQuestionEntails {W : Type u_1} {Entity : Type u_2} (q q' : WhQuestion W Entity) (_hSubset : ∀ e ∈ q'.domain, e ∈ q.domain) : Prop

Wh-question entailment: Q entails Q' if every complete answer to Q determines a complete answer to Q'.

When Q' has a subset domain of Q (Q'.domain ⊆ Q.domain), knowing the predicate's extension over Q.domain determines its extension over Q'.domain. This is the sense in which wider wh-questions are stronger.

Equations

• Semantics.Questions.EntropyNPIs.whQuestionEntails q q' _hSubset = ∀ (w : W), ∀ e ∈ q'.domain, q.predicate e w = true → q'.predicate e w = true

theorem Semantics.Questions.EntropyNPIs.wh_subject_is_de {W : Type u_1} {Entity : Type u_2} (q q' : WhQuestion W Entity) (hWider : ∀ e ∈ q.domain, e ∈ q'.domain) (hSamePred : ∀ (e : Entity) (w : W), q.predicate e w = q'.predicate e w) : whQuestionEntails q' q hWider

Domain widening in wh-subject position is DE when predicates agree.

When Q and Q' share the same predicate and Q'.domain ⊇ Q.domain, knowing the predicate for all of Q'.domain determines it for Q.domain. The hSamePred hypothesis ensures the predicate is the same function.

theorem Semantics.Questions.EntropyNPIs.npi_licensed_wh_subject {W : Type u_1} {Entity : Type u_2} (q q' : WhQuestion W Entity) (hWider : ∀ e ∈ q.domain, e ∈ q'.domain) (hSamePred : ∀ (e : Entity) (w : W), q.predicate e w = q'.predicate e w) : whQuestionEntails q' q hWider

NPIs licensed in wh-subject position via standard DE reasoning.

The NPI widens the domain (Q'.domain ⊇ Q.domain). In subject position this is downward-entailing: the wider question entails the narrower one, because every complete answer to the wider question determines an answer to the narrower question. Requires predicates to agree.