Polarized Individuals and the Birkhoff Representation @cite{elliott-2025}

@cite{van-benthem-1984}

Entity–polarity pairs, trivalent functions, and the Birkhoff representation theorem for conservative GQs.

Overview

@cite{elliott-2025} argues that determiners denote sets of polarized individuals — entity–polarity pairs (e, ±) that encode whether an entity witnesses the restrictor ∩ scope (positive) or the restrictor ∖ scope (negative). The conservative GQ lattice (ConsGQ, §12 of Core.Logic.Quantification) is the algebraic setting.

The module is organized in five sections:

1. Trivalent values (Tri): three-valued type {pos, neg, blank} encoding an entity's status relative to a quantifier.

2. Encoding/decoding (triFunction, triSupport, triPositive): round-trip between (R, S) predicate pairs and trivalent functions α → Tri. This gives the concrete representation of the polarized domain D_e^± from Elliott §4.3.

3. Birkhoff representation (consGQOrderIso): the order-isomorphism ConsGQ α ≃o ((α → Tri) → Bool), using mathlib's Equiv.toOrderIso. This is the concrete Birkhoff representation: conservative GQs are exactly predicates on trivalent functions. Conservativity is a structural consequence of the encoding — predToGQ_conservative shows any predicate on trivalent functions yields a conservative GQ.

4. Entity–polarity pairs (PolInd α = α × Bool): the compositionally useful type. A polarized individual (e, p) maps to the GQ λ R S => R(e) ∧ (S(e) ↔ p) via polarized functional application. Under the Birkhoff representation, each PolInd corresponds to an atomic predicate checking a single entity's polarity.

5. Boolean algebra structure: ConsGQ α is a Boolean algebra.

inductive Core.Quantification.Tri : Type

Trivalent value: the polarity of an entity relative to a quantifier.

• pos: entity is in restrictor ∩ scope
• neg: entity is in restrictor ∖ scope
• blank: entity is irrelevant (not constrained by the quantifier) @cite{elliott-2025}, §4.3.

• pos : Tri
• neg : Tri
• blank : Tri

instance Core.Quantification.instDecidableEqTri : DecidableEq Tri

Equations

• Core.Quantification.instDecidableEqTri x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Quantification.instReprTri : Repr Tri

Equations

• Core.Quantification.instReprTri = { reprPrec := Core.Quantification.instReprTri.repr }

def Core.Quantification.instReprTri.repr : Tri → ℕ → Std.Format

Equations

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

def Core.Quantification.instBEqTri.beq : Tri → Tri → Bool

Equations

• Core.Quantification.instBEqTri.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Quantification.instBEqTri : BEq Tri

Equations

• Core.Quantification.instBEqTri = { beq := Core.Quantification.instBEqTri.beq }

def Core.Quantification.Tri.isNonBlank : Tri → Bool

Check whether a trivalent value is non-blank (= in the restrictor).

Equations

• Core.Quantification.Tri.pos.isNonBlank = true
• Core.Quantification.Tri.neg.isNonBlank = true
• Core.Quantification.Tri.blank.isNonBlank = false

def Core.Quantification.Tri.isPos : Tri → Bool

Check whether a trivalent value is positive (= in restrictor ∩ scope).

Equations

• Core.Quantification.Tri.pos.isPos = true
• Core.Quantification.Tri.neg.isPos = false
• Core.Quantification.Tri.blank.isPos = false

@[simp]

theorem Core.Quantification.Tri.isNonBlank_pos : pos.isNonBlank = true

@[simp]

theorem Core.Quantification.Tri.isNonBlank_neg : neg.isNonBlank = true

@[simp]

theorem Core.Quantification.Tri.isNonBlank_blank : blank.isNonBlank = false

@[simp]

theorem Core.Quantification.Tri.isPos_pos : pos.isPos = true

@[simp]

theorem Core.Quantification.Tri.isPos_neg : neg.isPos = false

@[simp]

theorem Core.Quantification.Tri.isPos_blank : blank.isPos = false

def Core.Quantification.triFunction {α : Type u_1} (R S : α → Bool) : α → Tri

Encode a (restrictor, scope) pair as a trivalent function. pos = R ∩ S, neg = R ∖ S, blank = outside R.

Equations

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

def Core.Quantification.triSupport {α : Type u_1} (f : α → Tri) : α → Bool

Decode the restrictor from a trivalent function.

Equations

• Core.Quantification.triSupport f e = (f e).isNonBlank

def Core.Quantification.triPositive {α : Type u_1} (f : α → Tri) : α → Bool

Decode the positive part (R ∩ S) from a trivalent function.

Equations

