Questions/Partition.lean

@cite{groenendijk-stokhof-1984}

@cite{groenendijk-stokhof-1984} Partition Semantics for Questions.

Core Ideas

A question denotes an equivalence relation on worlds:

⟦?x.P(x)⟧ = λw.λv. [λx.P(w)(x) = λx.P(v)(x)]

Two worlds are equivalent iff the predicate has the same extension in both. This induces a partition of logical space.

Architecture

GSQuestion is an abbreviation for QUD. All partition lattice operations (refinement, coarsening, cells) are defined in Core/Partition.lean and apply to any equivalence-relation partition, not just question denotations.

This module provides question-specific constructors and interpretation.

@[reducible, inline]

abbrev Semantics.Questions.GSQuestion (W : Type u_1) : Type u_1

A G&S-style question is exactly a QUD: an equivalence relation on worlds.

Two worlds are equivalent iff they give the same answer to the question. This induces a partition of the world space.

Equations

• Semantics.Questions.GSQuestion W = QUD W

@[reducible, inline]

abbrev Semantics.Questions.GSQuestion.equiv {W : Type u_1} (q : GSQuestion W) : W → W → Bool

Compatibility accessor: equiv is the same as sameAnswer.

Equations

• q.equiv = q.sameAnswer

def Semantics.Questions.GSQuestion.«term_⊑_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Questions.GSQuestion.exact {W : Type u_1} [BEq W] [LawfulBEq W] : GSQuestion W

The finest possible partition (identity). Each world is its own equivalence class. This is the "maximally informative" question.

Equations

• Semantics.Questions.GSQuestion.exact = QUD.exact

def Semantics.Questions.GSQuestion.trivial {W : Type u_1} : GSQuestion W

The coarsest partition (all worlds equivalent). Conveys no information. This is the "tautological" question (always answered "yes").

Equations

• Semantics.Questions.GSQuestion.trivial = QUD.trivial

def Semantics.Questions.GSQuestion.ofProject {W : Type u_1} {A : Type} [BEq A] [LawfulBEq A] (f : W → A) : GSQuestion W

Build a question from a projection function. Two worlds are equivalent iff they have the same value under projection.

Example: ofProject (λ w => w.weather) asks "What's the weather?"

Equations

• Semantics.Questions.GSQuestion.ofProject f = QUD.ofProject f

def Semantics.Questions.GSQuestion.ofPredicate {W : Type u_1} (p : W → Bool) : GSQuestion W

Build a question from a Boolean predicate (polar question). Partitions into {yes-worlds} and {no-worlds}.

Equations

• Semantics.Questions.GSQuestion.ofPredicate p = QUD.ofProject p

def Semantics.Questions.GSQuestion.toQuestion {W : Type u_1} (q : GSQuestion W) (worlds : List W) : Question W

Convert to the general Question type (list of characteristic functions).

Equations

• q.toQuestion worlds = QUD.toCells q worlds

def Semantics.Questions.GSQuestion.toQUD {W : Type u_1} (q : GSQuestion W) : QUD W

Convert to a Core.QUD (identity since GSQuestion = QUD).

Equations

• q.toQUD = q

def Semantics.Questions.GSQuestion.ofQUD {W : Type u_1} (qud : QUD W) : GSQuestion W

Convert from a QUD (identity since GSQuestion = QUD).

Equations

• Semantics.Questions.GSQuestion.ofQUD qud = qud

theorem Semantics.Questions.GSQuestion.toQUD_ofQUD_roundtrip {W : Type u_1} (q : GSQuestion W) : ofQUD q.toQUD = q

theorem Semantics.Questions.GSQuestion.ofQUD_toQUD_roundtrip {W : Type u_1} (qud : QUD W) : (ofQUD qud).toQUD = qud

def Semantics.Questions.polarQuestion {W : Type u_1} (p : W → Bool) : GSQuestion W

A yes/no (polar) question: partitions into {yes-worlds} and {no-worlds}.

Example: "Is it raining?" partitions worlds into rainy and not-rainy.

Equations

• Semantics.Questions.polarQuestion p = Semantics.Questions.GSQuestion.ofPredicate p

theorem Semantics.Questions.polarQuestion_eq_ofProject {W : Type u_1} (p : W → Bool) : polarQuestion p = GSQuestion.ofProject p

