dedekind::category::IsBooleanAlgebra Concept Reference

The top of the Boolean-algebra variety Alg(∨,∧,¬,⊥,⊤): a complemented distributive bounded lattice — the ∨/∧/¬ analogue of IsField topping the (signature-expanded) ring variety. More...

Concept definition

template<typename T, typename Join std::bit_or<>, typename Meet std::bit_and<>, typename Not std::bit_not<>>
concept dedekind::category::IsBooleanAlgebra = 
    IsBoundedLattice<T, Join, Meet> && IsDistributiveLattice<T, Join, Meet> &&
    IsClosedUnderUnary<T, Not> && is_complemented_v<T, Join, Meet, Not>

Detailed Description

The top of the Boolean-algebra variety Alg(∨,∧,¬,⊥,⊤): a complemented distributive bounded lattice — the ∨/∧/¬ analogue of IsField topping the (signature-expanded) ring variety.

\((T, \vee, \wedge, \neg, \bot, \top)\) with distributivity and complements. bool under (logical_or, logical_and, logical_not) is the initial Boolean algebra \(\mathbb{B} = \{\bot < \top\}\). This is the variety reading (operation-parametric, Birkhoff), distinct from the relation-based category::IsBooleanLatticeCategory in :lattice.

Note

This is not the top of the pure two-operation variety Alg(∧,∨) (which tops at IsDistributiveLattice). Complement ¬ and the bounds ⊥/⊤ expand the signature to Alg(∨,∧,¬,⊥,⊤); the pure (∧,∨) reducts of Boolean algebras are not even HSP-closed — a 3-element chain is a (∧,∨)-sublattice of the 4-element Boolean algebra yet has no complement.

Not is required to be a genuine unary operation T → T (IsClosedUnderUnary), not merely a trait key: the is_complemented_v certificate alone would let a non-callable Not satisfy the concept, so a consumer could not actually apply the advertised complement. The closure clause makes ¬a well-formed before the semantic law is trusted.