GQ Generators: Meets and Joins of Individual Quantifiers

@cite{xiang-2016} @cite{elliott-nicolae-sauerland-2022}

Conjunction and disjunction GQs as iterated meet/join of Montagovian individual quantifiers in the NPQ Boolean algebra.

Given a domain of entities, each entity lifts to its principal ultrafilter (individual). The conjunction GQ over a subset X is the infimum ⨅{x ∈ X} individual(x), and the disjunction GQ is the supremum ⨆{x ∈ X} individual(x). These recover universal and existential quantification over X as lattice operations.

Architecture

NPQ α = (α → Prop) → Prop inherits a full BooleanAlgebra from Mathlib's Pi instances over Prop. All definitions here are stated directly in terms of Mathlib's ⊓/⊔/⊤/⊥/≤. The propositional characterizations (conjGQ X P ↔ ∀ x ∈ X, P x, disjGQ X P ↔ ∃ x ∈ X, P x) are derived theorems, not definitions — the definitions express the lattice-theoretic content directly.

Key Definitions

• conjGQ X — ⨅_{x ∈ X} individual(x) via iterated ⊓
• disjGQ X — ⨆_{x ∈ X} individual(x) via iterated ⊔
• conjGQs dom / disjGQs dom — all non-empty sub-meets / sub-joins

Key Theorems

• conjGQ_iff_forall / disjGQ_iff_exists — propositional characterization
• conjGQ_cons / disjGQ_cons — recursive decomposition (definitional)
• conjGQ_le_individual + le_conjGQ — glb characterization via ≤
• individual_le_disjGQ + disjGQ_le — lub characterization via ≤
• conjGQ_antitone / disjGQ_monotone — subset monotonicity
• individual_le_disjGQ_iff — individual quantifiers are join-prime
• deMorgan_conj / deMorgan_disj — De Morgan duality
• conjGQ_append / disjGQ_append — compositionality

def Core.Quantification.conjGQ {α : Type u_1} (X : List α) : NPQ α

Conjunction GQ: iterated meet of individual quantifiers.

⊓(X) = ⨅_{x ∈ X} individual(x)

Defined as a right fold of ⊓ over individual lifts, starting from ⊤ (the tautological quantifier). For singleton X = {a}, this recovers individual a (the principal ultrafilter generated by a). For X = {a, b}, this is individual a ⊓ individual b: the unique GQ that holds of P iff both a and b have P.

@cite{xiang-2016}: conjunction GQs range over non-empty subsets of an entity domain, generating the "conjunctive" answers to questions.

Equations

• Core.Quantification.conjGQ X = List.foldr (fun (a : α) (acc : Core.Quantification.NPQ α) => Core.Quantification.individual a ⊓ acc) ⊤ X

def Core.Quantification.disjGQ {α : Type u_1} (X : List α) : NPQ α

Disjunction GQ: iterated join of individual quantifiers.

⊔(X) = ⨆_{x ∈ X} individual(x)

@cite{xiang-2016}: disjunction GQs generate "disjunctive" answers.

Equations

• Core.Quantification.disjGQ X = List.foldr (fun (a : α) (acc : Core.Quantification.NPQ α) => Core.Quantification.individual a ⊔ acc) ⊥ X

theorem Core.Quantification.conjGQ_cons {α : Type u_1} (a : α) (X : List α) : conjGQ (a :: X) = individual a ⊓ conjGQ X

⊓(a::X) = individual(a) ⊓ ⊓(X): one step of the iterated meet.

theorem Core.Quantification.disjGQ_cons {α : Type u_1} (a : α) (X : List α) : disjGQ (a :: X) = individual a ⊔ disjGQ X

⊔(a::X) = individual(a) ⊔ ⊔(X): one step of the iterated join.

theorem Core.Quantification.conjGQ_nil {α : Type u_1} : conjGQ [] = ⊤

⊓(∅) = ⊤: empty conjunction is the tautological quantifier.

theorem Core.Quantification.disjGQ_nil {α : Type u_1} : disjGQ [] = ⊥

⊔(∅) = ⊥: empty disjunction is the contradictory quantifier.

The lattice-based definitions compute as ∀ x ∈ X, P x / ∃ x ∈ X, P x. These theorems bridge the abstract lattice structure with first-order quantification.

