Diaconescu's theorem

The proof given here is in the context of a constructive set theory with an axiom of specification that allows for comprehension involving some proposition ${\displaystyle P}$. One considers two subsets of a set with two distinguishable members, such as ${\displaystyle \{0,1\}}$ with ${\displaystyle 0\neq 1}$:

${\displaystyle U=\{x\in \{0,1\}\mid (x=0)\vee P\}}$

and

${\displaystyle V=\{x\in \{0,1\}\mid (x=1)\lor P\}.}$

If ${\displaystyle P}$ can be proven, then both of these sets equal ${\displaystyle \{0,1\}}$. In particular, by the axiom of extensionality, ${\displaystyle P\,\to \,U=V}$. In turn, for any mathematical function ${\displaystyle g}$ that can take both of these sets as an argument, one finds ${\displaystyle P\,\to \,g(U)=g(V)}$, the contrapositive of which is ${\displaystyle g(U)\neq g(V)\,\to \,\neg P}$.

Both sets are inhabited, as witnessed by ${\displaystyle 0\in U}$ and ${\displaystyle 1\in V}$. So assuming the axiom of choice, there exists a choice function ${\displaystyle f}$ for the set ${\displaystyle \{U,V\}}$ into their union ${\displaystyle \{0,1\}}$. By definition of the axiom, it fulfills

${\displaystyle f(U)\in U\,\land \,f(V)\in V.}$

Using the definition of the two subsets and having already established the codomain, this reduces to

${\displaystyle {\big (}f(U)=0\lor P{\big )}\land {\big (}f(V)=1\lor P{\big )}.}$

Using the law of distributivity, this implies ${\displaystyle P\,\lor \,f(U)\neq f(V)}$. By the previous comment on functions, this in turn implies ${\displaystyle P\lor \neg P}$.

As noted, ${\displaystyle P}$ implies that both defined sets equal ${\displaystyle \{0,1\}}$. In that case, the pair ${\displaystyle \{U,V\}}$ equals the singleton set ${\displaystyle \{\{0,1\}\}}$ and there are two possible choice functions on that domain, picking either ${\displaystyle 0}$ or ${\displaystyle 1}$. If, instead, ${\displaystyle P}$ can be rejected, i.e. if ${\displaystyle \neg P}$ can be proven, then ${\displaystyle U=\{0\}}$ and ${\displaystyle V=\{1\}}$. So in that case ${\displaystyle U\neq V}$, and on the proper pair ${\displaystyle \{\{0\},\{1\}\}}$ there is only one possible choice function, picking the unique inhabitant of each singleton set. This last assignment "${\displaystyle U\mapsto 0}$ and ${\displaystyle V\mapsto 1}$" is not viable if ${\displaystyle P}$ holds, as then the two inputs are actually the same. Similarly, the former two assignments are not viable if ${\displaystyle \neg P}$ holds, as then the two inputs share no common member. What can be said is that if a choice function exists at all, then there exists a choice function choosing ${\displaystyle 0}$ from ${\displaystyle U}$, and one (possibly the same function) choosing ${\displaystyle 1}$ from ${\displaystyle V}$.

For bivalent semantics, the above three explicit candidates are all the possible choice assignments.

In classical set theory, one may define certain sets in terms of the proposition ${\displaystyle P}$ and, using excluded middle, prove these constitute choice functions ${\displaystyle f\colon \{U,V\}\to \{0,1\}}$. Such a set represents an assignment conditioned on whether or not ${\displaystyle P}$ holds. If ${\displaystyle P}$ can be decided true or false, then the classical set simplifies to one of the above three explicit candidates.

But, in any case, neither ${\displaystyle P}$ nor ${\displaystyle \neg P}$ can necessarily be established. Indeed, they may even be independent of the theory at hand. Since the former two explicit candidates are each incompatible with the third, it is generally not possible to identify both of the choice function's return values, ${\displaystyle f(U)}$ and ${\displaystyle f(V)}$, among the terms ${\displaystyle 0}$ and ${\displaystyle 1}$. So it is not a function in the sense of the word that it could be explicitly evaluated into its codomain of distinguishable values.