QUD (Question Under Discussion) @cite{roberts-2012}

A QUD partitions the meaning space into equivalence classes. Two meanings are equivalent under a QUD if they "answer the question the same way."

The file also contains inquisitive semantics core types (InfoState, Issue) and @cite{roberts-2012}'s formalization of question entailment, subquestions, and discourse move relevance.

structure QUD (M : Type u_1) : Type u_1

A QUD partitions the meaning space via an equivalence relation. Two meanings are equivalent if they "answer the question the same way."

• sameAnswer : M → M → Bool

  Are two meanings equivalent under this QUD?

• refl (m : M) : self.sameAnswer m m = true

  Equivalence must be reflexive

• symm (m1 m2 : M) : self.sameAnswer m1 m2 = self.sameAnswer m2 m1

  Equivalence must be symmetric

• trans (m1 m2 m3 : M) : self.sameAnswer m1 m2 = true → self.sameAnswer m2 m3 = true → self.sameAnswer m1 m3 = true

  Equivalence must be transitive

• name : String

  Name for display/debugging

theorem QUD.isReflexive {M : Type u_1} (q : QUD M) (m : M) : q.sameAnswer m m = true

Reflexivity is guaranteed by construction

theorem QUD.isSymmetric {M : Type u_1} (q : QUD M) (m1 m2 : M) : q.sameAnswer m1 m2 = q.sameAnswer m2 m1

Symmetry is guaranteed by construction

theorem QUD.isTransitive {M : Type u_1} (q : QUD M) (m1 m2 m3 : M) : q.sameAnswer m1 m2 = true → q.sameAnswer m2 m3 = true → q.sameAnswer m1 m3 = true

Transitivity is guaranteed by construction

def QUD.toSetoid {M : Type u_1} (q : QUD M) : Setoid M

Convert QUD's equivalence relation to a Mathlib Setoid.

This enables Finpartition.ofSetoid for partition-based expected utility decomposition, replacing ~200 lines of custom foldl arithmetic.

Equations

• q.toSetoid = { r := fun (a b : M) => q.sameAnswer a b = true, iseqv := ⋯ }

instance QUD.decidableRel_toSetoid {M : Type u_1} (q : QUD M) : DecidableRel ⇑q.toSetoid

Equations

• q.decidableRel_toSetoid a b = inferInstanceAs (Decidable (q.sameAnswer a b = true))

def QUD.trivial {M : Type u_1} : QUD M

