Diaconescu's theorem

In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle or restricted forms of it.

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]).

Proof

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 . One considers two subsets of a set with two distinguishable members, such as with :

and

If can be proven, then both of these sets equal . In particular, by the axiom of extensionality, . In turn, for any mathematical function that can take both of these sets as an argument, one finds , the contrapositive of which is .

Both sets are inhabited, as witnessed by and . So assuming the axiom of choice, there exists a choice function for the set into their union . By definition of the axiom, it fulfills

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

Using the law of distributivity, this implies . By the previous comment on functions, this in turn implies .

Discussion

As noted, implies that both defined sets equal . In that case, the pair equals the singleton set and there are two possible choice functions on that domain, picking either or . If, instead, can be rejected, i.e. if can be proven, then and . So in that case , and on the proper pair there is only one possible choice function, picking the unique inhabitant of each singleton set. This last assignment " and " is not viable if holds, as then the two inputs are actually the same. Similarly, the former two assignments are not viable if 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 from , and one (possibly the same function) choosing from .

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 and, using excluded middle, prove these constitute choice functions . Such a set represents an assignment conditioned on whether or not holds. If can be decided true or false, then the classical set simplifies to one of the above three explicit 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 the two sets and are not even provably finite, in the usual sense of there existing a bijection with a natural number. (However, any finite ordinal injects into any Dedekind-infinite set and so a subset of a finite ordinal does validate the logically negative notion of Dedekind-finiteness. This is the case for both and , into which cannot be injected. As an aside, it is consistent also with classical that there exist sets which are neither Dedekind-infinite nor finite.)

In turn, the pairing is also elusive. It is in the surjective image of the domain , but 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 countable and dependent choice, since in these cases the domain is always just , the trivially countable first infinite cardinal.

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 functionality), equality is related to membership (through the axiom of extensionality and in the notion 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 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 constructive type theory, or in Heyting arithmetic extended with finite types, there is typically no separation principle at all - subsets of a type are given different treatments. A form of the axiom of choice is a theorem, yet excluded middle is not.

Topoi

In Diaconescu's original paper, the theorem is presented in terms of topos models of constructive set theroy.

Notes

  1. Diaconescu, Radu (1975). "Axiom of choice and complementation". Proceedings of the American Mathematical Society. 51 (1): 176–178. doi:10.1090/S0002-9939-1975-0373893-X. MR 0373893.
  2. Goodman, N. D.; Myhill, J. (1978). "Choice Implies Excluded Middle". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 24: 461. doi:10.1002/malq.19780242514.
  3. E. Bishop, Foundations of constructive analysis, McGraw-Hill (1967)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.