Questions/Polarity.lean #

Proof: conditionalGoalProb p prior worlds (pnot p) = 0 because filtering by ¬p means all remaining worlds have p = false, so the goal p is never satisfied. And conditionalGoalProb p prior worlds p ≥ 0 because it equals either 0 (when totalProb = 0) or totalProb/totalProb = 1 (when totalProb ≠ 0).

source

def Semantics.Questions.Polarity.surprisal {W : Type u_1} (prior : W → ℚ) (worlds : List W) (p : W → Bool) :

ℚ

Surprisal (negative log probability) of a proposition.

inf(q) = -log P(q)

Higher surprisal = lower probability = more informative if true.

We approximate with 1/prob - 1, which is monotonically decreasing in prob for all prob > 0 (like -log), equals 0 at prob = 1, and is positive for prob < 1. The prob = 0 guard handles ℚ's 1/0 = 0 convention.

Equations

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

Instances For

source

def Semantics.Questions.Polarity.informativenessAdvantage {W : Type u_1} (prior : W → ℚ) (worlds : List W) (p : W → Bool) :

ℚ

For informativity: UV(q) > UV(¬q) iff P(q) < P(¬q).

Less likely propositions are more informative when confirmed.

Equations

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

Instances For

source

def Semantics.Questions.Polarity.positiveIsLessLikely {W : Type u_1} (prior : W → ℚ) (worlds : List W) (p : W → Bool) :

Bool

Givón's generalization: by default, positive propositions are less likely.

For most natural language statements q: P(q) < P(¬q) This explains why PPQs are the default form of polar questions.

Equations

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

Instances For

source

inductive Semantics.Questions.Polarity.QuestionUse :

Type

Classification of polar question uses based on utility source.

request : QuestionUse
Goal = questioned prop (requests, pleas)
invitation : QuestionUse
Goal is facilitated by positive answer (invitations)
grounding : QuestionUse
Checking surprising new information
inference : QuestionUse
Drawing inferences from context
rhetorical : QuestionUse
Speaker indicates believed answer (rhetorical)
neutral : QuestionUse
Pure information seeking with no bias

Instances For

source

instance Semantics.Questions.Polarity.instDecidableEqQuestionUse :

DecidableEq QuestionUse

Equations

Semantics.Questions.Polarity.instDecidableEqQuestionUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Semantics.Questions.Polarity.instReprQuestionUse :

Repr QuestionUse

Equations

Semantics.Questions.Polarity.instReprQuestionUse = { reprPrec := Semantics.Questions.Polarity.instReprQuestionUse.repr }

source

def Semantics.Questions.Polarity.instReprQuestionUse.repr :

QuestionUse → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Questions.Polarity.expectedTypeForUse :

QuestionUse → PolarQuestionType

Expected question type for each use.

Equations

Instances For

source

theorem Semantics.Questions.Polarity.request_disprefers_alt (use : QuestionUse) :

use = QuestionUse.request → expectedTypeForUse use ≠ PolarQuestionType.alternative

For requests, alternative questions are pragmatically degraded.

"Will you marry me or not?" signals indifference to outcome, which is inconsistent with a genuine request.

source

