Conservative GQ Lattice

@cite{elliott-2025}

Conservative GQs form a bounded distributive sublattice of GQ α. The DistribLattice instance is inherited from Mathlib's Pi instances (Prop is a DistribLattice, and (α → Prop) → (α → Prop) → Prop lifts pointwise). Closure under ⊔/⊓ follows from conservative_gqJoin/conservative_gqMeet.

def Core.Quantification.conservativeSublattice {α : Type u_1} : Sublattice (GQ α)

Conservative GQs form a sublattice of GQ α. The DistribLattice on GQ α is inherited from Mathlib's Pi instances (Prop is a DistribLattice, and (α → Prop) → (α → Prop) → Prop lifts pointwise). Closure under ⊔/⊓ follows from conservative_gqJoin/conservative_gqMeet (§8).

Reference: Elliott, P. (2025). Determiners as predicates. SALT 35.

Equations

• Core.Quantification.conservativeSublattice = { carrier := {q : Core.Quantification.GQ α | Core.Quantification.Conservative q}, supClosed' := ⋯, infClosed' := ⋯ }

@[reducible, inline]

abbrev Core.Quantification.ConsGQ (α : Type u_2) : Sublattice (GQ α)

Conservative GQs: the subtype of GQ α satisfying conservativity. Forms a bounded distributive lattice under pointwise propositional operations. Meet is ∧, join is ∨, the order is pointwise implication. The Birkhoff representation theorem applied to this lattice yields polarized individuals as join-irreducible elements.

The DistribLattice instance is inherited from GQ α via Sublattice.instDistribLatticeCoe — no manual axiom proofs needed.

Equations

• Core.Quantification.ConsGQ α = Core.Quantification.conservativeSublattice

theorem Core.Quantification.ConsGQ.sup_eq_gqJoin {α : Type u_2} (q₁ q₂ : ↥(ConsGQ α)) : ↑(q₁ ⊔ q₂) = gqJoin ↑q₁ ↑q₂

The join of conservative GQs agrees with gqJoin.

theorem Core.Quantification.ConsGQ.inf_eq_gqMeet {α : Type u_2} (q₁ q₂ : ↥(ConsGQ α)) : ↑(q₁ ⊓ q₂) = gqMeet ↑q₁ ↑q₂

The meet of conservative GQs agrees with gqMeet.

@[implicit_reducible]

instance Core.Quantification.ConsGQ.instBotSubtypeGQMemSublattice {α : Type u_2} : Bot ↥(ConsGQ α)

Equations

• Core.Quantification.ConsGQ.instBotSubtypeGQMemSublattice = { bot := ⟨⊥, ⋯⟩ }

@[implicit_reducible]

instance Core.Quantification.ConsGQ.instTopSubtypeGQMemSublattice {α : Type u_2} : Top ↥(ConsGQ α)

Equations

• Core.Quantification.ConsGQ.instTopSubtypeGQMemSublattice = { top := ⟨⊤, ⋯⟩ }

@[implicit_reducible]

instance Core.Quantification.ConsGQ.instOrderBotSubtypeGQMemSublattice {α : Type u_2} : OrderBot ↥(ConsGQ α)

Equations

• Core.Quantification.ConsGQ.instOrderBotSubtypeGQMemSublattice = { toBot := Core.Quantification.ConsGQ.instBotSubtypeGQMemSublattice, bot_le := ⋯ }

@[implicit_reducible]

instance Core.Quantification.ConsGQ.instOrderTopSubtypeGQMemSublattice {α : Type u_2} : OrderTop ↥(ConsGQ α)

Equations

• Core.Quantification.ConsGQ.instOrderTopSubtypeGQMemSublattice = { toTop := Core.Quantification.ConsGQ.instTopSubtypeGQMemSublattice, le_top := ⋯ }

@[simp]

theorem Core.Quantification.ConsGQ.sup_val {α : Type u_2} (q₁ q₂ : ↥(ConsGQ α)) (R S : α → Prop) : ↑(q₁ ⊔ q₂) R S = (↑q₁ R S ∨ ↑q₂ R S)

@[simp]

theorem Core.Quantification.ConsGQ.inf_val {α : Type u_2} (q₁ q₂ : ↥(ConsGQ α)) (R S : α → Prop) : ↑(q₁ ⊓ q₂) R S = (↑q₁ R S ∧ ↑q₂ R S)

@[simp]

theorem Core.Quantification.ConsGQ.top_val {α : Type u_2} (R S : α → Prop) : ↑⊤ R S = True

@[simp]

theorem Core.Quantification.ConsGQ.bot_val {α : Type u_2} (R S : α → Prop) : ↑⊥ R S = False