Decidability of the Axiom of Choice Everything that I read regarding Set Theory states that the Axiom of Choice is independent and undecidable within the context of Zermelo-Frankel Set Theory. My question is this: Is there any consistent form of Set Theory stronger than ZF in which the Axiom of Choice IS decidable?
Thanks guys...First time on here =)
---Dan
 A: Assuming the consistency of ZF, the two minimal such theories are ZFC (= ZF + AC) and ZF + ¬AC. However, there are plenty of stronger statements that imply the Axiom of Choice over ZF, such as the Axiom of Constructibility (aka V = L) and V = HOD (every set is ordinal definable). There are also statements that refute the Axiom of Choice over ZF such as the Axiom of Determinacy and various "regularity axioms" such as "every subset of [0,1] is Lebesgue measurable" or "every uncountable subset of [0,1] contains a perfect set."
A: One should be carefull with the word "consistent".
One of the fundamental results in axiomatic set theory is the incompleteness theorem of Gödel that states that any consistent (set) theory that is strong enough to do some specific arithmetic things (and every reasonable set theory should be strong enough to do that) cannot prove its own consistency. In particular: A consistent set theory that is stronger than ZF (in the sense that it implies ZF) cannot proven to be consistent with means of ZF. If it could, ZF would prove its own consistency and would therefore be inconsistent by Gödels theorem. As a result the stronger theory would be inconsistent as well.
Because ZFC "is" consistent (I do believe it is as do propably most other mathematicians who know about Gödel), this means that (absolut) consistency is not a good requirement because we will never know it for sure. ("know" in the sense that someone has a ZF(C)-proof of it)
A better requirement would be that the theory your looking for is relative consistent with ZF(C), i.e. if we assume that ZF(C) is consistent, then the other theory is consistent as well. Example: ZFC is relative consistent to ZF.
There are plenty of theories that are stronger than ZF, relative consitent to ZF and imply the axiom of choice, for example ZF+GCH. A result of Sierpinksi shows that ZF+GCH implies the axiom of choice. Another perhaps more popular example is ZF+(V=L). V=L implies not only the AC but the axiom of global choice, i.e. there is a well-ordering of the whole universe.
A: There are, of course, exactly two ways for a theory to decide AC. Either it proves that AC is true, or it proves that AC is false. 
Consequently, if you have a theory extending ZF and deciding AC, then either your theory includes ZFC or it includes ZF+¬AC.  Thus, there are two minimal possibilities which meet your requirement, and any theory extending ZF and deciding AC must extend one of them.
The results of Godel on the constructible universe show that if ZF is consistent, then so is ZF+AC. And the results of Cohen on the forcing method show that if ZF is consistent, then so is ZF+¬AC.  So both of these minimal theories are consistent, if ZF itself is consistent. 
There are, of course, a huge variety of further extensions of ZFC that are intensely studied in set theory, and you can learn about them in any introductory graduate level set theory text. For example, one will want to know whether V=L, or whether CH holds, or GCH, or Diamond, whether there are Suslin trees or not, or large cardinals, and so on. Similarly, there are also a large variety of further extensions of ZF+¬AC that are studied, some quite intensely. For example, one might want to have the countable AC, or DC, or the Axiom of Determinacy and so on.
A: NF is inconsistent with choice:
http://www.pnas.org/content/39/9/972.full.pdf+html
But there aren't even any relative consistency proofs.  Interestingly, NF+urelements proves choice and is consistent if Peano Arithmetic is.  More about NF here:
http://plato.stanford.edu/entries/quine-nf/
A: There is an interesting question here: "Are there any set theories in which the question of choice is decided without inserting an axiom tailored to the purpose?"
As Jeremy points out, NF is inconsistent with choice. It's strongly implied in Holmes (PDF), though not stated outright, that the Axiom of Choice is independent of the other axioms of NFU, though it does state outright on p.95 that the problem of proving there are atoms without choice is open: specifically, if it's adopted, Specker's inconsistency proof becomes a proof that there are atoms.
Many set-class theories, in particular NBG and MK, have the axiom of limitation of size, which effectively says that every proper class is the same size. This implies a well-ordering of the class of all sets, and therefore global choice. There is a (very short) Wikipedia article on this axiom.
