Binary Partitions and P-Preserving Coarsenings

@cite{merin-1999}

Yes/no partitions induced by Boolean predicates, plus the coarsest P-preserving coarsening of a given partition:

• binaryPartition p — equivalence by agreement on p. Building block of proper coarsening: every refinement step that merges two cells is a binary partition.
• complement_same_partition — p and !p carry the same information.
• coarsestPreserving q P = q * binaryPartition P — the finest partition that refines q and still distinguishes P-worlds from ¬P-worlds. Universality property: any q'-refinement that preserves P also refines this construction.

Used by Core/Question/Partition/Negativity.lean for Merin's epistemic characterization of negative attributes.

Binary Partitions

@[reducible, inline]

abbrev QUD.binaryPartition {M : Type u_1} (p : M → Bool) : QUD M

Binary partition from a Boolean predicate. Two elements are equivalent iff the predicate gives the same value on both.

Binary partitions are the building blocks of coarsening: every proper coarsening can be decomposed into steps that merge exactly two cells, each corresponding to a binary partition. @cite{merin-1999} characterizes negative attributes entirely in terms of binary partition coarsening.

Equations

• QUD.binaryPartition p = QUD.ofProject p

theorem QUD.complement_same_partition {M : Type u_1} (p : M → Bool) (w v : M) : (binaryPartition p).sameAnswer w v = (binaryPartition fun (m : M) => !p m).sameAnswer w v

Complement predicates induce the same binary partition.

@cite{merin-1999}: a proposition and its negation carry exactly the same information. {P-worlds, ¬P-worlds} = {¬P-worlds, P-worlds} as partitions.

theorem QUD.binaryPartition_coarsens {M : Type u_1} (q : QUD M) (p : M → Bool) (h : ∀ (w v : M), q.sameAnswer w v = true → p w = p v) : (binaryPartition p).coarsens q

A binary partition from a predicate that respects q's equivalence classes is a coarsening of q. Every "coarser" yes/no distinction is a coarsening.

Coarsest P-Preserving Coarsening (@cite{merin-1999}, Fact 3)

def QUD.coarsestPreserving {M : Type u_1} (q : QUD M) (P : M → Bool) : QUD M

The coarsest coarsening of Q that preserves predicate P.

Two elements are equivalent iff they are Q-equivalent AND agree on P. This is the meet of Q with the binary partition of P: the finest partition that is coarser than both Q and binaryPartition P.

@cite{merin-1999}: for any proposition P and partition Q, this is the unique coarsest partition that refines Q while still distinguishing P-worlds from ¬P-worlds within each Q-cell.

Equations

• q.coarsestPreserving P = q * QUD.binaryPartition P

theorem QUD.coarsestPreserving_refines {M : Type u_1} (q : QUD M) (P : M → Bool) : (q.coarsestPreserving P).refines q

The P-preserving coarsening refines Q (it can only be finer).

theorem QUD.coarsestPreserving_preserves_P {M : Type u_1} (q : QUD M) (P : M → Bool) (w v : M) (h : (q.coarsestPreserving P).sameAnswer w v = true) : P w = P v

The P-preserving coarsening respects P: equivalent elements agree on P.

theorem QUD.coarsestPreserving_universal {M : Type u_1} (q q' : QUD M) (P : M → Bool) (hrefines : q'.refines q) (hpreserves : ∀ (w v : M), q'.sameAnswer w v = true → P w = P v) : q'.refines (q.coarsestPreserving P)

Any partition that refines Q and preserves P also refines the P-preserving coarsening. This is the universality property: coarsestPreserving is the coarsest such partition.