Double-negation Boolean algebra
ID: double-negation-boolean-algebra
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 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.
New to topics? Read the docs here!