Does the Axiom of Choice (or any other "optional" set theory axiom) have real-world consequences? Or another way to put it: Could the axiom of choice, or any other set-theoretic axiom/formulation which we normally think of as undecidable, be somehow empirically testable? If you have a particular scheme for testing it, that's great, but even the existence or non-existence of a proof regarding potential testability is wonderful.
How about something a little simpler: can we even test the Peano axioms? Are there experiments that can empirically verify theorems not provable by them?
This is a slightly fuzzy question, so to clarify what I mean, consider this: the parallel postulate produces good, useful geometry, yet beyond its inapplicability to the sphere, there's evidence to suggest that the universe is actually hyperbolic - this can be considered an experimental evidence "against" the parallel postulate in our universe.
Edit: Thanks to all the people who answered - I understand the concerns of those who don't like this questions, and I appreciate all those who answered a more modest interpretation that I should, in retrospect, have stated. That is, "Is the axiom of choice agreeable with testable theories of mathematical physics, is it completely and forever irrelevant, or is it conceivably relevant but in a way not yet known," to which I got several compelling answers indicating the former.
 A: I think this question is the wrong way around (but this is also a philosophical issue).
The question is not if a theory has real world consequences but if the theory fits the parts of reality that is in the focus of the researcher.
Mathematics is about deducing lemmas and theorems from axioms  so there are no consequences for the real world. All the lemmas and theorems are already there when you choose the axioms (sometimes you don't find them within some hundred years - this is also about computability). The question is if these theorems describe the real world and give correct forecasts when you insert real world variables into them.
If you choose too few axioms you won't get a very rich theory, if you choose too many you will get something with which you could prove anything and its counterpart. So it is really a tightrope walk to find the "right" axioms - also trial and error over the centuries.
After that you model reality with your lemmas/theorems and fit it to reality. If it works - fine, if not, try something else. I think it all boils down to that.
A: 
This is a slightly fuzzy question, so to clarify what I mean, consider this: the parallel postulate produces good, useful geometry, yet beyond its inapplicability to the sphere, there's evidence to suggest that the universe is actually hyperbolic - this can be considered an experimental evidence "against" the parallel postulate in our universe.

But that doesn't mean the same thing as your question is asking.  The generalization of Euclidean geometry is not just hyperbolic or spherical geometry, but differential geometry.  And a lot of the power of general relativity (or any Yang-Mills theory) comes from its general differential geometric structure (in other words, that it's a principal bundle with certain gauge group, etc), not the specific "geometry."  This is analogous to thinking of differential equations v.s. initial conditions and specific solutions.
From the point of view of theoretical physicists, in a sense the answer is the same.  If it is sensible to have math with and without the axiom of choice, one could reasonably expect that there are physical situations that can be described with and without the axiom of choice.
In other words, it may not be reasonable to say that AC is "empirically testable," as some systems may be described by "X+AC" and some others may be described by "X".  Analogously, some systems are hyperbolic, e.g., special relativity's geometry, and others are not, e.g., generic Yang-Mills, string theory, etc--this does not mean that "geometry" is testable, it simply means that specific systems have specific descriptions.  Not that any one formulation is in any way "better" than others from an experimental standpoint.  
So I do not believe it makes sense to ask if the "universe" satisfies AC (or any other property) in this way.
A: Unfortunately, I can't remember either the details or an appropriate reference, but I once read of an amusing proposal made by a physicist to exploit ideas in relativity, which, if the geometry of the universe was as it might possibly be, would allow you to do infinitely many computational steps in finite time (though presumably it wasn't finite time from the point of view of the computer). If it worked, then one could test number theoretic statements by simply running through all the integers. (This is in non-serious answer to your question about the Peano axioms.)
Well, I wrote that, but I now see that there's a problem because the input size would tend to infinity, so the computer would need infinite memory as well. I imagine the physicist concerned had thought about that but can't remember enough to be sure. 
A: Asking whether a mathematical axiom can be empirically tested makes little or no sense, as it would be asking the same about the rules of chess. Excuse me for trivializing a little. If we use natural numbers with Peano's axioms to count grains of rice, we may be satisfied, for they give a quite satisfying model. One could also object that after all there are finitely many grains of rice in the world, though. But this say nothing about the consistency of Peano axioms; it only shows the range of applicability of a certain physical interpretation of them.  
A: Stan Wagon mentions the following paper in his book: B. W. Augenstein, Hadron physics and transfinite set theory, International Journal of Theoretical Physics, 23(1984), 1572-9575.  
Peter Komjath
A: I vaguely recall some (humorous?) exchange about whether it is possible that a bridge would fall down because the calculations in its design had used the Lebesgue integral instead of the Riemann integral...  Does anyone know where this was?
A: I'm not sure how to add comments to other responses (maybe I don't have enough reputation, or maybe I'm just inept). I think the paper that gowers is referring to is on Malament-Hogarth spacetime. 
http://en.wikipedia.org/wiki/Malament%E2%80%93Hogarth_spacetime
A: The following paper "On Non-measurable sets and Invariant Tori' uses the axiom choice to solve a problem in classical mechanics and discusses the application of the axiom of choice to physics.
A: The 1996 paper The Axiom of Choice in Quantum Theory by Brunner, Svozil
and Baaz contains the following provocative statement in the first paragraph: 
"Hence the very notion of a self-adjoint operator as an observable of quantum
theory may become meaningless without the axiom of choice." The authors arrive 
at this conclusion by "constructing peculiar Hilbert spaces from counterexamples 
to the axiom of choice."
A: Before answering your question about the axiom of choice, let me take another set-theoretic axiom: "There exists an inaccessible cardinal."  This axiom implies that ZFC is consistent.  One could argue that this has the following "real-world consequence": If you set a computer running to look for a contradiction in ZFC, it will never find one.  More generally, large cardinal axioms imply that smaller cardinal axioms are consistent with ZFC.  Thus running your computer to search for contradictions in large cardinal axioms is a way to "test" larger cardinal axioms.
If you buy that, then one way to "test" an axiom is to look at what $\Pi^0_1$ sentences (i.e., sentences of the form "for all integers $n$, $P(n)$ holds" where $P(n)$ is some statement about the number $n$ that can be checked by a terminating computer program) the axiom implies.  Coming back now to the axiom of choice, there is unfortunately no way to test it in this manner, because it is a theorem that any $
\Pi^0_1$ sentence (in fact, any first-order sentence of arithmetic) is a theorem of ZFC if and only if it is a theorem of ZF.  The same goes for statements like the continuum hypothesis: any arithmetical theorem of ZFC + CH is already a theorem of ZF.
One might still wonder whether there is some other way to test mathematical statements using physical experiments.  It seems unlikely to me, mainly because as finite creatures we can make only finitely many physical observations, so I think that the only mathematical statements that we will be able to reject definitively on the basis of physical experiments will be finitary ones, and first-order arithmetic should be able to express any finitary mathematical statement.  It's true that, as some others have mentioned, some physicists have used the axiom of choice to construct physical theories, but if one of these theories were to be contradicted by experiment, we would probably just say that this disproves the physical theory, not the axiom of choice itself.
A: Answering your question specifically concerning real-world consequence of AC, it is worth noting that the answer is strongly dependent on whether or not the universe is discrete or continuous. Although quantum mechanics and high energy physics hint at a fully discrete universe, this is not at all settled. For example it is not known whether or not space-time is discrete. If the universe is discrete, and therefore either finitely or infinitely countable, depending on whether or not the size of the universe is finite (also not known), the full AC is no longer applicable (a choice function for finite sets can be proven within ZF). In this case AC would seem exceedingly unlikely to have real-world consequences.
