Dimensional Aggregation for Multidimensional Predicates

General mechanisms for combining dimensional assessments into overall predicate application. These apply to any multi-dimensional predicate — gradable adjectives (@cite{dambrosio-hedden-2024}, @cite{sassoon-2013}), artifact nouns (@cite{waldon-etal-2023}, @cite{sassoon-fadlon-2017}), and disturbance predicates (@cite{tham-2025}).

Aggregation is analogous to preference aggregation in social choice theory. Arrow's impossibility theorem and its escape routes characterize the available aggregation functions:

• Counting (§1): x is F iff ≥k dimensions are satisfied. Subsumes @cite{sassoon-2013}'s conjunctive (k=n) and disjunctive (k=1).
• Majority (§1): x is F iff a strict majority of dimensions are satisfied.
• Weighted (§2): x is F iff Σᵢ wᵢ·fᵢ(x) ≥ θ (utilitarian aggregation). Subsumes @cite{tham-2025}'s eq. 47b and @cite{waldon-etal-2023}'s eq. 8.
• Multiplicative (§4): x is F iff Πᵢ fᵢ(x) ≥ θ (Cobb-Douglas aggregation). @cite{sassoon-fadlon-2017} argue natural kinds compose multiplicatively: failure on ANY dimension kills membership.

The weighted score is unified over ℚ-valued measure functions. Bool-valued dimension predicates are a special case via boolMeasures.

def Semantics.Degree.Aggregation.countBinding {α : Type} (k : ℕ) (dims : List (α → Bool)) (x : α) : Bool

Counting aggregation: x satisfies the predicate iff at least k of the dimension predicates in dims return true for x.

Generalizes @cite{sassoon-2013}'s binding types:

• k = dims.length → conjunctive (∀ dims)
• k = 1 → disjunctive (∃ dim)
• intermediate k → mixed / "dimension counting"

Equations

• Semantics.Degree.Aggregation.countBinding k dims x = decide ((List.filter (fun (d : α → Bool) => d x) dims).length ≥ k)

def Semantics.Degree.Aggregation.majorityBinding {α : Type} (dims : List (α → Bool)) (x : α) : Bool

Majority binding: x satisfies the predicate iff a strict majority of dimensions are satisfied. May's theorem (1952) characterizes this as the unique aggregation rule satisfying neutrality, anonymity, and positive responsiveness.

Equations

• Semantics.Degree.Aggregation.majorityBinding dims x = decide (2 * (List.filter (fun (d : α → Bool) => d x) dims).length > dims.length)

def Semantics.Degree.Aggregation.boolMeasures {α : Type} (dims : List (α → Bool)) : List (α → ℚ)

Lift Bool dimension predicates to ℚ-valued measure functions. Each d : α → Bool becomes fun x => if d x then 1 else 0.

Equations

• Semantics.Degree.Aggregation.boolMeasures dims = List.map (fun (d : α → Bool) (x : α) => if d x = true then 1 else 0) dims

def Semantics.Degree.Aggregation.weightedScore {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (x : α) : ℚ

Weighted score: Σᵢ wᵢ · fᵢ(x), where each fᵢ : α → ℚ is a measure function along one dimension.

This is the unified core: @cite{waldon-etal-2023}'s eq. (8) uses ℚ-valued measures directly; @cite{dambrosio-hedden-2024}'s Bool dimensions are the special case via boolMeasures.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Degree.Aggregation.weightedBinding {α : Type} (weights : List ℚ) (θ : ℚ) (dims : List (α → Bool)) (x : α) : Bool

Weighted binding (Bool dimensions): x is F iff its weighted score over Bool-lifted measures exceeds threshold θ.

Equations

• Semantics.Degree.Aggregation.weightedBinding weights θ dims x = decide (Semantics.Degree.Aggregation.weightedScore weights (Semantics.Degree.Aggregation.boolMeasures dims) x ≥ θ)

def Semantics.Degree.Aggregation.weightedBindingQ {α : Type} (weights : List ℚ) (θ : ℚ) (measures : List (α → ℚ)) (x : α) : Bool

Weighted binding over continuous ℚ-valued measures.

Equations

• Semantics.Degree.Aggregation.weightedBindingQ weights θ measures x = decide (Semantics.Degree.Aggregation.weightedScore weights measures x ≥ θ)

theorem Semantics.Degree.Aggregation.countBinding_zero {α : Type} (dims : List (α → Bool)) (x : α) : countBinding 0 dims x = true

Counting with threshold 0 is always satisfied (vacuously true).

def Semantics.Degree.Aggregation.multiplicativeScore {α : Type} (measures : List (α → ℚ)) (x : α) : ℚ

Multiplicative (Cobb-Douglas) score: Πᵢ fᵢ(x). @cite{sassoon-fadlon-2017} argue natural kind nouns compose multiplicatively: failure on ANY single dimension kills membership. Contrast with additive weightedScore for artifact nouns.

Equations

• Semantics.Degree.Aggregation.multiplicativeScore measures x = List.foldl (fun (acc : ℚ) (f : α → ℚ) => acc * f x) 1 measures

inductive Semantics.Degree.Aggregation.AggregationType : Type

Classification of dimensional aggregation mechanisms. Each type corresponds to an escape route from Arrow's impossibility.

• counting : AggregationType

  Threshold counting (rejects WO via non-transitivity or incompleteness).

• utilitarian : AggregationType

  Weighted sum / utilitarian (rejects ONC, accepts interval scale IUC).

• cobbDouglas : AggregationType

  Weighted product / Cobb-Douglas (rejects ONC, accepts ratio scale RNC).

def Semantics.Degree.Aggregation.instReprAggregationType.repr : AggregationType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Semantics.Degree.Aggregation.instReprAggregationType : Repr AggregationType

Equations

• Semantics.Degree.Aggregation.instReprAggregationType = { reprPrec := Semantics.Degree.Aggregation.instReprAggregationType.repr }

instance Semantics.Degree.Aggregation.instDecidableEqAggregationType : DecidableEq AggregationType

Equations

• Semantics.Degree.Aggregation.instDecidableEqAggregationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Degree.Aggregation.instBEqAggregationType : BEq AggregationType

Equations

• Semantics.Degree.Aggregation.instBEqAggregationType = { beq := Semantics.Degree.Aggregation.instBEqAggregationType.beq }

def Semantics.Degree.Aggregation.instBEqAggregationType.beq : AggregationType → AggregationType → Bool

Equations

• Semantics.Degree.Aggregation.instBEqAggregationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)