Double-negation Boolean algebra (source code)

= Double-negation Boolean algebra
{title2=$B=\{p\in\mathcal P(1):\neg\neg p=p\}$}

Inside <IZF>, truth values are subsets of a singleton. Their double-negation-stable elements form a complete Boolean algebra: arbitrary meets are intersections and arbitrary joins are double-negation closures of unions. Negation gives Boolean complement. The join of $p$ and its complement is top although their ordinary union need not be top. The closure here is taken inside the fixed singleton; it does not assume that the class of all objects double-negatively belonging to an arbitrary set is itself a set.