theorem Core.Quantification.conjGQ_iff_forall {α : Type u_1} (X : List α) (P : α → Prop) : conjGQ X P ↔ ∀ x ∈ X, P x

conjGQ computes as universal quantification: conjGQ X P ↔ ∀ x ∈ X, P x.

theorem Core.Quantification.disjGQ_iff_exists {α : Type u_1} (X : List α) (P : α → Prop) : disjGQ X P ↔ ∃ x ∈ X, P x

disjGQ computes as existential quantification: disjGQ X P ↔ ∃ x ∈ X, P x.

theorem Core.Quantification.conjGQ_singleton {α : Type u_1} (a : α) : conjGQ [a] = individual a

Singleton conjunction GQ recovers the Montagovian individual. ⊓({a}) = individual(a) ⊓ ⊤ = individual(a).

theorem Core.Quantification.disjGQ_singleton {α : Type u_1} (a : α) : disjGQ [a] = individual a

Singleton disjunction GQ recovers the Montagovian individual. ⊔({a}) = individual(a) ⊔ ⊥ = individual(a).

conjGQ X is the greatest lower bound (infimum) and disjGQ X the least upper bound (supremum) of {individual a | a ∈ X} in the NPQ lattice. These use Mathlib's ≤ on NPQ α, which is pointwise implication: f ≤ g ↔ ∀ P, f P → g P for the Pi-of-Prop ordering.

theorem Core.Quantification.conjGQ_le_individual {α : Type u_1} (a : α) (X : List α) (ha : a ∈ X) : conjGQ X ≤ individual a

conjGQ X ≤ individual a for every a ∈ X: the iterated meet is below each factor.

theorem Core.Quantification.le_conjGQ {α : Type u_1} (Q : NPQ α) (X : List α) (h : ∀ a ∈ X, Q ≤ individual a) : Q ≤ conjGQ X

conjGQ X is the greatest lower bound of {individual a | a ∈ X}: any Q below every individual in X is below conjGQ X.

theorem Core.Quantification.individual_le_disjGQ {α : Type u_1} (a : α) (X : List α) (ha : a ∈ X) : individual a ≤ disjGQ X

individual a ≤ disjGQ X for every a ∈ X: each factor is below the iterated join.

theorem Core.Quantification.disjGQ_le {α : Type u_1} (Q : NPQ α) (X : List α) (h : ∀ a ∈ X, individual a ≤ Q) : disjGQ X ≤ Q

disjGQ X is the least upper bound of {individual a | a ∈ X}: any Q above every individual in X is above disjGQ X.

theorem Core.Quantification.conjGQ_antitone {α : Type u_1} {X Y : List α} (h : ∀ x ∈ X, x ∈ Y) (P : α → Prop) : conjGQ Y P → conjGQ X P

conjGQ is antimonotone in the subset ordering: more conjuncts produce a stronger (more restrictive) quantifier.

X ⊆ Y → ⊓(Y) ≤ ⊓(X) in the NPQ lattice.

theorem Core.Quantification.disjGQ_monotone {α : Type u_1} {X Y : List α} (h : ∀ x ∈ X, x ∈ Y) (P : α → Prop) : disjGQ X P → disjGQ Y P

disjGQ is monotone: more disjuncts produce a weaker quantifier.

X ⊆ Y → ⊔(X) ≤ ⊔(Y) in the NPQ lattice.

theorem Core.Quantification.conjGQ_le_disjGQ {α : Type u_1} {X : List α} (hne : X ≠ []) (P : α → Prop) : conjGQ X P → disjGQ X P

⊓(X) ≤ ⊔(X) when X ≠ ∅: conjunction entails disjunction for non-empty subsets (pointwise form).

theorem Core.Quantification.conjGQ_le_disjGQ' {α : Type u_1} {X : List α} (hne : X ≠ []) : conjGQ X ≤ disjGQ X

⊓(X) ≤ ⊔(X) when X ≠ ∅: conjunction below disjunction in the NPQ lattice. Lattice-order form of conjGQ_le_disjGQ.

theorem Core.Quantification.individual_le_disjGQ_iff {α : Type u_1} [DecidableEq α] (a : α) (X : List α) : (∀ (P : α → Prop), individual a P → disjGQ X P) ↔ a ∈ X

Individual quantifiers are join-prime: individual(a) ≤ ⊔(X) iff a ∈ X.

