= Boolean-valued inner universe over intuitionistic set theory
{title2=$V^B$}
Using the <double-negation Boolean algebra>, form well-founded names whose immediate subnames have truth-value weights. Define valued membership and equality by recursion on the underlying well-founded trees. Logical conjunction and universal quantification use meets; disjunction and existence use Boolean joins. Explicit names for pairs, unions and subsets verify the elementary set axioms, and <collection for Boolean-valued names> handles unbounded witnesses. The resulting internal valued universe validates classical <ZF>. This is a negative inner interpretation, not an assertion that the external intuitionistic universe satisfies excluded middle.
Back to article page