Trivial QUD: all meanings are equivalent (speaker doesn't care about this dimension).

Equations

• QUD.trivial = { sameAnswer := fun (x x_1 : M) => true, refl := ⋯, symm := ⋯, trans := ⋯, name := "trivial" }

def QUD.compose {M : Type u_1} (q1 q2 : QUD M) : QUD M

Compose two QUDs: equivalent iff equivalent under both.

Equations

• q1.compose q2 = { sameAnswer := fun (m1 m2 : M) => q1.sameAnswer m1 m2 && q2.sameAnswer m1 m2, refl := ⋯, symm := ⋯, trans := ⋯, name := toString q1.name ++ toString "∧" ++ toString q2.name }

instance QUD.instMul {M : Type u_1} : Mul (QUD M)

Equations

• QUD.instMul = { mul := QUD.compose }

def QUD.cell {M : Type u_1} (q : QUD M) (m : M) : Set M

The equivalence class (partition cell) of a meaning under a QUD.

Equations

• q.cell m = {m' : M | q.sameAnswer m m' = true}

theorem QUD.mem_cell_iff {M : Type u_1} (q : QUD M) (m m' : M) : m' ∈ q.cell m ↔ q.sameAnswer m m' = true

Two meanings are in the same cell iff they have the same answer.

def QUD.ofDecEq {M : Type u_1} {α : Type u_2} [DecidableEq α] (project : M → α) (name : String := "") : QUD M

Build QUD from a projection function using DecidableEq on the codomain. Avoids the need for BEq + LawfulBEq; useful when the codomain only derives DecidableEq (which is common for inductive types in Lean 4).

Example: QUD.ofDecEq MagriWorld.grade partitions by grade value.

Equations

• QUD.ofDecEq project name = { sameAnswer := fun (w v : M) => decide (project w = project v), refl := ⋯, symm := ⋯, trans := ⋯, name := name }

def QUD.ofProject {M : Type u_1} {A : Type} [BEq A] [LawfulBEq A] (f : M → A) (name : String := "") : QUD M

Build QUD from a projection function with BEq/LawfulBEq codomain.

This is the primary constructor for QUDs over types with Boolean equality. exact, binaryPartition, and PrecisionProjection.applyToQUD all delegate to this.

Equations

• QUD.ofProject f name = { sameAnswer := fun (m1 m2 : M) => f m1 == f m2, refl := ⋯, symm := ⋯, trans := ⋯, name := name }

@[simp]

theorem QUD.ofProject_sameAnswer {M : Type u_1} {A : Type} [BEq A] [LawfulBEq A] (f : M → A) (m1 m2 : M) : (ofProject f).sameAnswer m1 m2 = (f m1 == f m2)

theorem QUD.ofProject_sameAnswer_iff {M : Type u_1} {A : Type} [BEq A] [LawfulBEq A] (f : M → A) (m1 m2 : M) : (ofProject f).sameAnswer m1 m2 = true ↔ f m1 = f m2

sameAnswer for projection QUD iff same image under f.

theorem QUD.ofProject_cell_eq_fiber {M : Type u_1} {A : Type} [BEq A] [LawfulBEq A] (f : M → A) (m : M) : (ofProject f).cell m = {m' : M | f m' = f m}

For projection QUDs, cells are exactly fibers of the projection.

def QUD.exact {M : Type u_1} [BEq M] [LawfulBEq M] : QUD M

The identity QUD: speaker wants to convey exact meaning. Each meaning is its own equivalence class.

Equations

• QUD.exact = { sameAnswer := fun (m1 m2 : M) => m1 == m2, refl := ⋯, symm := ⋯, trans := ⋯, name := "exact" }

def ProductQUD.fst {A B : Type} [BEq A] [LawfulBEq A] : QUD (A × B)

QUD that cares only about first component

Equations

• ProductQUD.fst = QUD.ofProject Prod.fst "fst"

def ProductQUD.snd {A B : Type} [BEq B] [LawfulBEq B] : QUD (A × B)

QUD that cares only about second component

Equations

• ProductQUD.snd = QUD.ofProject Prod.snd "snd"

def ProductQUD.both {A B : Type} [BEq A] [BEq B] [LawfulBEq A] [LawfulBEq B] : QUD (A × B)

QUD that cares about both components (exact)

Equations

• ProductQUD.both = QUD.exact

structure PrecisionProjection (N : Type) : Type

Precision projection for numeric meanings (approximate vs exact).

• round : N → N

  Round/approximate the value

• name : String

  Name

def PrecisionProjection.exact {N : Type} : PrecisionProjection N

Exact precision: no rounding

Equations

• PrecisionProjection.exact = { round := id, name := "exact" }

def PrecisionProjection.roundTo (k : ℕ) : PrecisionProjection ℕ

Round to nearest multiple of k

Equations

• PrecisionProjection.roundTo k = { round := fun (n : ℕ) => n / k * k, name := toString "round" ++ toString k }

def PrecisionProjection.applyToQUD {M N : Type} [BEq N] [LawfulBEq N] (prec : PrecisionProjection N) (proj : M → N) : QUD M

Compose precision with a QUD. Delegates to QUD.ofProject.

Equations

• prec.applyToQUD proj = QUD.ofProject (prec.round ∘ proj) prec.name

@[reducible, inline]

abbrev Discourse.InfoState (W : Type u_1) : Type u_1

An information state: worlds compatible with current information.

In standard Inquisitive Semantics, an info state is a SET of worlds. Here we represent it as a characteristic function σ : W → Bool.

Semantically: σ w = true means "world w is compatible with the information". The empty info state (σ = λ_ => false) represents inconsistent information.

Equations

• Discourse.InfoState W = (W → Bool)

def Discourse.absurdState {W : Type u_1} : InfoState W

The absurd/inconsistent info state: no worlds are compatible.

Equations

• Discourse.absurdState x✝ = false

def Discourse.trivialState {W : Type u_1} : InfoState W

The trivial info state: all worlds are compatible (total ignorance).

Equations

• Discourse.trivialState x✝ = true

def Discourse.InfoState.isEmpty {W : Type u_1} (σ : InfoState W) (worlds : List W) : Bool

Check if an info state is empty (inconsistent).

Equations

• σ.isEmpty worlds = !worlds.any σ

def Discourse.InfoState.isNonEmpty {W : Type u_1} (σ : InfoState W) (worlds : List W) : Bool

Check if an info state is non-empty.

Equations

• σ.isNonEmpty worlds = worlds.any σ

def Discourse.InfoState.subset {W : Type u_1} (σ σ' : InfoState W) (worlds : List W) : Bool

Info state σ is a subset of σ' (σ ⊆ σ').

Equations

• σ.subset σ' worlds = worlds.all fun (w : W) => decide (σ w = true → σ' w = true)

def Discourse.InfoState.inter {W : Type u_1} (σ σ' : InfoState W) : InfoState W

Intersection of two info states.

Equations

• σ.inter σ' w = (σ w && σ' w)

def Discourse.InfoState.union {W : Type u_1} (σ σ' : InfoState W) : InfoState W

Union of two info states.

Equations

• σ.union σ' w = (σ w || σ' w)

def Discourse.supports {W : Type u_1} (σ : InfoState W) (p : W → Bool) (worlds : List W) : Bool

Info state σ supports proposition p iff σ ⊆ ⟦p⟧.

This is the fundamental relation in Inquisitive Semantics: σ ⊨ p (σ supports p) iff every world in σ makes p true.

If σ is empty, it supports every proposition (ex falso quodlibet).

Equations

• Discourse.supports σ p worlds = worlds.all fun (w : W) => decide (σ w = true → p w = true)

def Discourse.propEntails {W : Type u_1} (p q : W → Bool) (worlds : List W) : Bool

Propositional entailment: p entails q iff every p-world is a q-world.

Equivalently: the info state ⟦p⟧ supports ⟦q⟧ over all worlds.

Equations

• Discourse.propEntails p q worlds = worlds.all fun (w : W) => !p w || q w

structure Discourse.Issue (W : Type u_1) : Type u_1

An issue: set of information states that resolve the question.

In full Inquisitive Semantics, issues must be:

1. Downward-closed: if σ resolves and σ' ⊆ σ, then σ' resolves
2. Non-empty: the absurd state ∅ resolves every issue

Here we represent an issue by its maximal (largest) resolving states, called alternatives. Downward closure is then implicit.

This representation aligns with Hamblin semantics: the alternatives are the possible complete answers.

• alternatives : List (InfoState W)

  The maximal resolving states (alternatives)

def Discourse.Issue.resolves {W : Type u_1} (q : Issue W) (σ : InfoState W) (worlds : List W) : Bool

Check if an info state resolves the issue.

σ resolves Q iff σ is contained in some alternative. (Downward closure: any sub-state of an alternative also resolves.)

Equations

• q.resolves σ worlds = q.alternatives.any fun (alt : Discourse.InfoState W) => σ.subset alt worlds

def Discourse.Issue.isInquisitive {W : Type u_1} (q : Issue W) : Bool

An issue is inquisitive if it has multiple alternatives.

Non-inquisitive issues have exactly one alternative (assertions). Inquisitive issues genuinely ask for information.

Equations

• q.isInquisitive = decide (q.alternatives.length > 1)

def Discourse.Issue.isInformative {W : Type u_1} (q : Issue W) (worlds : List W) : Bool

An issue is informative if not all states resolve it.

Non-informative issues are resolved by the trivial state (tautologies). Informative issues rule out some possibilities.

Equations

• q.isInformative worlds = !q.resolves Discourse.trivialState worlds

def Discourse.Issue.empty {W : Type u_1} : Issue W

The empty issue: resolved by any info state.

Equations

• Discourse.Issue.empty = { alternatives := [Discourse.trivialState] }

def Discourse.Issue.absurd {W : Type u_1} : Issue W

The absurd issue: resolved only by the absurd state.

Equations

• Discourse.Issue.absurd = { alternatives := [Discourse.absurdState] }

def Discourse.Issue.isMentionSomeAnswer {W : Type u_1} (q : Issue W) (answer : InfoState W) (worlds : List W) : Bool

A proposition is a mention-some answer to Q: it resolves Q by settling at least one alternative without settling all of them.

In the decision-theoretic setting, mention-some answerhood is defined relative to a decision problem (see Core.Agent.DecisionTheory.isMentionSome). This definition is the purely logical version from inquisitive semantics: an answer settles Q partially.

Equations

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

def Discourse.Issue.isMentionAllAnswer {W : Type u_1} (q : Issue W) (answer : InfoState W) (worlds : List W) : Bool

A proposition is a mention-all answer to Q: it settles all alternatives (resolves Q completely by being contained in every alternative).

Equations

• q.isMentionAllAnswer answer worlds = q.alternatives.all fun (alt : Discourse.InfoState W) => answer.subset alt worlds

def Discourse.Issue.numAlternatives {W : Type u_1} (q : Issue W) : ℕ

Number of alternatives (possible complete answers).

Equations

• q.numAlternatives = q.alternatives.length

def Discourse.Issue.inter {W : Type u_1} (q q' : Issue W) (worlds : List W) : Issue W

Intersection of two issues (conjunction): Q ∩ Q'.

Equations

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

def Discourse.Issue.union {W : Type u_1} (q q' : Issue W) : Issue W

Union of two issues (disjunction): Q ∪ Q'.

Equations

• q.union q' = { alternatives := q.alternatives ++ q'.alternatives }

def Discourse.Issue.polar {W : Type u_1} (p : W → Bool) : Issue W

Create an Issue from a polar question.

"Is p true?" has two alternatives: ⟦p⟧ and ⟦¬p⟧.

Equations

• Discourse.Issue.polar p = { alternatives := [p, fun (w : W) => !p w] }

def Discourse.Issue.ofAlternatives {W : Type u_1} (alts : List (InfoState W)) : Issue W

Create an Issue from a list of alternatives (direct construction).

Equations

• Discourse.Issue.ofAlternatives alts = { alternatives := alts }

def Discourse.Issue.which {W : Type u_1} {E : Type u_2} (domain : List E) (pred : E → W → Bool) : Issue W

Create a wh-question Issue: "which x satisfies P?"

Equations

• Discourse.Issue.which domain pred = { alternatives := List.map (fun (e : E) (w : W) => pred e w) domain }

def Discourse.Issue.infoContent {W : Type u_1} (q : Issue W) : W → Bool

The informational content of an issue: the union of all alternatives.

This is what the issue "presupposes" — the proposition that SOME alternative is true.

Equations

• q.infoContent w = q.alternatives.any fun (alt : Discourse.InfoState W) => alt w

@[reducible, inline]

abbrev Discourse.Issue.highlighted {W : Type u_1} (q : Issue W) : W → Bool

The highlighted/informational content of an issue. Alias for infoContent.

In the standard inquisitive semantics framework, the informational content (union of all alternatives) IS the highlighted content for declarative sentences. We keep this alias because @cite{ippolito-kiss-williams-2025} Def. 16 uses "highlighted content" terminology in defining the at-issue content of discourse only.

Equations

• q.highlighted = q.infoContent

theorem Discourse.polar_is_inquisitive {W : Type u_1} (p : W → Bool) : (Issue.polar p).isInquisitive = true

Polar questions are always inquisitive (two alternatives).

theorem Discourse.empty_not_inquisitive {W : Type u_1} : Issue.empty.isInquisitive = false

The empty issue is not inquisitive.

def Discourse.partiallyAnswers {W : Type u_1} (p : W → Bool) (q : Issue W) (worlds : List W) : Bool

A proposition p partially answers an issue q if p entails at least one of q's alternatives.

@cite{roberts-2012}: a partial answer to Q is a proposition that, when added to the common ground, resolves at least one alternative. We use the strong version: p entails (is a subset) some alternative of q.

Equations

• Discourse.partiallyAnswers p q worlds = q.alternatives.any fun (alt : Discourse.InfoState W) => Discourse.propEntails p alt worlds

def Discourse.questionEntails {W : Type u_1} (q₁ q₂ : Issue W) (worlds : List W) : Bool

Question q₁ entails question q₂ iff every alternative of q₁ entails some alternative of q₂.

@cite{roberts-2012} Def. 8 (following @cite{groenendijk-stokhof-1984}:16): "One interrogative q₁ entails another q₂ iff every proposition that answers q₁ answers q₂ as well."

At the partition level, this corresponds to QUD.refines (Core/Partition.lean): if Q refines q, then knowing Q's answer determines q's answer.

Equations

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

def Discourse.isSubquestion {W : Type u_1} (q parent : Issue W) (worlds : List W) : Bool

q is a subquestion of Q iff Q entails q: answering Q yields a complete answer to q.

@cite{roberts-2012} Def. 8–9. At the partition level, this is QUD.refines: the parent question's partition is a refinement of the subquestion's.

Equations

• Discourse.isSubquestion q parent worlds = Discourse.questionEntails parent q worlds

def Discourse.moveRelevant {W : Type u_1} (den qud : Issue W) (subquestions : List (Issue W)) (worlds : List W) : Bool

A discourse move (assertion or question) is relevant to the QUD if it partially answers the QUD or a subquestion.

@cite{roberts-2012} Def. 15 / @cite{ippolito-kiss-williams-2025} assumption iii, p. 225: "S is relevant to QUD if S is either a subquestion of QUD or an answer to a subquestion q of QUD."

For assertions (single-alternative issues): checks whether the propositional content partially answers the QUD or a subquestion. For questions (multi-alternative issues): checks whether any alternative partially answers the QUD or a subquestion — resolving the question would inform a subquestion.

Equations

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

theorem Discourse.propEntails_refl {W : Type u_1} (p : W → Bool) (worlds : List W) : propEntails p p worlds = true

propEntails is reflexive.

theorem Discourse.questionEntails_refl {W : Type u_1} (q : Issue W) (worlds : List W) : questionEntails q q worlds = true

questionEntails is reflexive: every question entails itself.

theorem Discourse.isSubquestion_refl {W : Type u_1} (q : Issue W) (worlds : List W) : isSubquestion q q worlds = true

Subquestion is reflexive: every question is a subquestion of itself.

theorem Discourse.partiallyAnswers_implies_relevant {W : Type u_1} (den qud : Issue W) (worlds : List W) (alt : W → Bool) (hAlt : alt ∈ den.alternatives) (hPA : partiallyAnswers alt qud worlds = true) : moveRelevant den qud [] worlds = true

Partial answerhood of an alternative implies move relevance.

If some alternative of a move partially answers the QUD directly, the move is relevant (even without subquestions).