Merin (1999) — Why Not Speak Notspeak

[Mer99b]

[Mer99b] "Negative Attributes, Partitions, and Rational Decisions" gives a decision-theoretic rationale for attribute spaces being partitions and a purely epistemic, syntax-independent characterization of negative attributes as proper coarsenings.

Formalized:

• FACT 1 (p. 261): the complements of a partition's cells form a partition iff the partition is binary (compl_isPartition_iff).
• FACT 3 (p. 261): complement probabilities sum to n − 1 (sum_compl_prob); they form a distribution iff n = 2 (sum_compl_prob_eq_one_iff, Merin's FACT 2).
• Coarsening (p. 262): IsProperCoarsening; negation-induced binary partitions (binaryPartition, complement_same_partition).
• FACT 4 (p. 263): {P, ¬P} is the coarsest P-preserving coarsening (binaryPartition_coarsens).
• Negative attributes (p. 263): R is negative w.r.t. partition F iff {R, Q} properly coarsens F for some cell Q ∈ F (IsNegativeAttribute).
• EU compositionality under coarsening (p. 264): partition-relative expected utility is the law of total expectation (eu_eq_partitionEU), and a coarsening's cell terms regroup the finer partition's terms (partitionEU_coarsening_regroup).

Not formalized: FACT 5 (pp. 264–265), that re-coverings which neither coarsen nor refine fail compositionality (an existence claim over discrete measures), and the [Joh86] conditional-independence result motivating binary partitions in epistemic kinetics (§8, cited by Merin, not proved there).

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.