Diaconescu's theorem
In
The theorem was discovered in 1975 by Radu Diaconescu[1] and later by Goodman and Myhill.[2] Already in 1967, Errett Bishop posed the theorem as an exercise (Problem 2 on page 58 in Foundations of constructive analysis[3]).
In set theory
The theorem is a foregone conclusion over classical logic, where law of the excluded middle is assumed. The proof below is therefore given using the means of a
Fixing terminology for the proof: Call a set
The strategy of the proof is to couple a given proposition to a potential choice domain . And in the end, only a rather restrained form of full choice must be made use of. For concreteness and simplicity, the section supposes a constructive set theory with full Separation, i.e. we allow for comprehension involving any proposition . In that context, the following lemma then more sharply isolates the core insight:
- The law of excluded middle is equivalent to choice in all inhabited sets .
Once the backward-direction of this equivalence is a given, then the axiom of choice, in particular granting a choice function on all sets of this form, implies excluded middle for all propositions.
Proof of the lemma
Choice is valid in all finite sets. Given that in classical set theory the sets under consideration here are provably all finite (with exactly either the cardinalities one or two), the forward direction of the equivalence is thus established.
To prove the backward-direction one considers two subsets of any doubleton with two distinguishable members. As , a convenient choice is again . So, using Separation, let
and
Both and are inhabited, as witnessed by and . If the proposition can be proven, then both of these sets equal . In particular, by extensionality. In turn, for any
The rest of the proof concerns the pair , a set of inhabited sets. (Indeed, is itself inhabited and even validates , meaning it is finitely indexed. However, note that when not assuming excluded middle, need not be provably finite, in the bijection sense.)
A choice function on by definition has to map into the general union and fulfill
Using the definition of the two subsets and the function's established codomain, this reduces to
Using the
Discussion
As noted, implies that both defined sets equal . In that case, the pair equals the
For bivalent semantics, the above three explicit candidates are all the possible choice assignments.
One may define certain sets in terms of the proposition and, using excluded middle, in classical set theory prove that these sets constitute choice functions . Such a set represents an assignment conditioned on whether or not holds. If can be decided true or false, then such a set explicitly simplifies to one of the above three candidates.
But, in any case, neither nor 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, and , among the terms and . So it is not a function in the sense of the word that it could be explicitly evaluated into its codomain of distinguishable values.
Finitude
In a theory not assuming the disjunction or any principle implying it, it cannot even be proven that a disjunction of the set equality statements above must be the case. In fact, constructively also the two sets and are not even provably
In turn, the pairing is also elusive. It is in the surjective image of the domain , but regarding choice assignments it is not known how explicit value-assignments for both and can be made, or even how many different assignments would have to be specified. So there is generally no (set) definition such that a constructive theory would prove that joint assignment (set) to be a choice function with domain . Note that such a situation does not arise with the domain of choice functions granted by the weaker principles of
Adopting the full axiom of choice or classical logic formally implies that the cardinality of is either or , which in turn implies that it is finite. But a postulate such as this mere function existence axiom still does not resolve the question what exact cardinality this domain has, nor does it determine the cardinality of the set of that functions possible output values.
Role of separation
In summary, functions are related to equality (by the definition of unique existence used in functionality), equality is related to membership (directly through the axiom of extensionality and also through the formalization of choice in sets) and membership is related to predicates (through an axiom of separation). Using the disjunctive syllogism, the statement ends up equivalent to the extensional equality of the two sets. And the excluded middle statement for it is equivalent to the existence of some choice function on . Both goes through whenever can be used in a set separation principle.
In theories with only restricted forms of separation, the types of propositions for which excluded middle is implied by choice is also restricted. In particular, in the axiom schema of predicative separation only sentences with set bound quantifiers may be used. This restricted form of excluded middle is still not acceptable constructively. For example, when arithmetic has a model (when, relevantly, the infinite collection of natural numbers form a set one may quantify over), then set-bounded but undecidable propositions can be expressed.
Other frameworks
In
In topoi
In Diaconescu's original paper, the theorem is presented in terms of topos models of constructive set theory.