Probabilistic Question Semantics

[Tho26] [westera-brasoveanu-2014] [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 [CGR18]).

Key API

• evidencesMore μ A R R' — Bayesian comparator: R provides more evidence for A than R' does. [Tho26] Def 63 (operator-level).

• IsResolutionEvidencedBy Q 𝒜 R μ — structure with four named fields capturing [Tho26] 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. [Tho26] 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. [Tho26] Def 63.

Note on relocated apparatus

The doxastic Supports / Agree / Disagree predicates previously lived here; they have been moved to 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'). [Tho26] 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 ([Tho26] §1.2, the IKW 2022 Supports predicate in 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 ([Tho26] Def 62)

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

𝒜 ⊆ alt Q is the resolution of Q evidenced by R under prior μ. [Tho26] 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 [Tho26] 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 (⋂₀ 𝒜')

theorem Semantics.Questions.Probabilistic.IsResolutionEvidencedBy.sInter_subset_or_subset {W : Type u_1} {μ : PMF W} {R : Set W} {Q : Question W} {𝒜 𝒜' : Set (Set W)} (h₁ : IsResolutionEvidencedBy Q 𝒜 R μ) (h₂ : IsResolutionEvidencedBy Q 𝒜' R μ) : ⋂₀ 𝒜 ⊆ ⋂₀ 𝒜' ∨ ⋂₀ 𝒜' ⊆ ⋂₀ 𝒜

Evidenced resolutions are nested: two resolutions of Q for the same evidence R have ⊆-comparable intersections. This is the robust content of [Tho26] Def 62's "if such a set 𝒜 exists, it is unique" — the dominates field forces a chain, so the strongest (⊆-minimal) resolution is the canonical Q|_R. Full set-uniqueness does not hold: dominates deliberately waives competitors whose intersection contains ⋂₀ 𝒜, so weaker resolutions can coexist higher in the chain.

Probabilistic answerhood

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

R answers Q (under prior μ): an evidenced resolution exists. [Tho26] 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 : 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 : 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.

Witnessing the structure (finite worlds)

A constructor and a negative test showing the answerhood structure is both satisfiable and genuinely discriminating. Both require [Fintype W], via the finite-PMF mass bounds of Core/Probability/Finite.lean.

theorem Semantics.Questions.Probabilistic.isResolutionEvidencedBy_singleton {W : Type u_1} {μ : PMF W} {A R : Set W} {Q : Question W} [Fintype W] (hA : A ∈ Q.alt) (hsel : ∀ A' ∈ Q.alt, A' ≠ A → R ∩ A' = ∅) (hRA : R ⊆ A) (hRpos : μ.probOfSet R > 0) (hAlt1 : μ.probOfSet A < 1) : IsResolutionEvidencedBy Q {A} R μ

Constructor for a singleton evidenced resolution. If A is an alternative of Q, the evidence R lies inside A and misses every other alternative (R ∩ A' = ∅ for A' ∈ alt Q, A' ≠ A), the prior puts positive mass on R, and A is not full-measure, then {A} is a resolution of Q evidenced by R. The dominates field holds because any competitor not containing A must contain some other alternative A', whose intersection R misses — giving it impact ratio 0 < μ.impactRatio R A.

theorem Semantics.Questions.Probabilistic.not_answers_univ {W : Type u_1} {μ : PMF W} {Q : Question W} [Fintype W] : ¬Answers Set.univ Q μ

Trivial (universal) evidence answers no question: conditioning on univ changes nothing, so no resolution is strictly raised.

Resolution-as-projection

noncomputable def Semantics.Questions.Probabilistic.resolutionEvidencedBy {W : Type u_1} (Q : 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. Evidenced resolutions are nested (IsResolutionEvidencedBy.sInter_subset_or_subset), so the strongest is the canonical Q|_R of [Tho26] Def 62; Classical.choose need not return it, since full set-uniqueness fails (weaker resolutions coexist).

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 : 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 : 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 ⋂₀ 𝒜. [Tho26] 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 ([Tho26] 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 [Tho26] §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 : Question W) (μ : PMF W) : Prop

R is relevant to Q (under prior μ): some alternative of R shifts the probability of some alternative of Q. [Tho26] 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 : 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 [Tho26] 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 : Question W) (μ : PMF W) : IsRelevantPropOf R Q μ ↔ ∃ A' ∈ Q.alt, μ.condProbSet R A' ≠ μ.probOfSet A'

The defining unfolding of IsRelevantPropOf.

Bridge: Answers ⇒ IsRelevantPropOf

[Tho26] §5.1.3 asserts "all Answers are Relevant, but not all Relevant assertions are Answers." The forward direction does not hold mechanically: a strict inequality on condProbSet R (⋂₀ 𝒜) need not imply that some single A ∈ alt Q has condProbSet R A ≠ probOfSet A, because the conditional probability of an intersection does not decompose into those of its components without an independence assumption. Positivity of the prior on each alternative is not sufficient — R can correlate with the conjunction while leaving every marginal fixed. It does hold unconditionally for singleton (mention-some/one) resolutions, and in general once the prior propagates marginal irrelevance to the resolution.

theorem Semantics.Questions.Probabilistic.IsResolutionEvidencedBy.isRelevantPropOf_singleton {W : Type u_1} {μ : PMF W} {A R : Set W} {Q : Question W} (h : IsResolutionEvidencedBy Q {A} R μ) : IsRelevantPropOf R Q μ

For a singleton resolution {A}, answerhood evidence is directly relevance to Q: R raises P(A) and A ∈ alt Q. The mention-some/one instance of [Tho26] §5.1.3.

theorem Semantics.Questions.Probabilistic.IsResolutionEvidencedBy.isRelevantPropOf {W : Type u_1} {μ : PMF W} {R : Set W} {Q : Question W} {𝒜 : Set (Set W)} (hRes : IsResolutionEvidencedBy Q 𝒜 R μ) (hindep : (∀ A' ∈ Q.alt, μ.condProbSet R A' = μ.probOfSet A') → μ.condProbSet R (⋂₀ 𝒜) = μ.probOfSet (⋂₀ 𝒜)) : IsRelevantPropOf R Q μ

General forward bridge under an explicit independence hypothesis: if the prior carries marginal irrelevance (R shifts no alternative of Q) to the resolution ⋂₀ 𝒜, then any evidenced resolution makes R relevant to Q. The hypothesis is exactly the non-degeneracy [Tho26] §5.1.3 leaves implicit.