Merin (1999): Negative Attributes, Partitions, and Rational Decisions

This file formalizes the decision-theoretic rationale in [Mer99b] for attribute spaces being partitions and its epistemic, syntax-independent characterization of negative attributes as proper coarsenings. The complements of a partition's cells form a partition exactly when the partition is binary (compl_isPartition_iff); complement probabilities sum to one less than the number of cells and form a distribution exactly for two cells (sum_compl_prob, sum_compl_prob_eq_one_iff); the binary partition of a proposition and its negation is the coarsest coarsening preserving it (binaryPartition_coarsens); an attribute is negative with respect to a partition when it and some cell properly coarsen it (IsNegativeAttribute); and partition-relative expected utility is the law of total expectation, a coarsening's cell terms regrouping the finer partition's (eu_eq_partitionEU, partitionEU_coarsening_regroup). The paper's claim that re-coverings which neither coarsen nor refine fail compositionality, and the conditional-independence result of [Joh86] it cites, are not represented.

TODO

The paper is not on file; page locators are transcribed from an earlier version of this file and are UNVERIFIED.

References

• [Mer99b]
• [Joh86]

FACT 1: complement families

theorem Merin1999.compl_isPartition_iff {W : Type u_1} [Nonempty W] {F : Set (Set W)} (hF : Setoid.IsPartition F) : Setoid.IsPartition (compl '' F) ↔ F.encard = 2

FACT 1 ([Mer99b] p. 261): for a partition F of a nonempty type, the complements of its cells form a partition iff F has exactly two cells.

FACT 3: complement probabilities

theorem Merin1999.sum_compl_prob {W : Type u_1} [Fintype W] [DecidableEq W] (P : Finpartition Finset.univ) (prior : W → ℚ) (hsum : Finset.univ.sum prior = 1) : ∑ c ∈ P.parts, (Finset.univ \ c).sum prior = ↑P.parts.card - 1

FACT 3 ([Mer99b] p. 261): under a proper prior, the probabilities of the complements of a partition's cells sum to n − 1, n the number of cells.

theorem Merin1999.sum_compl_prob_eq_one_iff {W : Type u_1} [Fintype W] [DecidableEq W] (P : Finpartition Finset.univ) (prior : W → ℚ) (hsum : Finset.univ.sum prior = 1) : ∑ c ∈ P.parts, (Finset.univ \ c).sum prior = 1 ↔ P.parts.card = 2

Merin's FACT 2 ([Mer99b] p. 261), summed form: the complement probabilities form a probability distribution (sum to 1) iff the partition is binary.

Coarsening and negative attributes

@[reducible, inline]

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

Binary partition from a Boolean predicate: two elements are equivalent iff the predicate agrees on both. Negation-induced repartitioning yields exactly these ([Mer99b] §8).

Equations

• Merin1999.binaryPartition p = QUD.ofProject p

theorem Merin1999.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: a proposition and its negation carry the same information.

def Merin1999.IsProperCoarsening {M : Type u_1} [DecidableEq M] (q q' : QUD M) (elements : List M) : Prop

Q properly coarsens Q' over a finite domain: Q coarsens Q' with strictly fewer cells ([Mer99b] p. 262 definition).

Equations

• Merin1999.IsProperCoarsening q q' elements = (q.coarsens q' ∧ q.numCells elements < q'.numCells elements)

theorem Merin1999.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

FACT 4 ([Mer99b] p. 263): {P, ¬P} is the coarsest P-preserving coarsening. Any partition whose cells respect P — in particular any P-preserving coarsening of a given partition — is refined by the binary partition of P.

def Merin1999.IsNegativeAttribute {M : Type u_1} [DecidableEq M] (R : M → Bool) (q : QUD M) (elements : List M) : Prop

R is a negative attribute with respect to q ([Mer99b] p. 263): the complement of R is a cell of q, and the two-cell partition {R, ¬R} properly coarsens q. Negativity is epistemic (partition-kinetic), not morphological.

Equations

• Merin1999.IsNegativeAttribute R q elements = ((∃ (w : M), ∀ (v : M), q.sameAnswer w v = true ↔ R v = false) ∧ Merin1999.IsProperCoarsening (Merin1999.binaryPartition R) q elements)

EU compositionality under coarsening

def Merin1999.partitionEU {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] (dp : Core.DecisionTheory.DecisionProblem ℚ M A) (q : QUD M) (a : A) : ℚ

Expected utility computed via a partition: weight each cell's conditional EU by the cell's probability (EU_Q(a) = Σ_{c ∈ cells Q} P(c) · EU(a | c)).

Equations

• Merin1999.partitionEU dp q a = ∑ cell ∈ q.toCellsFinset Finset.univ, cell.sum dp.prior * dp.condExpectedUtility cell a

theorem Merin1999.eu_eq_partitionEU {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] (dp : Core.DecisionTheory.DecisionProblem ℚ M A) (a : A) (q : QUD M) (hprior : ∀ (w : M), dp.prior w ≥ 0) : dp.expectedUtility a = partitionEU dp q a

Law of total expectation: the unconditional expected utility equals the partition-relative EU, for any partition (non-negative priors).

theorem Merin1999.partitionEU_congr {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] (dp : Core.DecisionTheory.DecisionProblem ℚ M A) (q q' : QUD M) (a : A) (hprior : ∀ (w : M), dp.prior w ≥ 0) : partitionEU dp q a = partitionEU dp q' a

Partition-relative EU is partition-independent: any two partitions compute the unconditional EU. [Mer99b] p. 264 is the coarsening instance; the paper's FACT 5 — that non-coarsening re-coverings fail term-by-term re-usability — is not formalized.

theorem Merin1999.partitionEU_coarsening_regroup {M : Type u_1} {A : Type u_2} [Fintype M] [DecidableEq M] (dp : Core.DecisionTheory.DecisionProblem ℚ M A) {q q' : QUD M} (a : A) (hcoarse : q'.coarsens q) (hprior : ∀ (w : M), dp.prior w ≥ 0) : partitionEU dp q' a = ∑ c' ∈ q'.toCellsFinset Finset.univ, ∑ c ∈ q.toCellsFinset Finset.univ with c ⊆ c', c.sum dp.prior * dp.condExpectedUtility c a

EU compositionality under coarsening ([Mer99b] p. 264): each coarse cell's term is the sum of the terms of the fine cells it groups, so a coarsening re-uses the finer partition's computations.