QUD: Equivalence-Relation Partitioning of a Meaning Space

@cite{roberts-2012}

A QUD M partitions a meaning space M via an equivalence relation: two meanings are equivalent iff they "answer the question the same way."

Design

A QUD M is a Setoid M together with decidability of its equivalence relation. Setoid is the single source of truth for the equivalence structure (no separately-stored Bool field that can drift); decidability is bundled so consumer code doesn't need to thread [DecidableRel q.r] through every signature.

This file is the algebraic core: the bundle, constructors (trivial, compose, ofProject, ofDecEq, exact), equivalence-class cells, the Bool-view (sameAnswer), and the ProductQUD projections.

Place in the Question API

QUD M lives inside Core/Question/ (rather than a parallel Core/QUD/ directory) as the construction-side API for partition-shaped questions. The inquisitive Question W (Core/Question/Basic.lean) is the consumer-side type with the richer lattice and answerhood structure; Question.fromSetoid (Core/Mood/PartitionAsInquiry.lean) is the canonical bridge from a Setoid (or QUD) into an inquisitive Question. Long-term mathlib alignment is abbrev QUD M := Setoid M once the Bool-API consumer sites have migrated to [DecidableRel s.r] plus Prop-valued outputs; the bundled {toSetoid, decR} shape is a transitional form that preserves Bool ergonomics while keeping Setoid as the single source of truth.

structure QUD (M : Type u_1) : Type u_1

A QUD partitions a meaning space M via an equivalence relation. Bundles a Setoid M with decidability of its equivalence relation — Setoid is the source of truth, decidability is along for the ride.

• toSetoid : Setoid M

  The underlying setoid (equivalence relation + reflexivity/symmetry/transitivity).

• decR : DecidableRel ⇑self.toSetoid

  Decidability of the equivalence relation.

@[reducible]

def QUD.r {M : Type u_1} (q : QUD M) : M → M → Prop

Forward r from the underlying setoid.

Equations

• q.r = ⇑q.toSetoid

@[implicit_reducible]

instance QUD.instDecidableRel {M : Type u_1} (q : QUD M) : DecidableRel q.r

Equations

• q.instDecidableRel = q.decR

theorem QUD.iseqv {M : Type u_1} (q : QUD M) : Equivalence q.r

Forward iseqv from the underlying setoid.

def QUD.sameAnswer {M : Type u_1} (q : QUD M) (a b : M) : Bool

Decidable equivalence as a Bool.

Equations

• q.sameAnswer a b = decide (q.r a b)

@[simp]

theorem QUD.sameAnswer_eq_true_iff {M : Type u_1} (q : QUD M) (a b : M) : q.sameAnswer a b = true ↔ q.r a b

theorem QUD.sameAnswer_of_r {M : Type u_1} {q : QUD M} {a b : M} (h : q.r a b) : q.sameAnswer a b = true

theorem QUD.r_of_sameAnswer {M : Type u_1} {q : QUD M} {a b : M} (h : q.sameAnswer a b = true) : q.r a b

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

theorem QUD.symm {M : Type u_1} (q : QUD M) (a b : M) : q.sameAnswer a b = q.sameAnswer b a

theorem QUD.trans {M : Type u_1} (q : QUD M) (a b c : M) (h1 : q.sameAnswer a b = true) (h2 : q.sameAnswer b c = true) : q.sameAnswer a c = true

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.

@[simp]

theorem QUD.toSetoid_r {M : Type u_1} (q : QUD M) (a b : M) : q.toSetoid a b ↔ q.r a b

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

Trivial QUD: all meanings are equivalent. Mathlib ⊤ : Setoid M.

Equations

• QUD.trivial = { toSetoid := ⊤, decR := fun (x x_1 : M) => isTrue True.intro }

@[simp]

theorem QUD.trivial_r {M : Type u_1} (m1 m2 : M) : trivial.r m1 m2

@[simp]

theorem QUD.trivial_sameAnswer {M : Type u_1} (m1 m2 : M) : trivial.sameAnswer m1 m2 = true

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

Compose two QUDs: equivalent iff equivalent under both. Mathlib q1 ⊓ q2.

Equations

• q1.compose q2 = { toSetoid := q1.toSetoid ⊓ q2.toSetoid, decR := fun (a b : M) => decidable_of_iff (q1.toSetoid a b ∧ q2.toSetoid a b) ⋯ }

@[simp]

theorem QUD.compose_r {M : Type u_1} (q1 q2 : QUD M) (a b : M) : (q1.compose q2).r a b ↔ q1.r a b ∧ q2.r a b

@[simp]

theorem QUD.compose_sameAnswer {M : Type u_1} (q1 q2 : QUD M) (m1 m2 : M) : (q1.compose q2).sameAnswer m1 m2 = (q1.sameAnswer m1 m2 && q2.sameAnswer m1 m2)

theorem QUD.compose_sameAnswer_iff {M : Type u_1} (q1 q2 : QUD M) (m1 m2 : M) : (q1.compose q2).sameAnswer m1 m2 = true ↔ q1.sameAnswer m1 m2 = true ∧ q2.sameAnswer m1 m2 = true

