Polarized Individuals and the Birkhoff Representation [Ell25]

[vB84]

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

Overview

[Ell25] 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 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 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) [Ell25], §4.3.

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

@[implicit_reducible]

instance Quantification.instDecidableEqTri : DecidableEq Tri

Equations

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

@[implicit_reducible]

instance Quantification.instReprTri : Repr Tri

Equations

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

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

Equations

• Quantification.instReprTri.repr Quantification.Tri.pos prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Quantification.Tri.pos")).group prec✝
• Quantification.instReprTri.repr Quantification.Tri.neg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Quantification.Tri.neg")).group prec✝
• Quantification.instReprTri.repr Quantification.Tri.blank prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Quantification.Tri.blank")).group prec✝

def Quantification.Tri.IsNonBlank : Tri → Prop

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

Equations

• Quantification.Tri.pos.IsNonBlank = True
• Quantification.Tri.neg.IsNonBlank = True
• Quantification.Tri.blank.IsNonBlank = False

def Quantification.Tri.IsPos : Tri → Prop

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

Equations

• Quantification.Tri.pos.IsPos = True
• Quantification.Tri.neg.IsPos = False
• Quantification.Tri.blank.IsPos = False

@[simp]

theorem Quantification.Tri.IsNonBlank_pos : pos.IsNonBlank

@[simp]

theorem Quantification.Tri.IsNonBlank_neg : neg.IsNonBlank

@[simp]

theorem Quantification.Tri.not_IsNonBlank_blank : ¬blank.IsNonBlank

@[simp]

theorem Quantification.Tri.IsPos_pos : pos.IsPos

@[simp]

theorem Quantification.Tri.not_IsPos_neg : ¬neg.IsPos

@[simp]

theorem Quantification.Tri.not_IsPos_blank : ¬blank.IsPos

@[implicit_reducible]

instance Quantification.Tri.instDecidablePredIsNonBlank : DecidablePred IsNonBlank

Equations

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

@[implicit_reducible]

instance Quantification.Tri.instDecidablePredIsPos : DecidablePred IsPos

Equations

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

noncomputable def 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

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

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

Decode the restrictor from a trivalent function.

Equations

• Quantification.triSupport f e = (f e).IsNonBlank

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

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

Equations

• Quantification.triPositive f e = (f e).IsPos

@[simp]

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

@[simp]

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

@[simp]

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

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

Map a predicate on trivalent functions to a GQ. [Ell25], §4.3.2, equation (44).

Equations

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

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

Map a GQ to a predicate on trivalent functions. [Ell25], §4.3.1, equation (40).

Equations

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

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

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

Lift predToGQ into the conservative GQ sublattice.

Equations

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

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

Round-trip: encoding then decoding is the identity.

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

noncomputable def 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 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. [Ell25], §4.3, eq. (43).

@[reducible, inline]

abbrev 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

• Quantification.PolInd α = (α × Bool)

def 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 Quantification.PolInd.toGQ_conservative {α : Type u_2} (x : PolInd α) : Conservative x.toGQ

The GQ of a polarized individual is conservative.

def 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 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 Quantification.PolInd.toConsGQ_val {α : Type u_2} (x : PolInd α) : ↑x.toConsGQ = x.toGQ

theorem Quantification.PolInd.toGQ_pos {α : Type u_2} (e : α) (R S : α → Prop) : toGQ (e, true) R S ↔ R e ∧ S e

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

theorem 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 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 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 Quantification.PolInd.pos_inf_neg {α : Type u_2} (e : α) : toConsGQ (e, true) ⊓ toConsGQ (e, false) = ⊥

theorem 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).

The order on ConsGQ α is pointwise implication, so ≤ unfolds to ∀ R S, toGQ x R S → toGQ y R S. Instantiating at the restrictor (· = x.1) and a scope that selects x's polarity forces y.1 = x.1 (first conjunct) and y.2 = x.2 (the polarity branch).

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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