# Axiom of Choice in a weaker system

Is it known whether or not there is a consistent system of logic where two or all of the axiom of choice, well-ordering principle, and Zorn's lemma have no (known) proof of equivalence?

I was thinking about the old adage "The Axiom of Choice is clearly true, the well-ordering principle is clearly false, and nobody really knows about Zorn's lemma" and the content of Proof that pi is transcendental that doesn't use the infinitude of primes, particularly François G. Dorais' beautiful answer, where he explains the existence of systems where it isn't known whether infinite primes is necessary for the transcendence of $\pi$, and it occurred to my rather logic-ignorant self that perhaps a sufficiently weak system might allow for this adage to be true, at least in the form $X$ is (clearly or otherwise) true and $Y$ is (again, clearly or otherwise) false for suitable $X$ and $Y$ from the above list. I think it would be particularly poetic to find one in which $X$ is the Axiom of Choice and $Y$ is the well-ordering principle.

-

A small quibble: I would view these principles as primarily set-theoretic principles, not logical principles per se. It's actually a little bit tricky, because even if we choose to weaken the metalogic (that is, the logical principles we allow ourselves to apply to a set theory, from the outside as it were), one can also speak of the internal logic of a category of sets, which can be stronger than the metalogic. This fact is definitely relevant to the question here.

More exactly, even if the external logic applied to ZF is intuitionistic first-order logic, assuming the axiom of choice will force the law of excluded middle to hold internally. What does this mean, exactly? It means that for every subset $A \subseteq X$, we can, with the help of the axiom of choice, construct a complement, i.e., a subset $B \subseteq X$ such that $A \cap B = \emptyset$ and $A \cup B = X$, so that the lattice of subobjects of a set is a Boolean algebra. This result is due to Diaconescu, who was an early pioneer in topos theory. See the nLab article on excluded middle for a discussion.

I bring this up because proofs of the the three-way equivalence between AC, Zorn, and well-ordering use excluded middle, but if we assume AC, this is no obstacle to being able to prove Zorn's lemma. But not the other way around. I believe the situation is this:

• The proof of "well-ordering" implies "axiom of choice" is perfectly constructive. If we formulate AC as saying that every surjection $p: A \to B$ has a section $s$, then we can construct a section if $A$ is well-ordered: for each fiber $b \in B$, define $s(b)$ to be the least element of $p^{-1}(b)$.

• Under intuitionistic logic, the axiom of choice implies internal excluded middle, and the usual proof that AC implies Zorn will then carry over.

• Under intuitionistic logic, Zorn's lemma plus internal excluded middle can be used to construct a well-ordering on any set $X$. (The usual proof carries over: if a maximal well-orderable subset is not the whole set, we could extend the well-ordering in contradiction to maximality.) It follows from the previous bullet point that AC proves the well-ordering principle in intuitionistic logic. But (I believe -- I should check this carefully): under intuitionistic logic, Zorn's lemma by itself does not prove the (internal) law of excluded middle, and does not imply the well-ordering principle, hence cannot imply AC either.

There is some material on this in the nLab. There may be other answers to this question which devolve on what one takes the underlying set theory to be, but the vanilla approach taken here, which I guess is in line with the question, is to take ZF but weaken the metalogic to get some form of IZF (although what I really had in mind was just to use topos theory as the baseline "set theory").

-
Proposition D4.5.14 of the Elephant shows that Zorn's Lemma holds internally in any localic Set-topos. So there are plenty of non-Boolean toposes that satisfy Zorn's Lemma. – François G. Dorais Jan 29 '11 at 16:24
Excellent -- thanks for bringing this to my attention, Francois! – Todd Trimble Jan 29 '11 at 18:31
This is a good answer, but I think it's also worth noting that in intuitionistic logic, the usual definition of "well-ordering" (every inhabited set has a least element) is arguably kind of stupid. It's pretty hard to do much with it without using proof by contradiction (find a least counterexample, etc.). More useful is the notion of well-founded relation: nlab.mathforge.org/nlab/show/well-founded+relation , and you can have lots of well-founded relations in intuitionistic logic without implying any choice. – Mike Shulman Mar 15 '11 at 21:53