Mathematics cannot learn new things and cannot forget old things. This is so different from the way that we experience the world that we can misunderstand how mathematics works. Mathematicians may make conjectures, but mathematics itself contains no conjectures, only theorems (and antitheorems, and logically independent statements). I believe that mathematicians have know about this for a long time. I was surprised to discover how this works beyond logic. While we might like to model problems with given sets, mathematics cannot forget how the set was constructed (or how it is used). Mathematics need not have such a thing as an unordered set. I am sure that you have been told that sets are unordered, but how is that? Which set theoretic axiom defines sets as being unordered? Which rule of inference defines sets to be unordered? Is such a rule even possible? Where could the disorder come from? Unorderedness cannot be a mathematical concept. If there cannot be an axiom based on unorderedness, we can consider axioms that deal with orders. The well ordering axiom comes to mind (along with its twins the axiom of choice and Zorn's lemma). The implication of AoC for orders is only that the set in question 'could' be unordered because you might want a different order. AoC makes proofs easier because it chooses an order with the desired properties, like a variable. An axiom that fixes the order that a set may have would imply that the set 'might' not be unordered. I have found it tricky to formulate an axiom like that. I think that the axiom of determinacy works this way. Wouldn't AD (or any such axiom) make proofs more difficult? Why would we want it? The short answer is that we may need to use AD to advance our understanding of mathematics. The broad acceptance of AoC (not to mention the existence of unordered sets) has influenced how math has developed and the questions that we have asked. There may be assumptions that we have not noticed built into those questions. A number of important open problems are in an effort to do something mathematically convenient. To my knowledge, the way to measure mathematical effort is computational complexity. It may be possible to extend (and formalize) the Turing thesis from functions of strings to functions of ordered sets. The combination of AD and the Turing thesis may lead to new insights. To put this perspective on the AoC, judge me on one thing. Do you agree that the axiom of choice is used as a proof strategy rather than as an axiom? Mathematicians may be reluctant to admit it, but I don't think that they really want to develop restatements of AoC (like Zorn's lemma). AoC allows mathematicians to put off the tedious details of the ordering of some set, but they want a proof in ZF eventually. That may make using AD + Turing thesis less imposing, since you can think of them as clauses that you add to a conjecture. Such a modification can't change the problem in terms of ZF, so if you struggling to find a proof why not try it. Now how about variables? ...