• Core.Quantification.triPositive f e = (f e).isPos

@[simp]

theorem Core.Quantification.triSupport_triFunction {α : Type u_1} (R S : α → Bool) : triSupport (triFunction R S) = R

@[simp]

theorem Core.Quantification.triPositive_triFunction {α : Type u_1} (R S : α → Bool) : triPositive (triFunction R S) = fun (e : α) => R e && S e

@[simp]

theorem Core.Quantification.triFunction_decode {α : Type u_1} (f : α → Tri) : triFunction (triSupport f) (triPositive f) = f

def Core.Quantification.predToGQ {α : Type u_1} (P : (α → Tri) → Bool) : GQ α

Map a predicate on trivalent functions to a GQ. @cite{elliott-2025}, §4.3.2, equation (44).

Equations

• Core.Quantification.predToGQ P R S = P (Core.Quantification.triFunction R S)

def Core.Quantification.gqToPred {α : Type u_1} (Q : GQ α) : (α → Tri) → Bool

Map a conservative GQ to a predicate on trivalent functions. @cite{elliott-2025}, §4.3.1, equation (40).

Equations

• Core.Quantification.gqToPred Q f = Q (Core.Quantification.triSupport f) (Core.Quantification.triPositive f)

theorem Core.Quantification.predToGQ_conservative {α : Type u_1} (P : (α → Tri) → Bool) : Conservative (predToGQ P)

def Core.Quantification.predToConsGQ {α : Type u_1} (P : (α → Tri) → Bool) : ↥(ConsGQ α)

Lift predToGQ into the conservative GQ sublattice.

Equations

• Core.Quantification.predToConsGQ P = ⟨Core.Quantification.predToGQ P, ⋯⟩

theorem Core.Quantification.gqToPred_predToGQ {α : Type u_1} (P : (α → Tri) → Bool) : gqToPred (predToGQ P) = P

Round-trip: encoding then decoding is the identity.

theorem Core.Quantification.predToConsGQ_gqToPred {α : Type u_1} (Q : ↥(ConsGQ α)) : predToConsGQ (gqToPred ↑Q) = Q

Round-trip: decoding then encoding a conservative GQ is the identity. Uses conservativity in the key step.

@[simp]

theorem Core.Quantification.predToConsGQ_val {α : Type u_1} (P : (α → Tri) → Bool) (R S : α → Bool) : ↑(predToConsGQ P) R S = P (triFunction R S)

def Core.Quantification.consGQOrderIso {α : Type u_1} : ↥(ConsGQ α) ≃o ((α → Tri) → Bool)

Birkhoff Representation for ConsGQ.

Conservative GQs are order-isomorphic to predicates on trivalent functions (= the powerset of the polarized domain D_e^±).

This is the concrete Birkhoff representation: the abstract version (OrderIso.lowerSetSupIrred in Mathlib.Order.Birkhoff) identifies any finite distributive lattice with the lattice of lower sets of its sup-irreducible elements. Our isomorphism makes this explicit for ConsGQ using Equiv.toOrderIso from mathlib.

The isomorphism is constructive and works for any α, not just finite types.

Equations

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

theorem Core.Quantification.predToGQ_gqToPred_eq {α : Type u_1} (Q : GQ α) (R S : α → Bool) : predToGQ (gqToPred Q) R S = Q R fun (x : α) => R x && S x

For any GQ (not necessarily conservative), the Birkhoff round-trip replaces S with R ∩ S. Conservative GQs are exactly those for which this substitution is the identity. Non-conservative determiners cannot be expressed as predicates on trivalent functions. @cite{elliott-2025}, §4.3, eq. (43).

@[reducible, inline]

abbrev Core.Quantification.PolInd (α : Type u_2) : Type u_2

Polarized individual: an entity paired with a polarity. (e, true) = positive (e⁺): entity witnesses restrictor ∩ scope. (e, false) = negative (e⁻): entity witnesses restrictor ∖ scope.

Equations

• Core.Quantification.PolInd α = (α × Bool)

def Core.Quantification.PolInd.toGQ {α : Type u_2} (x : PolInd α) : GQ α

GQ denotation via polarized functional application. ⟦(e, p)⟧(R, S) = R(e) ∧ (S(e) ↔ p).

• (e, true): R(e) ∧ S(e) — entity in restrictor ∩ scope
• (e, false): R(e) ∧ ¬S(e) — entity in restrictor ∖ scope

Equations

• x.toGQ R S = (R x.1 && S x.1 == x.2)

theorem Core.Quantification.PolInd.toGQ_conservative {α : Type u_2} (x : PolInd α) : Conservative x.toGQ

