Evidential Support

@cite{ippolito-kiss-williams-2025} @cite{thomas-2026}

Named abstraction over probabilistic answerhood primitives, factored out for reuse across discourse particles that share the notion of "supporting an answer to a QUD" — additive particles and discourse only.

Two layers of SUPPORT

@cite{ippolito-kiss-williams-2025} Definition 13 decomposes SUPPORT into two independent conditions:

1. Doxastic: the speaker believes some alternative q of the sentence's denotation (DOX_sp ⊆ q for some q ∈ ⟦S⟧)
2. Probabilistic: q provides evidence for answer r (P(r|q) > P(r))

The doxastic condition is what blocks canonical info-seeking questions as the left argument of discourse only: the speaker doesn't believe any answer, so DOX_sp ⊄ q for all q ∈ ⟦S⟧. Biased/rhetorical questions CAN satisfy the doxastic condition because the speaker does believe an answer.

Definitions

• probSupports — probabilistic support: P(α|E) > P(α) (wraps isPositiveEvidence)
• probAntiSupports — probabilistic anti-support: P(α|E) < P(α)
• fullSupport — IKW Def. 13: doxastic + probabilistic (DOX_sp ⊆ q ∧ P(r|q) > P(r))
• supportedAnswers — which alternatives are supported
• supportStrength — magnitude of evidential boost

def Semantics.Questions.Support.probSupports {W : Type u_1} [Fintype W] (prior : ProbabilisticAnswerhood.Prior W) (evidence answer : W → Bool) : Bool

Probabilistic support: evidence E raises the probability of answer α.

This is the probabilistic component of @cite{ippolito-kiss-williams-2025} Definition 13: P(α|E) > P(α). Wraps isPositiveEvidence from ProbabilisticAnswerhood.

Equations

• Semantics.Questions.Support.probSupports prior evidence answer = Semantics.Questions.ProbabilisticAnswerhood.isPositiveEvidence evidence answer prior

def Semantics.Questions.Support.probAntiSupports {W : Type u_1} [Fintype W] (prior : ProbabilisticAnswerhood.Prior W) (evidence answer : W → Bool) : Bool

Probabilistic anti-support: evidence E lowers the probability of answer α.

P(α|E) < P(α). Wraps isNegativeEvidence.

Equations

• Semantics.Questions.Support.probAntiSupports prior evidence answer = Semantics.Questions.ProbabilisticAnswerhood.isNegativeEvidence evidence answer prior

def Semantics.Questions.Support.supportedAnswers {W : Type u_1} [Fintype W] (evidence : W → Bool) (q : Discourse.Issue W) (prior : ProbabilisticAnswerhood.Prior W) : List (Discourse.InfoState W)

Which answers in a QUD are probabilistically supported by evidence E.

Equations

• Semantics.Questions.Support.supportedAnswers evidence q prior = Semantics.Questions.ProbabilisticAnswerhood.supportedAlternatives evidence q prior

def Semantics.Questions.Support.supportStrength {W : Type u_1} [Fintype W] (evidence conclusion : W → Bool) (prior : ProbabilisticAnswerhood.Prior W) : ℚ

The magnitude of evidential support: P(α|E) − P(α).

Equations

• Semantics.Questions.Support.supportStrength evidence conclusion prior = Semantics.Questions.ProbabilisticAnswerhood.evidentialBoost evidence conclusion prior

def Semantics.Questions.Support.conjunctionStrengthensSupport {W : Type u_1} [Fintype W] (p1 p2 conclusion : W → Bool) (prior : ProbabilisticAnswerhood.Prior W) : Bool

Conjunction of two propositions strengthens support for a conclusion beyond what the first proposition provides alone.

Equations

• Semantics.Questions.Support.conjunctionStrengthensSupport p1 p2 conclusion prior = Semantics.Questions.ProbabilisticAnswerhood.conjunctionStrengthens p1 p2 conclusion prior

def Semantics.Questions.Support.fullSupport {W : Type u_1} [Fintype W] (dox : Discourse.InfoState W) (sentDen : Discourse.Issue W) (prior : ProbabilisticAnswerhood.Prior W) (answer : W → Bool) (worlds : List W) : Bool

