Polarity–Partition Bridge

@cite{icard-2012} @cite{merin-1999}

Connects the natural logic algebra (Core.NaturalLogic) to partition structure (Core.Partition), formalizing @cite{merin-1999}'s central insight: negativity is coarsening.

Key connections

1. NLRelation.negation (A∩B=∅, A∪B=U) corresponds to partition identity: complements induce the same binary partition (complements_same_partition).

2. ContextPolarity.downward (DE) corresponds to partition coarsening: a DE context maps refinements to coarsenings.

3. negationSig ^ 2 = addMult (double negation = morphism) corresponds to double complement being the identity on partitions (double_complement_same_partition).

Design

Core.NaturalLogic is the algebraic root: EntailmentSig, ContextPolarity, NLRelation define the abstract algebra of entailment and polarity. Core.Partition provides the partition lattice on QUD. This module connects them: the NL algebra governs partition structure.

def Core.PolarityPartition.AreComplements {M : Type u_1} (p q : M → Bool) : Prop

Two predicates are pointwise complements. This is the semantic content of NLRelation.negation (A∩B=∅ and A∪B=U) instantiated to Boolean predicates on a type M.

Equations

• Core.PolarityPartition.AreComplements p q = ∀ (m : M), q m = !p m

theorem Core.PolarityPartition.complements_same_partition {M : Type u_1} (p q : M → Bool) (h : AreComplements p q) (w v : M) : (QUD.binaryPartition p).sameAnswer w v = (QUD.binaryPartition q).sameAnswer w v

Complementary predicates (NLRelation.negation) induce identical binary partitions. This grounds the set-theoretic NL relation in partition structure: complements carry the same information content.

This is @cite{merin-1999} via the NL relation algebra.

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

Double complement returns to the same partition.

Partition-theoretic content of negationSig ^ 2 = addMult: complement ∘ complement is the identity on partitions. The algebraic fact that the anti-morphism signature is self-inverse is visible in partition structure as double complement preserving all cells.

theorem Core.PolarityPartition.complement_preserves_coarsening {M : Type u_1} (q : QUD M) (R : M → Bool) (h : (QUD.binaryPartition R).coarsens q) : (QUD.binaryPartition fun (m : M) => !R m).coarsens q

Complement preserves the coarsening relation.

If the binary partition of R is a coarsening of Q, then so is the binary partition of ¬R. This follows immediately from complement_same_partition: the two partitions are identical, so they coarsen the same things.

This is the partition-theoretic reading of DE: complement doesn't change the information structure.

theorem Core.PolarityPartition.complement_equally_negative_coarsening {M : Type u_1} (R : M → Bool) (q : QUD M) : (QUD.binaryPartition R).coarsens q ↔ (QUD.binaryPartition fun (m : M) => !R m).coarsens q

A negative attribute and its complement are equally negative (coarsening direction).

Merin's fundamental insight: negativity is not about morphological negation ("un-", "not") but about the partition a predicate induces. Since complements induce the same partition, R is a negative attribute iff ¬R is.

Syntactic negation markers are surface cues for partition coarsening, but the underlying property is purely information-theoretic.