The GQ of a polarized individual is conservative.

def Core.Quantification.PolInd.toConsGQ {α : Type u_2} (x : PolInd α) : ↥(ConsGQ α)

Lift a polarized individual into the conservative GQ sublattice.

Equations

• x.toConsGQ = ⟨x.toGQ, ⋯⟩

@[simp]

theorem Core.Quantification.PolInd.toGQ_apply {α : Type u_2} (x : PolInd α) (R S : α → Bool) : x.toGQ R S = (R x.1 && S x.1 == x.2)

@[simp]

theorem Core.Quantification.PolInd.toConsGQ_val {α : Type u_2} (x : PolInd α) : ↑x.toConsGQ = x.toGQ

theorem Core.Quantification.PolInd.toGQ_pos {α : Type u_2} (e : α) (R S : α → Bool) : toGQ (e, true) R S = (R e && S e)

theorem Core.Quantification.PolInd.toGQ_neg {α : Type u_2} (e : α) (R S : α → Bool) : toGQ (e, false) R S = (R e && !S e)

theorem Core.Quantification.PolInd.toGQ_pos_eq_individual {α : Type u_2} (e : α) (R S : α → Bool) : toGQ (e, true) R S = (R e && individual e S)

The positive polarized individual (e, true) restricts the Montagovian individual individual e to entities in the restrictor.

theorem Core.Quantification.PolInd.toGQ_eq_predToGQ {α : Type u_2} (x : PolInd α) : x.toGQ = predToGQ fun (f : α → Tri) => (f x.1).isNonBlank && (f x.1).isPos == x.2

Under the Birkhoff representation, an entity-polarity pair corresponds to an atomic predicate: (e, p) maps to the predicate that checks whether e is in the restrictor and has matching polarity in the trivalent function.

theorem Core.Quantification.PolInd.pos_sup_neg {α : Type u_2} (e : α) : toConsGQ (e, true) ⊔ toConsGQ (e, false) = ⟨fun (R x : α → Bool) => R e, ⋯⟩

Positive and negative polarized individuals for the same entity are complementary within the restrictor: their join covers all cases where e ∈ R, and their meet is ⊥ (restricted to R).

This is the lattice-theoretic content of the "split reading": e⁺ ⊔ e⁻ = λR S. R(e) (the individual-restrictor GQ).

theorem Core.Quantification.PolInd.pos_inf_neg {α : Type u_2} (e : α) : toConsGQ (e, true) ⊓ toConsGQ (e, false) = ⊥

theorem Core.Quantification.PolInd.toConsGQ_le_iff {α : Type u_2} [DecidableEq α] (x y : PolInd α) : x.toConsGQ ≤ y.toConsGQ ↔ x = y

toConsGQ x ≤ toConsGQ y iff x = y: distinct polarized individuals are incomparable in the ConsGQ lattice (they form an antichain).

theorem Core.Quantification.PolInd.toConsGQ_injective {α : Type u_2} [DecidableEq α] : Function.Injective toConsGQ

The embedding is order-reflecting: an injection into ConsGQ α.

instance Core.Quantification.instComplSubtypeGQMemSublatticeConsGQ {α : Type u_2} : Compl ↥(ConsGQ α)

Equations

• Core.Quantification.instComplSubtypeGQMemSublatticeConsGQ = { compl := fun (q : ↥(Core.Quantification.ConsGQ α)) => ⟨fun (R S : α → Bool) => !↑q R S, ⋯⟩ }

instance Core.Quantification.instSDiffSubtypeGQMemSublatticeConsGQ {α : Type u_2} : SDiff ↥(ConsGQ α)

Equations

• Core.Quantification.instSDiffSubtypeGQMemSublatticeConsGQ = { sdiff := fun (q₁ q₂ : ↥(Core.Quantification.ConsGQ α)) => q₁ ⊓ q₂ᶜ }

instance Core.Quantification.instHImpSubtypeGQMemSublatticeConsGQ {α : Type u_2} : HImp ↥(ConsGQ α)

Equations

• Core.Quantification.instHImpSubtypeGQMemSublatticeConsGQ = { himp := fun (q₁ q₂ : ↥(Core.Quantification.ConsGQ α)) => q₂ ⊔ q₁ᶜ }

instance Core.Quantification.instBooleanAlgebraSubtypeGQMemSublatticeConsGQ {α : Type u_2} : BooleanAlgebra ↥(ConsGQ α)

Equations

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

@[simp]

theorem Core.Quantification.ConsGQ.compl_val {α : Type u_2} (q : ↥(ConsGQ α)) (R S : α → Bool) : ↑qᶜ R S = !↑q R S