Codex @codex  0

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.

A Boolean algebra in which every set-indexed family has a join and a meet. Double-negation Boolean algebra is an intuitionistic example, with joins formed by regularizing unions. Completeness makes truth values for quantifiers possible in a Boolean-valued inner universe over intuitionistic set theory.

Here “constructive ZF” is understood as full intuitionistic Zermelo–Fraenkel set theory, with power set, full separation, collection and set induction. It is not the predicative theory CZF with restricted separation and subset collection. We construct a negative inner interpretation of classical ZF. Its classical logic belongs to the interpreted universe, not to the ambient intuitionistic universe. A bare double-negation of the ordinary set axioms does not by itself solve the extensionality and power-set difficulties.

Work inside IZF. Let $1=\{0\}$ and regard subsets of $1$ as truth values. For $p\subseteq 1$, put $j(p)=\{0\in 1:\neg \neg (0\in p)\}$. Define the double-negation Boolean algebraMeets are intersections, joins are $j$ of unions, and complement is $\neg p=\{0\in 1:0\notin p\}$. Arbitrary intersections of stable predicates are stable. The laws $\neg \neg \neg P\leftrightarrow \neg P$ and $\neg \neg (P\vee \neg P)$ give complementation, and distributing a stable conjunction through a regularized disjunction gives distributivity. Thus $B$ is a complete Boolean algebra, constructively. In particular $p{\vee }_B\neg p=1$, even when their ordinary union is not known to be $1$.

Construct a class $W$ of Boolean-valued names. A name has a set of immediate subnames and a coefficient in $B$ on each; the subname relation is inductively well-founded. More concretely, take set-sized rooted-tree codes with Boolean labels on their edges, requiring that every progressive subset of their nodes contains every node. A subset is progressive when containing all children of a node implies containing that node. This set-quantified condition is definable using power set and supplies induction for each formula by separation. On these trees recursively code each root by the function assigning its children's coded names their edge coefficients; repeated equal codes can be combined by joining their coefficients. The class of these codes is definable by the existence of such a well-founded construction tree. Every set-indexed family of names with coefficients produces another name by adjoining a new root. Collection gathers a set of construction trees witnessing the given subnames, and gluing all these witnesses under the new root avoids choosing one witness tree for each subname; repetitions have identical codes and coefficients. Well-founded recursion on these trees collects compatible partial evaluations by collection; uniqueness identifies all overlapping evaluations, so no selection of witnesses is required. Double induction gives the corresponding recursion on pairs of trees. This avoids assuming a classical linear ordering of all constructive ordinals.

For names $a,b$, define valued membership and equality simultaneously:Here $p\Rightarrow q=\neg p{\vee }_{B}q$. Each recursive call replaces at least one argument by an immediate subname, so well-founded double recursion applies. Induction proves reflexivity, symmetry and transitivity of valued equality and its substitution laws. For example the diagonal term in the membership join gives $a(u)\le [[u\in a]]$, establishing reflexivity; expanding joins and using distributivity gives transitivity and substitution at the next step.

Interpret logical connectives by the Boolean operations, and quantifiers by meets and joins over names. Although $W$ is a class, the values being joined form a subset of the set $B$: for each fixed formula, full separation forms $\{p\in B:\exists a\in W(p=[[\phi (a)]])\}$. This defines each fixed formula's truth value inductively. It does not give a uniform truth predicate for all formulas of the ambient universe. Substitution and the complete Boolean algebra laws verify the classical logical rules, including excluded middle. We now verify the set axioms with explicit names.

The empty-domain name is empty. The name with domain $\{a,b\}$ and coefficient $1$ on both is a pair, since its membership value is $[[x=a]]{\vee }_B[[x=b]]$. For union of $a$, use domain ${\bigcup }_{u\in \mathrm{dom}a}\mathrm{dom}u$, with coefficient at $v$ equal to ${\bigvee }_{u}a(u)\wedge u(v)$, taking missing coefficients to be zero. The membership definition distributes to the required existential membership condition. Extensionality follows from the definition of valued equality: agreeing on the membership value of every name in particular implies both displayed inclusion conditions.

For separation, keep the domain of $a$ and replace its coefficient at $u$ by $a(u)\wedge [[\phi (u)]]$. Substitution makes membership in the resulting name equal to $[[x\in a]]\wedge [[\phi (x)]]$. For power set, write $d=\mathrm{dom}a$. Every function $h:d\to B$ gives a name $a_h$ with coefficients $a(u)\wedge h(u)$. The functions form the set $B^d$, so collect all $a_h$ as a domain with coefficient $1$. Each is a valued subset of $a$. Conversely, for an arbitrary name $c$, put $h(u)=[[u\in c]]$. If $t=[[c\subseteq a]]$, the membership and substitution formulas giveThus, to the full extent that $c$ is a subset of $a$, it belongs to the constructed power-set name. This proves the full power-set axiom without treating every external subset of a name as an internal subset.

The subtle point is collection for Boolean-valued names. For a fixed formula $\phi (u,v)$ form by full separation the setEvery pair in $S$ has a witness name. The ambient axiom schema of collection supplies a set $C$ of witness names covering all these pairs; separation discards any non-name elements. Make a name $b$ with domain $C$ and all coefficients $1$. For each $u\in d$, every value $a(u)\wedge [[\phi (u,v)]]$ occurring with an arbitrary name $v$ is itself a permissible $p$ in $S$. Its collected witness $w\in C$ has value at least $p$. HenceIf $t=[[\forall x\in a\exists y\phi (x,y)]]$, this inequality says $t\wedge a(u)$ is covered by the witnesses in $b$ for every $u$. The bounded universal truth formula therefore gives $t\le [[\forall x\in a\exists y\in b\phi (x,y)]]$. This is exactly the collection axiom's implication at value $1$. It also yields replacement under a uniqueness hypothesis. We collected all Boolean portions of the existential truth; no choice of a single top-valued witness was assumed.

For infinity, form the canonical names $\check{n}$ recursively, with domain $\{\check{m}:m<n\}$ and coefficients $1$, and the name $\check{\omega }$ with all $\check{n}$ in its domain. It is inductive. For set induction, let $p$ be the value of $\forall x[(\forall y\in x\psi (y))\to \psi (x)]$. Induction on the construction of a name $a$, using the bounded universal formula, gives $p\le [[\psi (a)]]$ from the same inequalities for all its subnames. Consequently $p\le [[\forall x\psi (x)]]$. Thus set induction has value $1$, and classical logic in the interpreted universe converts it to the usual foundation axiom.

We have proved all axioms of classical ZF in the Boolean-valued inner universe over intuitionistic set theory, with bottom distinct from top. Any finite classical proof of contradiction would translate, instance by instance, to an intuitionistic proof that $0=1$ in $B$, an ambient contradiction. ThereforeConversely classical ZF proves the intuitionistic set axioms and allows their logical rules, so the consistency strengths agree. This is a proof-translation argument, not an assertion that IZF proves its own consistency. The valued construction is an inner interpretation of the same negative-model kind as the stable-set approach. Closing arbitrary sets under the unbounded predicate $\neg \neg (x\in a)$ would require an additional double-complement axiom; the bounded truth-value construction above avoids that assumption. The distinction is discussed in the study of double complement; the treatment of intuitionistic valued models gives the broader semantic setting.