def Semantics.Questions.Polarity.npqAppropriate {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (p : W → Bool) :

Bool

When is a negative polar question appropriate?

NPQ (?¬q) requires UV(¬q) > UV(q), which can happen when:

Goal is reached by ¬q being true (medical diagnosis, ecological quiz)
Prior strongly favors q, so ¬q is more informative (tag questions)

Equations

Semantics.Questions.Polarity.npqAppropriate dp actions p = (Semantics.Questions.Polarity.compareUtility dp actions p == Ordering.lt)

Instances For

source

def Semantics.Questions.Polarity.medicalDiagnosisDP {W : Type u_1} (_symptom illness : W → Bool) (prior : W → ℚ) :

Core.DecisionTheory.DecisionProblem W Bool

Example: Medical diagnosis questions.

"Is your child not eating?" is appropriate when:

Goal: diagnose illness
¬(eating properly) is a symptom that helps diagnosis
Thus P(diagnosis|¬eating) > P(diagnosis|eating)

Equations

Semantics.Questions.Polarity.medicalDiagnosisDP _symptom illness prior = { utility := fun (w : W) (a : Bool) => if (a && illness w) = true then 1 else 0, prior := prior }

Instances For

source

def Semantics.Questions.Polarity.tagQuestionInformativity {W : Type u_1} (prior : W → ℚ) (worlds : List W) (_declarative tag : W → Bool) (_hDeclarativeIsNotTag : ∀ (w : W), _declarative w = !tag w) (hDeclarativeLikely : positiveIsLessLikely prior worlds tag = true) (hPosProb : List.foldl (fun (acc : ℚ) (w : W) => acc + if tag w = true then prior w else 0) 0 worlds > 0) :

informativenessAdvantage prior worlds tag > 0

For tag questions like "John isn't bad, is he?": The speaker takes the declarative as likely true, making the tag's positive prop (that John IS bad) low probability, hence informative.

Requires positive probability for the tag proposition (so the 1/prob - 1 surprisal approximation is well-defined).

Equations

⋯ = ⋯

Instances For

source

def Semantics.Questions.Polarity.altAppropriate {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (p : W → Bool) (threshold : ℚ) :

Bool

Alternative questions are appropriate when utilities are balanced.

UV(q) ≈ UV(¬q) signals:

No preference for one answer over the other
Genuine information seeking without bias
Higher urgency (explicit enumeration of alternatives)

Equations

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

Instances For

source

theorem Semantics.Questions.Polarity.alt_impolite_for_invitation :

expectedTypeForUse QuestionUse.invitation = PolarQuestionType.positive

Alternative questions can be impolite as invitations.

"Do you want something to drink or not?" implies:

Speaker doesn't care about hearer's preference
Violates politeness by not encoding hearer's benefit

source

inductive Semantics.Questions.Polarity.AltInsistence :

Type

Degrees of insistence in alternative questions:

"Did you buy it or not?"
"Did you buy it or didn't you?"
"Did you buy it or didn't you buy it?"
"Did you or did you not buy it?"

These have increasing insistence while maintaining UV(q) ≈ UV(¬q).

minimal : AltInsistence
contracted : AltInsistence
expanded : AltInsistence
fronted : AltInsistence

Instances For

source

instance Semantics.Questions.Polarity.instDecidableEqAltInsistence :

DecidableEq AltInsistence

Equations

Semantics.Questions.Polarity.instDecidableEqAltInsistence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Semantics.Questions.Polarity.instReprAltInsistence :

Repr AltInsistence

Equations

Semantics.Questions.Polarity.instReprAltInsistence = { reprPrec := Semantics.Questions.Polarity.instReprAltInsistence.repr }

source

def Semantics.Questions.Polarity.instReprAltInsistence.repr :

AltInsistence → ℕ → Std.Format

Equations

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

Instances For

source

def Semantics.Questions.Polarity.instInhabitedAltInsistence.default :

AltInsistence

Equations

Semantics.Questions.Polarity.instInhabitedAltInsistence.default = Semantics.Questions.Polarity.AltInsistence.minimal

Instances For

source

instance Semantics.Questions.Polarity.instInhabitedAltInsistence :

Inhabited AltInsistence

Equations

Semantics.Questions.Polarity.instInhabitedAltInsistence = { default := Semantics.Questions.Polarity.instInhabitedAltInsistence.default }

On Ladd's INPQ/ONPQ Distinction #

@cite{ladd-1981} distinguished:

INPQ (inner negation): negation scopes narrowly, speaker expects negative answer
ONPQ (outer negation): negation scopes widely, speaker expects positive answer

Van Rooy & Šafářová argue this distinction is superfluous:

Both types involve UV(¬q) > UV(q)
The difference is only whether it's goal-based or informativity-based utility

The German examples:

"Gibt es kein vegetarisches Restaurant?" (INPQ reading possible)
"Gibt es nicht ein vegetarisches Restaurant?" (only ONPQ reading)

Can be explained by whether the negation can bear verum focus (INPQ = checking surprising negative info) or not (ONPQ = standard informativity-based NPQ).

source

structure Semantics.Questions.Polarity.NPQAnalysis (W : Type u_1) :

Type u_1

We don't distinguish INPQ from ONPQ semantically. The distinction is purely pragmatic (source of utility).

prop : W → Bool
The proposition being negated
utilitySource : Bool
Whether utility is goal-based or informativity-based

Instances For

source

def Semantics.Questions.Polarity.npqSemantics {W : Type u_1} (analysis : NPQAnalysis W) :

GSQuestion W

Both INPQ and ONPQ have the same semantic content.

Equations

Semantics.Questions.Polarity.npqSemantics analysis = Semantics.Questions.polarQuestion analysis.prop

Instances For

source

def Semantics.Questions.Polarity.questionPolarity (qtype : PolarQuestionType) :

Option Core.NaturalLogic.ContextPolarity

Question polarity (positive/negative) connects to entailment polarity.

In an upward-entailing context, stronger propositions are preferred. PPQ prefers the positive answer when it's more useful/informative.

This connects question pragmatics to scalar implicature contexts.

Equations

Instances For

source

structure Semantics.Questions.Polarity.RhetoricalQuestion (W : Type u_1) :

Type u_1

A rhetorical question is one where the speaker presupposes an answer but uses question form for pragmatic effect.

Key insight: Rhetorical questions MUST be polar, not alternative. "Are you crazy?" works rhetorically; "Are you crazy or not?" doesn't.

prop : W → Bool
The questioned proposition
presupposedPositive : Bool
The presupposed answer (true = positive, false = negative)
beliefStrength : ℚ
Speaker's evidence/belief strength

Instances For

source

theorem Semantics.Questions.Polarity.rhetorical_requires_polar {W : Type u_1} (_rq : RhetoricalQuestion W) :

expectedTypeForUse QuestionUse.rhetorical ≠ PolarQuestionType.alternative

Rhetorical effect requires polar form.

The speaker:

Has high prior for one answer (say ¬q)
Uses question form to highlight that recent evidence suggests q
Alternative form would remove this highlighting effect

source

def Semantics.Questions.Polarity.rhetoricalUsePPQ {W : Type u_1} (prior : W → ℚ) (worlds : List W) (p : W → Bool) (hPriorFavorsNegative : positiveIsLessLikely prior worlds p = true) (hPosProb : List.foldl (fun (acc : ℚ) (w : W) => acc + if p w = true then prior w else 0) 0 worlds > 0) :

informativenessAdvantage prior worlds p > 0

Why rhetorical questions use PPQ form even when expecting negative answer:

Speaker signals: "I have new evidence for q, even though I believed ¬q" This makes q surprising (high surprisal), thus high informativity. PPQ highlights this surprising-if-true proposition.

Requires P(p) > 0 so surprisal is well-defined.

Equations

⋯ = ⋯

Instances For

source

structure Semantics.Questions.Polarity.GroundingQuestion (W : Type u_1) :

Type u_1

A grounding question checks whether surprising new information should be accepted.

"Is David back?" after being told David returned (unexpectedly). "Is it raining?" after seeing someone with a wet jacket.

The speaker double-checks because:

P(q) was very low in prior state
New evidence suggests q might be true
Accepting q would significantly revise beliefs

prop : W → Bool
The proposition to be grounded
priorProb : ℚ
Prior probability before new evidence
posteriorProb : ℚ
Posterior probability after new evidence
hIncreased : self.posteriorProb > self.priorProb
Evidence must have increased probability