Probabilistic Question Semantics

@cite{thomas-2026} @cite{westera-brasoveanu-2014} @cite{onea-2019}

Bayesian inquisitive answerhood. The probabilistic refinement of the set-theoretic resolution relation in Resolution.lean: a state σ "answers" a question Q under a prior μ to the extent that conditioning μ on σ shifts mass toward some resolution of Q (a conjunction of alternatives, in the inquisitive sense of @cite{ciardelli-groenendijk-roelofsen-2018}).

Key API

• evidencesMore μ A R R' — Bayesian comparator: R provides more evidence for A than R' does. @cite{thomas-2026} Def 63 (operator-level).

• IsResolutionEvidencedBy Q 𝒜 R μ — structure with four named fields capturing @cite{thomas-2026} Def 62: 𝒜 ⊆ alt Q is nonempty, R raises P(⋂𝒜), and the impact ratio of ⋂𝒜 strictly dominates that of any competing intersection.

• Answers R Q μ — R answers Q: an evidenced resolution exists. @cite{thomas-2026} Def 62.

• resolutionEvidencedBy Q R μ : Option (Set (Set W)) — the evidenced resolution as a Classical.choose-extracted witness, none when Answers fails.

• evidencesResolutionMore μ 𝒜 R R' — resolution-level analogue of evidencesMore. @cite{thomas-2026} Def 63.

Note on relocated apparatus

The doxastic Supports / Agree / Disagree predicates previously lived here; they have been moved to Phenomena/Focus/Studies/IppolitoKissWilliams2022.lean (the paper that introduced them) since their only consumer is the IKW 2025 discourse-only study file.

Bayesian evidence comparator

def Semantics.Questions.Probabilistic.evidencesMore {W : Type u_1} (μ : PMF W) (A R R' : Set W) : Prop

R evidences A more strongly than R' does: P(A | R) > P(A | R'). @cite{thomas-2026} Def 63.

Equations

• Semantics.Questions.Probabilistic.evidencesMore μ A R R' = (μ.condProbSet R A > μ.condProbSet R' A)

theorem Semantics.Questions.Probabilistic.evidencesMore_irrefl {W : Type u_1} (μ : PMF W) (A R : Set W) : ¬evidencesMore μ A R R

theorem Semantics.Questions.Probabilistic.evidencesMore_asymm {W : Type u_1} {μ : PMF W} {A R R' : Set W} (h : evidencesMore μ A R R') : ¬evidencesMore μ A R' R

theorem Semantics.Questions.Probabilistic.evidencesMore_trans {W : Type u_1} {μ : PMF W} {A R R' R'' : Set W} (h : evidencesMore μ A R R') (h' : evidencesMore μ A R' R'') : evidencesMore μ A R R''

instance Semantics.Questions.Probabilistic.instIrreflSetEvidencesMore {W : Type u_1} {μ : PMF W} {A : Set W} : Std.Irrefl (evidencesMore μ A)

@[implicit_reducible]

instance Semantics.Questions.Probabilistic.instTransSetEvidencesMore {W : Type u_1} {μ : PMF W} {A : Set W} : Trans (evidencesMore μ A) (evidencesMore μ A) (evidencesMore μ A)

Equations

• Semantics.Questions.Probabilistic.instTransSetEvidencesMore = { trans := ⋯ }

Pointwise positive evidence

The atomic Bayesian-evidence relation: conditioning on R raises the probability of A. The pointwise version of IsResolutionEvidencedBy's raises_prob field, factored out so consumers (@cite{thomas-2026} §1.2, the IKW 2022 Supports predicate in Phenomena/Focus/Studies/IppolitoKissWilliams2022.lean) can refer to it directly.

def Semantics.Questions.Probabilistic.IsPositiveEvidence {W : Type u_1} (R A : Set W) (μ : PMF W) : Prop

R provides positive evidence for A: conditioning on R raises the probability of A.

Equations

• Semantics.Questions.Probabilistic.IsPositiveEvidence R A μ = (μ.condProbSet R A > μ.probOfSet A)

theorem Semantics.Questions.Probabilistic.IsPositiveEvidence.probOfSet_pos {W : Type u_1} {μ : PMF W} {A R : Set W} (h : IsPositiveEvidence R A μ) : μ.probOfSet R > 0