@[implicit_reducible]

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

Equations

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

@[simp]

theorem QUD.mul_eq_compose {M : Type u_1} (q1 q2 : QUD M) : q1 * q2 = q1.compose q2

@[simp]

theorem QUD.mul_r {M : Type u_1} (q1 q2 : QUD M) (a b : M) : (q1 * q2).r a b ↔ q1.r a b ∧ q2.r a b

@[simp]

theorem QUD.mul_sameAnswer {M : Type u_1} (q1 q2 : QUD M) (m1 m2 : M) : (q1 * q2).sameAnswer m1 m2 = (q1.sameAnswer m1 m2 && q2.sameAnswer m1 m2)

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.r m m'}

theorem QUD.mem_cell_iff_r {M : Type u_1} (q : QUD M) (m m' : M) : m' ∈ q.cell m ↔ q.r m m'

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

theorem QUD.cell_self {M : Type u_1} (q : QUD M) (m : M) : m ∈ q.cell m

theorem QUD.mem_cell_symm {M : Type u_1} (q : QUD M) (m m' : M) : m' ∈ q.cell m ↔ m ∈ q.cell m'

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

Build QUD from a projection function with DecidableEq codomain. The name argument is documentation-only; it is discarded.

Equations

• QUD.ofDecEq project name = { toSetoid := Setoid.comap project ⊥, decR := fun (a b : M) => inst✝ (project a) (project b) }

@[simp]

theorem QUD.ofDecEq_r {M : Type u_1} {α : Type u_2} [DecidableEq α] (project : M → α) (name : String) (w v : M) : (ofDecEq project name).r w v ↔ project w = project v

@[simp]

theorem QUD.ofDecEq_sameAnswer {M : Type u_1} {α : Type u_2} [DecidableEq α] (project : M → α) (name : String) (w v : M) : (ofDecEq project name).sameAnswer w v = decide (project w = project v)

theorem QUD.ofDecEq_sameAnswer_iff {M : Type u_1} {α : Type u_2} [DecidableEq α] (project : M → α) (name : String) (w v : M) : (ofDecEq project name).sameAnswer w v = true ↔ project w = project v

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

Build QUD from a projection function with BEq/LawfulBEq codomain. The name argument is documentation-only; it is discarded.

Equations

• QUD.ofProject f name = { toSetoid := Setoid.comap f ⊥, decR := fun (a b : M) => decidable_of_iff ((f a == f b) = true) ⋯ }

@[simp]

theorem QUD.ofProject_r {M : Type u_1} {A : Type u_2} [BEq A] [LawfulBEq A] (f : M → A) (m1 m2 : M) : (ofProject f).r m1 m2 ↔ f m1 = f m2

@[simp]

theorem QUD.ofProject_sameAnswer {M : Type u_1} {A : Type u_2} [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 u_2} [BEq A] [LawfulBEq A] (f : M → A) (m1 m2 : M) : (ofProject f).sameAnswer m1 m2 = true ↔ f m1 = f m2

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

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

Identity QUD: each meaning is its own equivalence class.

Equations

• QUD.exact = QUD.ofProject id "exact"

@[simp]

theorem QUD.exact_r {M : Type u_1} [BEq M] [LawfulBEq M] (m1 m2 : M) : exact.r m1 m2 ↔ m1 = m2

@[simp]

theorem QUD.exact_sameAnswer {M : Type u_1} [BEq M] [LawfulBEq M] (m1 m2 : M) : exact.sameAnswer m1 m2 = (m1 == m2)

theorem QUD.exact_sameAnswer_iff {M : Type u_1} [BEq M] [LawfulBEq M] (m1 m2 : M) : exact.sameAnswer m1 m2 = true ↔ m1 = m2

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

@[simp]

theorem ProductQUD.fst_sameAnswer {A B : Type} [BEq A] [LawfulBEq A] (p1 p2 : A × B) : fst.sameAnswer p1 p2 = (p1.1 == p2.1)

theorem ProductQUD.fst_sameAnswer_iff {A B : Type} [BEq A] [LawfulBEq A] (p1 p2 : A × B) : fst.sameAnswer p1 p2 = true ↔ p1.1 = p2.1

@[simp]

theorem ProductQUD.snd_sameAnswer {A B : Type} [BEq B] [LawfulBEq B] (p1 p2 : A × B) : snd.sameAnswer p1 p2 = (p1.2 == p2.2)

theorem ProductQUD.snd_sameAnswer_iff {A B : Type} [BEq B] [LawfulBEq B] (p1 p2 : A × B) : snd.sameAnswer p1 p2 = true ↔ p1.2 = p2.2

@[simp]

theorem ProductQUD.both_sameAnswer {A B : Type} [BEq A] [BEq B] [LawfulBEq A] [LawfulBEq B] (p1 p2 : A × B) : both.sameAnswer p1 p2 = (p1 == p2)

theorem ProductQUD.both_sameAnswer_iff {A B : Type} [BEq A] [BEq B] [LawfulBEq A] [LawfulBEq B] (p1 p2 : A × B) : both.sameAnswer p1 p2 = true ↔ p1 = p2