The conservative determiners as a Boolean algebra

Keenan and Stavi show that conservative generalized quantifiers are closed under the pointwise Boolean operations, so they form a Boolean subalgebra conservativeSubalgebra of GQ α, whose elements ConsGQ α carry mathlib's Boolean algebra structure. They are moreover closed under arbitrary pointwise meets and joins, so the algebra is complete, and it is atomic because GQ α is a power of Prop: ConsGQ α is a CompleteAtomicBooleanAlgebra, the structure Keenan and Stavi's Appendix establishes on the way to the Conservativity Theorem. The atoms themselves and the counting consequences are in Studies/KeenanStavi1986.lean. Elliott identifies this algebra with the predicates of polarized groups.

Implementation notes

The Boolean algebra on GQ α is mathlib's Pi instance (Prop is a Boolean algebra and (α → Prop) → (α → Prop) → Prop lifts pointwise); closure under ⊔ and ⊓ is Conservative.sup and Conservative.inf, and the complement of a conservative quantifier is conservative because conservativity is an equivalence at every restrictor and scope. The complete structure extends the BooleanSubalgebra coercion instance rather than being pulled back along Subtype.val, so the finitary operations stay the coercion instances and no second BooleanAlgebra path is introduced.

References

• [KS86]
• [Ell25]

Infinitary closure

theorem Quantifier.GQ.Conservative.iSup {α : Type u_1} {ι : Sort u_2} {f : ι → GQ α} (hf : ∀ (i : ι), (f i).Conservative) : (⨆ (i : ι), f i).Conservative

An indexed join of conservative quantifiers is conservative.

theorem Quantifier.GQ.Conservative.iInf {α : Type u_1} {ι : Sort u_2} {f : ι → GQ α} (hf : ∀ (i : ι), (f i).Conservative) : (⨅ (i : ι), f i).Conservative

An indexed meet of conservative quantifiers is conservative.

The Boolean subalgebra

def Quantifier.GQ.conservativeSubalgebra {α : Type u_1} : BooleanSubalgebra (GQ α)

The conservative GQs, a Boolean subalgebra of GQ α.

Equations

• Quantifier.GQ.conservativeSubalgebra = { carrier := {q : Quantifier.GQ α | q.Conservative}, supClosed' := ⋯, infClosed' := ⋯, compl_mem' := ⋯, bot_mem' := ⋯ }

@[simp]

theorem Quantifier.GQ.mem_conservativeSubalgebra {α : Type u_1} {q : GQ α} : q ∈ conservativeSubalgebra ↔ q.Conservative

@[reducible, inline]

abbrev Quantifier.GQ.ConsGQ (α : Type u_2) : BooleanSubalgebra (GQ α)

The conservative GQs form the subtype of GQ α satisfying conservativity, a Boolean algebra under the pointwise propositional operations with pointwise implication as the order.

Equations

• Quantifier.GQ.ConsGQ α = Quantifier.GQ.conservativeSubalgebra

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

The complete atomic structure

The Appendix of [KS86] observes that GQ α is a complete atomic Boolean algebra under the pointwise operations and that the conservative functions are a complete subalgebra, hence themselves a complete atomic Boolean algebra. The instance extends the finitary coercion instance with pointwise set suprema and infima.

@[instance_reducible]

noncomputable instance Quantifier.GQ.ConsGQ.instSupSetSubtypeMemBooleanSubalgebra {α : Type u_2} : SupSet ↥(ConsGQ α)

Equations

• Quantifier.GQ.ConsGQ.instSupSetSubtypeMemBooleanSubalgebra = { sSup := fun (S : Set ↥(Quantifier.GQ.ConsGQ α)) => ⟨⨆ q ∈ S, ↑q, ⋯⟩ }

@[instance_reducible]

noncomputable instance Quantifier.GQ.ConsGQ.instInfSetSubtypeMemBooleanSubalgebra {α : Type u_2} : InfSet ↥(ConsGQ α)

Equations

• Quantifier.GQ.ConsGQ.instInfSetSubtypeMemBooleanSubalgebra = { sInf := fun (S : Set ↥(Quantifier.GQ.ConsGQ α)) => ⟨⨅ q ∈ S, ↑q, ⋯⟩ }

@[simp]

theorem Quantifier.GQ.ConsGQ.sSup_val {α : Type u_2} (S : Set ↥(ConsGQ α)) : ↑(sSup S) = ⨆ q ∈ S, ↑q

@[simp]

theorem Quantifier.GQ.ConsGQ.sInf_val {α : Type u_2} (S : Set ↥(ConsGQ α)) : ↑(sInf S) = ⨅ q ∈ S, ↑q

@[simp]

theorem Quantifier.GQ.ConsGQ.iSup_val {α : Type u_2} {ι : Sort u_3} (f : ι → ↥(ConsGQ α)) : ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

@[simp]

theorem Quantifier.GQ.ConsGQ.iInf_val {α : Type u_2} {ι : Sort u_3} (f : ι → ↥(ConsGQ α)) : ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

@[instance_reducible]

noncomputable instance Quantifier.GQ.ConsGQ.instCompleteAtomicBooleanAlgebraSubtypeMemBooleanSubalgebra {α : Type u_2} : CompleteAtomicBooleanAlgebra ↥(ConsGQ α)

Equations

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