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) → Prop), 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

@[implicit_reducible]

instance Core.Quantification.instDecidableEqTri : DecidableEq Tri

Equations

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

@[implicit_reducible]

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.Tri.IsNonBlank : Tri → Prop

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 → Prop

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

@[simp]

theorem Core.Quantification.Tri.IsNonBlank_neg : neg.IsNonBlank

@[simp]

theorem Core.Quantification.Tri.not_IsNonBlank_blank : ¬blank.IsNonBlank

@[simp]

theorem Core.Quantification.Tri.IsPos_pos : pos.IsPos

@[simp]

theorem Core.Quantification.Tri.not_IsPos_neg : ¬neg.IsPos

@[simp]

theorem Core.Quantification.Tri.not_IsPos_blank : ¬blank.IsPos

@[implicit_reducible]

instance Core.Quantification.Tri.instDecidablePredIsNonBlank : DecidablePred IsNonBlank

Equations

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

@[implicit_reducible]

instance Core.Quantification.Tri.instDecidablePredIsPos : DecidablePred IsPos

Equations

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

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

Encode a (restrictor, scope) pair as a trivalent function. pos = R ∩ S, neg = R ∖ S, blank = outside R. Noncomputable: uses classical decidability of the input predicates.

Equations

• Core.Quantification.triFunction R S e = if R e then if S e then Core.Quantification.Tri.pos else Core.Quantification.Tri.neg else Core.Quantification.Tri.blank

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

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) : α → Prop

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 : α → Prop) : triSupport (triFunction R S) = R

@[simp]

theorem Core.Quantification.triPositive_triFunction {α : Type u_1} (R S : α → Prop) : 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

noncomputable def Core.Quantification.predToGQ {α : Type u_1} (P : (α → Tri) → Prop) : 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) → Prop

Map a 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) → Prop) : Conservative (predToGQ P)

noncomputable def Core.Quantification.predToConsGQ {α : Type u_1} (P : (α → Tri) → Prop) : ↥(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) → Prop) : 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) → Prop) (R S : α → Prop) : ↑(predToConsGQ P) R S = P (triFunction R S)

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

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 in shape (though predToGQ is noncomputable due to classical decidability) and works for any α.

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 : α → Prop) : 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, true)⟧(R, S) = R(e) ∧ S(e) — entity in restrictor ∩ scope. ⟦(e, false)⟧(R, S) = R(e) ∧ ¬S(e) — entity in restrictor ∖ scope.

Equations

• x.toGQ R S = (R x.1 ∧ if x.2 = true then S x.1 else ¬S x.1)

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 : α → Prop) : x.toGQ R S = (R x.1 ∧ if x.2 = true then S x.1 else ¬S x.1)

@[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 : α → Prop) : toGQ (e, true) R S ↔ R e ∧ S e

theorem Core.Quantification.PolInd.toGQ_neg {α : Type u_2} (e : α) (R S : α → Prop) : toGQ (e, false) R S ↔ R e ∧ ¬S e

theorem Core.Quantification.PolInd.toGQ_pos_eq_individual {α : Type u_2} (e : α) (R S : α → Prop) : 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 ∧ if x.2 = true then (f x.1).IsPos else ¬(f x.1).IsPos

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 : α → Prop) => 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).

TODO: revive proof after Bool→Prop GQ migration. The original proof instantiates the implication at a witness pair (· = x.1, λ _ => x.2); after the migration, the subtype ≤ no longer applies as cleanly and the case-split on x.2 / y.2 interacts awkwardly with Prop equality. The downstream code uses pos_sup_neg/pos_inf_neg rather than this antichain lemma, so the gap is non-blocking.

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

noncomputable 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 : α → Prop) : ↑qᶜ R S = ¬↑q R S