A polar question is equivalent to projecting onto Bool.

def Semantics.Questions.whQuestion {W A : Type} [BEq A] [LawfulBEq A] (f : W → A) : GSQuestion W

A wh-question asks for the value of some function.

Example: "Who came?" = ofProject (λ w => w.guests) Two worlds are equivalent iff they have the same set of guests.

Equations

• Semantics.Questions.whQuestion f = Semantics.Questions.GSQuestion.ofProject f

def Semantics.Questions.alternativeQuestion {W : Type u_1} (alts : List (W → Bool)) : GSQuestion W

An alternative question: which of these propositions is true?

Example: "Did John or Mary come?"

Equations

• Semantics.Questions.alternativeQuestion alts = QUD.ofProject fun (w : W) => List.map (fun (p : W → Bool) => p w) alts

def Semantics.Questions.isExhaustive {W : Type u_1} (_q : GSQuestion W) : Bool

A question demands exhaustive answers if its semantics requires knowing exactly which cell the actual world is.

This is the default for G&S semantics — all questions are exhaustive.

Equations

• Semantics.Questions.isExhaustive _q = true

theorem Semantics.Questions.polar_exhaustive {W : Type u_1} (p : W → Bool) (w : W) : QUD.numCells (polarQuestion p) [w] ≤ 2

The exhaustive interpretation of a polar question is complete: answering requires saying "yes" or "no", not "I don't know".

@[reducible, inline]

abbrev Semantics.Questions.InfoSet (W : Type u_1) : Type u_1

An information set J ⊆ I represents what the questioner knows. J is the set of indices compatible with the questioner's factual knowledge.

@cite{groenendijk-stokhof-1984}, p. 350: "One may argue that using an information set to represent the questioner's informational state involves idealizations. [...] We think these idealizations are harmless."

Equations

• Semantics.Questions.InfoSet W = (W → Bool)

def Semantics.Questions.totalIgnorance {W : Type u_1} : InfoSet W

The total information set (no factual knowledge).

Equations

• Semantics.Questions.totalIgnorance x✝ = true

def Semantics.Questions.InfoSet.contains {W : Type u_1} (j : InfoSet W) (w : W) : Bool

Check if a world is in the information set.

Equations

• j.contains w = j w

def Semantics.Questions.InfoSet.intersect {W : Type u_1} (j : InfoSet W) (p : W → Bool) : W → Bool

Intersection of a proposition with an information set.

Equations

• j.intersect p w = (j w && p w)

def Semantics.Questions.GSQuestion.restrictedCells {W : Type u_1} (q : GSQuestion W) (j : InfoSet W) (worlds : List W) : List (W → Bool)

The restricted cells as a list of characteristic functions.

These are the cells of the partition J/Q: each cell P' is some P ∩ J where P is a cell of I/Q and P ∩ J ≠ ∅.

Moved from PragmaticAnswerhood: this is a general partition operation useful beyond pragmatic answerhood (e.g., for computing pragmatic exhaustivity, or for the GSQuestion↔Issue bridge).

Equations

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

theorem Semantics.Questions.foldl_reps_mem {W : Type u_1} (equiv : W → W → Bool) (l init : List W) (r : W) : r ∈ List.foldl (fun (acc : List W) (w : W) => if (acc.any fun (r : W) => equiv r w) = true then acc else w :: acc) init l → r ∈ init ∨ r ∈ l

Elements of the foldl-built representative list come from the input list.

theorem Semantics.Questions.restrictedCells_cover {W : Type u_1} (q : GSQuestion W) (j : InfoSet W) (worlds : List W) (w : W) (hw : w ∈ List.filter j worlds) : ∃ cell ∈ q.restrictedCells j worlds, cell w = true

Every J-world is Q-equivalent to some representative in restrictedCells.

This is the covering property: the foldl in restrictedCells produces reps such that every input element is equivalent to some rep.

theorem Semantics.Questions.restrictedCells_inhabited {W : Type u_1} (q : GSQuestion W) (j : InfoSet W) (worlds : List W) (cell : W → Bool) : cell ∈ q.restrictedCells j worlds → ∃ w ∈ worlds, cell w = true

Every cell produced by restrictedCells has a witness in worlds.