Resolution evidenced by R (@cite{thomas-2026} Def 62)

structure Semantics.Questions.Probabilistic.IsResolutionEvidencedBy {W : Type u_1} (Q : Core.Question W) (𝒜 : Set (Set W)) (R : Set W) (μ : PMF W) : Prop

𝒜 ⊆ alt Q is the resolution of Q evidenced by R under prior μ. @cite{thomas-2026} Def 62.

The four fields:

• subset_alt — 𝒜 ⊆ alt Q;
• nonempty — 𝒜 is nonempty;
• raises_prob — R raises the probability of ⋂₀ 𝒜;
• dominates — for any other nonempty 𝒜' ⊆ alt Q whose intersection does not contain ⋂₀ 𝒜, the impact ratio of ⋂₀ 𝒜 strictly dominates the impact ratio of ⋂₀ 𝒜'.

The ⋂₀ 𝒜 ⊆ ⋂₀ 𝒜' exclusion in dominates is what makes weaker resolutions (= larger intersections) not interfere with a stronger candidate: a weaker competitor's intersection contains the candidate's, so the comparison is vacuously waived. The intersection ⋂₀ 𝒜 is what @cite{thomas-2026} calls "the resolution of Q evidenced by R" (notation Q|_R).

• subset_alt : 𝒜 ⊆ Q.alt
• nonempty : 𝒜.Nonempty
• raises_prob : μ.condProbSet R (⋂₀ 𝒜) > μ.probOfSet (⋂₀ 𝒜)
• dominates (𝒜' : Set (Set W)) : 𝒜' ⊆ Q.alt → 𝒜'.Nonempty → ¬⋂₀ 𝒜 ⊆ ⋂₀ 𝒜' → μ.impactRatio R (⋂₀ 𝒜) > μ.impactRatio R (⋂₀ 𝒜')

Probabilistic answerhood

def Semantics.Questions.Probabilistic.Answers {W : Type u_1} (R : Set W) (Q : Core.Question W) (μ : PMF W) : Prop

R answers Q (under prior μ): an evidenced resolution exists. @cite{thomas-2026} Def 62.

Equations

• Semantics.Questions.Probabilistic.Answers R Q μ = ∃ (𝒜 : Set (Set W)), Semantics.Questions.Probabilistic.IsResolutionEvidencedBy Q 𝒜 R μ

theorem Semantics.Questions.Probabilistic.Answers.intro {W : Type u_1} {μ : PMF W} {R : Set W} {Q : Core.Question W} {𝒜 : Set (Set W)} (h : IsResolutionEvidencedBy Q 𝒜 R μ) : Answers R Q μ

theorem Semantics.Questions.Probabilistic.Answers.probOfSet_pos {W : Type u_1} {μ : PMF W} {R : Set W} {Q : Core.Question W} (h : Answers R Q μ) : μ.probOfSet R > 0

Answers requires the prior to put positive mass on the evidence: if R answers Q then μ.probOfSet R > 0.

Resolution-as-projection

noncomputable def Semantics.Questions.Probabilistic.resolutionEvidencedBy {W : Type u_1} (Q : Core.Question W) (R : Set W) (μ : PMF W) : Option (Set (Set W))

The evidenced resolution as Option (Set (Set W)): some 𝒜 for some witness when Answers R Q μ holds, none otherwise. Witness extraction uses Classical.choose, hence noncomputable. Uniqueness of ⋂₀ 𝒜 (the "resolution of Q evidenced by R" in @cite{thomas-2026} Def 62 prose) is a consumer-side claim that follows from the dominates field under appropriate side conditions.

Equations

• Semantics.Questions.Probabilistic.resolutionEvidencedBy Q R μ = if h : Semantics.Questions.Probabilistic.Answers R Q μ then some (Classical.choose h) else none

@[simp]

theorem Semantics.Questions.Probabilistic.resolutionEvidencedBy_isSome_iff {W : Type u_1} (Q : Core.Question W) (R : Set W) (μ : PMF W) : (resolutionEvidencedBy Q R μ).isSome = true ↔ Answers R Q μ

theorem Semantics.Questions.Probabilistic.resolutionEvidencedBy_spec {W : Type u_1} {𝒜 : Set (Set W)} (Q : Core.Question W) (R : Set W) (μ : PMF W) (h : resolutionEvidencedBy Q R μ = some 𝒜) : IsResolutionEvidencedBy Q 𝒜 R μ

Resolution-level evidence comparison

def Semantics.Questions.Probabilistic.evidencesResolutionMore {W : Type u_1} (μ : PMF W) (𝒜 : Set (Set W)) (R R' : Set W) : Prop

R evidences resolution ⋂₀ 𝒜 more strongly than R' does; evidencesMore with the A argument fixed to ⋂₀ 𝒜. @cite{thomas-2026} Def 63.

Equations

• Semantics.Questions.Probabilistic.evidencesResolutionMore μ 𝒜 R R' = Semantics.Questions.Probabilistic.evidencesMore μ (⋂₀ 𝒜) R R'

@[simp]

theorem Semantics.Questions.Probabilistic.evidencesResolutionMore_iff {W : Type u_1} (μ : PMF W) (𝒜 : Set (Set W)) (R R' : Set W) : evidencesResolutionMore μ 𝒜 R R' ↔ μ.condProbSet R (⋂₀ 𝒜) > μ.condProbSet R' (⋂₀ 𝒜)

theorem Semantics.Questions.Probabilistic.evidencesResolutionMore_asymm {W : Type u_1} {μ : PMF W} {R R' : Set W} {𝒜 : Set (Set W)} (h : evidencesResolutionMore μ 𝒜 R R') : ¬evidencesResolutionMore μ 𝒜 R' R

theorem Semantics.Questions.Probabilistic.evidencesResolutionMore_trans {W : Type u_1} {μ : PMF W} {R R' R'' : Set W} {𝒜 : Set (Set W)} (h : evidencesResolutionMore μ 𝒜 R R') (h' : evidencesResolutionMore μ 𝒜 R' R'') : evidencesResolutionMore μ 𝒜 R R''

Probabilistic relevance (@cite{thomas-2026} Def 61)

The weaker companion of Answers: R is relevant to Q if some alternative of Q has its prior shifted by conditioning on some alternative of R. Used in @cite{thomas-2026} §5.4.3 to license too's prejacent against an implicit "Relevant Question" rather than a Current Question — an RQ need not be a CQ, only relevant to one.

def Semantics.Questions.Probabilistic.IsRelevantTo {W : Type u_1} (R Q : Core.Question W) (μ : PMF W) : Prop

R is relevant to Q (under prior μ): some alternative of R shifts the probability of some alternative of Q. @cite{thomas-2026} Def 61. The relation is also lifted to declarative-as-singleton-issue contexts via IsRelevantOf.

Equations

• Semantics.Questions.Probabilistic.IsRelevantTo R Q μ = ∃ A ∈ R.alt, ∃ A' ∈ Q.alt, μ.condProbSet A A' ≠ μ.probOfSet A'

def Semantics.Questions.Probabilistic.IsRelevantPropOf {W : Type u_1} (R : Set W) (Q : Core.Question W) (μ : PMF W) : Prop

A proposition R is relevant to a question Q if conditioning on R shifts the probability of some alternative of Q. The "assertion-to-question" instance of @cite{thomas-2026} Def 61.

Equations

• Semantics.Questions.Probabilistic.IsRelevantPropOf R Q μ = ∃ A' ∈ Q.alt, μ.condProbSet R A' ≠ μ.probOfSet A'

@[simp]

theorem Semantics.Questions.Probabilistic.isRelevantPropOf_iff {W : Type u_1} (R : Set W) (Q : Core.Question W) (μ : PMF W) : IsRelevantPropOf R Q μ ↔ ∃ A' ∈ Q.alt, μ.condProbSet R A' ≠ μ.probOfSet A'

The defining unfolding of IsRelevantPropOf.

Bridge claim: Answers ⇒ IsRelevantPropOf

@cite{thomas-2026} §5.1.3 informally asserts "all Answers are Relevant, but not all Relevant assertions are Answers." The forward direction is non-trivial in the substrate: a strict inequality on condProbSet R (⋂₀ 𝒜) does not mechanically imply that some A ∈ alt Q has condProbSet R A ≠ probOfSet A, because conditional probability of an intersection does not decompose into conditional probabilities of its components without independence assumptions.

The bridge holds under standard non-degeneracy hypotheses (e.g., the prior is positive on every alternative) and is proved consumer-side in the relevant study files.