This is a deep lattice-theoretic characterization: individual quantifiers are the atoms of the NPQ Boolean algebra, and they detect membership in disjunctive quantifiers. It is the formal foundation for Dayal's ANS identifying which individual satisfies the answer.

theorem Core.Quantification.conjGQ_le_individual_iff {α : Type u_1} [DecidableEq α] (a : α) (X : List α) : (∀ (P : α → Prop), conjGQ X P → individual a P) ↔ a ∈ X

Dual: ⊓(X) ≤ individual(a) iff a ∈ X.

The GQ-level De Morgan laws: negating each argument of a conjunction GQ produces a disjunction GQ and vice versa. These are the ∀/∃-level lifts of classical De Morgan:

  ¬(∀x∈X. P(x)) ↔ ∃x∈X. ¬P(x)
  ¬(∃x∈X. P(x)) ↔ ∀x∈X. ¬P(x)

Note: these are distinct from the BooleanAlgebra complement laws
on NPQ α. The lattice complement `(conjGQ X)ᶜ` negates the
*output*; De Morgan negates the *input predicate*. 

theorem Core.Quantification.deMorgan_conj {α : Type u_1} (X : List α) (P : α → Prop) : (conjGQ X fun (a : α) => ¬P a) ↔ ¬disjGQ X P

De Morgan for conjunction: negating each argument swaps ∀ to ∃.

theorem Core.Quantification.deMorgan_disj {α : Type u_1} (X : List α) (P : α → Prop) : (disjGQ X fun (a : α) => ¬P a) ↔ ¬conjGQ X P

De Morgan for disjunction: negating each argument swaps ∃ to ∀. Classical (requires excluded middle).

Conjunction and disjunction GQs decompose over list append: ⊓(X ++ Y) = ⊓(X) ⊓ ⊓(Y) and ⊔(X ++ Y) = ⊔(X) ⊔ ⊔(Y). List concatenation of entity domains corresponds to the lattice meet/join of the corresponding GQ generators.

theorem Core.Quantification.conjGQ_append {α : Type u_1} (X Y : List α) (P : α → Prop) : conjGQ (X ++ Y) P ↔ conjGQ X P ∧ conjGQ Y P

⊓(X ++ Y) ↔ ⊓(X) ⊓ ⊓(Y): conjunction GQ decomposes over append.

theorem Core.Quantification.disjGQ_append {α : Type u_1} (X Y : List α) (P : α → Prop) : disjGQ (X ++ Y) P ↔ disjGQ X P ∨ disjGQ Y P

⊔(X ++ Y) ↔ ⊔(X) ⊔ ⊔(Y): disjunction GQ decomposes over append.

def Core.Quantification.powerset {α : Type u_1} : List α → List (List α)

Power set of a list: all subsequences (order-preserving sublists).

Equations

• Core.Quantification.powerset [] = [[]]
• Core.Quantification.powerset (x_1 :: xs) = Core.Quantification.powerset xs ++ List.map (fun (x : List α) => x_1 :: x) (Core.Quantification.powerset xs)

def Core.Quantification.nonemptySubsets {α : Type u_1} (l : List α) : List (List α)

Non-empty subsets of a list.

Equations

• Core.Quantification.nonemptySubsets l = List.filter (fun (x : List α) => !x.isEmpty) (Core.Quantification.powerset l)

def Core.Quantification.conjGQs {α : Type u_1} (dom : List α) : List (NPQ α)

All conjunction GQs from non-empty subsets of a domain.

conjGQs(dom) = {⊓(X) | ∅ ≠ X ⊆ dom}

For a domain of n entities, produces 2ⁿ − 1 conjunction GQs, one per non-empty subset. Singleton subsets produce individual quantifiers; the full set produces the strongest (most conjuncts).

Equations

• Core.Quantification.conjGQs dom = List.map Core.Quantification.conjGQ (Core.Quantification.nonemptySubsets dom)

def Core.Quantification.disjGQs {α : Type u_1} (dom : List α) : List (NPQ α)

All disjunction GQs from non-empty subsets of a domain.

disjGQs(dom) = {⊔(X) | ∅ ≠ X ⊆ dom}

Equations

• Core.Quantification.disjGQs dom = List.map Core.Quantification.disjGQ (Core.Quantification.nonemptySubsets dom)