Full SUPPORT predicate from @cite{ippolito-kiss-williams-2025} Definition 13.

SUPPORT(S, r) holds iff:

1. (Doxastic) ∃q ∈ ⟦S⟧: DOX_sp ⊆ q — the speaker believes some alternative of S's denotation
2. (Probabilistic) q provides evidence for r — P(r|q) > P(r)

Parameters:

• dox: the speaker's doxastic state DOX_sp (an info state)
• sentDen: the inquisitive denotation ⟦S⟧ (its alternatives are the q's)
• prior: probability distribution over worlds
• answer: the answer r being supported
• worlds: list of worlds for evaluating the doxastic subset check

Equations

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

theorem Semantics.Questions.Support.probSupports_iff_positive_boost {W : Type u_1} [Fintype W] (prior : ProbabilisticAnswerhood.Prior W) (evidence answer : W → Bool) : probSupports prior evidence answer = ProbabilisticAnswerhood.isPositiveEvidence evidence answer prior

probSupports is definitionally isPositiveEvidence.

theorem Semantics.Questions.Support.probSupports_implies_relevant {W : Type u_1} [Fintype W] (p : W → Bool) (q : Discourse.Issue W) (prior : ProbabilisticAnswerhood.Prior W) (h : ProbabilisticAnswerhood.probAnswers p q prior = true) : ProbabilisticAnswerhood.relevant p q prior = true

Supporting some answer implies relevance to the QUD.

theorem Semantics.Questions.Support.probSupports_when_entailing {W : Type u_1} [Fintype W] [DecidableEq W] (p : W → Bool) (q : Discourse.Issue W) (prior : ProbabilisticAnswerhood.Prior W) (alt : W → Bool) (hAltMem : alt ∈ q.alternatives) (hEntails : ∀ (w : W), p w = true → alt w = true) (hPosP : ProbabilisticAnswerhood.probOfProp prior p > 0) (hNotCertain : ProbabilisticAnswerhood.probOfState prior alt < 1) : ProbabilisticAnswerhood.probAnswers p q prior = true

Entailing an alternative guarantees support, given positive probability and non-certainty.

theorem Semantics.Questions.Support.fullSupport_declarative {W : Type u_1} [Fintype W] (dox : Discourse.InfoState W) (p : W → Bool) (prior : ProbabilisticAnswerhood.Prior W) (answer : W → Bool) (worlds : List W) (hBelief : Discourse.supports dox p worlds = true) (hEvidence : probSupports prior p answer = true) : fullSupport dox { alternatives := [p] } prior answer worlds = true

Full support for declaratives: a declarative's denotation has one alternative (its propositional content). If the speaker believes p (DOX_sp ⊆ p) and p provides evidence for r, then SUPPORT(S, r) holds.

This is a convenience lemma — fullSupport applied to a singleton Issue.

theorem Semantics.Questions.Support.fullSupport_fails_unbelieved {W : Type u_1} [Fintype W] (dox : Discourse.InfoState W) (sentDen : Discourse.Issue W) (prior : ProbabilisticAnswerhood.Prior W) (answer : W → Bool) (worlds : List W) (hNoBelief : ∀ q ∈ sentDen.alternatives, Discourse.supports dox q worlds = false) : fullSupport dox sentDen prior answer worlds = false

Full support fails when the speaker doesn't believe any alternative.

For canonical info-seeking questions, the speaker doesn't know the answer: DOX_sp ⊄ q for ALL q ∈ ⟦S⟧. This blocks SUPPORT entirely, regardless of the probabilistic component. This is IKW's explanation of the interrogative left-argument restriction (§5.2).

theorem Semantics.Questions.Support.probAntiSupports_implies_not_probSupports {W : Type u_1} [Fintype W] (prior : ProbabilisticAnswerhood.Prior W) (evidence answer : W → Bool) (h : probAntiSupports prior evidence answer = true) : probSupports prior evidence answer = false

Anti-support implies non-support: if evidence lowers P(α), it certainly doesn't raise it.

This captures the key asymmetry between but and discourse only: but requires negRelevant (anti-support / BF < 1), while discourse only only requires ¬probSupports (failure to support). Since anti-support implies non-support, but's condition is strictly stronger.