# What are the “ordinary” (e.g. arithmetic) consequences of the universe axiom?

Consider the first-order theory obtained by adjoining to ZFC (or, better, Mac Lane set theory) the Grothendieck–Verdier (or Bourbaki?) universe axiom:

• For each set $x$ there exists a Grothendieck universe $\mathbf{U}$ with $x \in \mathbf{U}$.

Of course, this is strictly stronger than ordinary ZFC because it proves $\textrm{Con}(\mathsf{ZFC})$. In fact, it proves $\textrm{Con}(\mathsf{ZFC} + \mathsf{Con}(\mathsf{ZFC}))$, $\textrm{Con}(\mathsf{ZFC} + \mathsf{Con}(\mathsf{ZFC} + \mathsf{Con}(\mathsf{ZFC})))$, and so on, as well as variants where $\mathsf{Con}$ is replaced by stronger notions of consistency. On the other hand, this can be rephrased in terms of Gödel numbers as a number-theoretic proposition (and if I understand correctly, even as the existence of solutions for a Diophantine equation), and so these are examples of arithmetic consequences of the universe axiom.

However, this feels somewhat contrived. What I want to know is this:

Question. Is there a down-to-earth statement in ordinary mathematics (algebra, number theory, finite combinatorics, real analysis, etc.) that is decided by the universe axiom?

-
Now when you say "down-to-earth", I suppose you don't mean "Zero sharp exists", or so on; but rather some real life arithmetical/analytical statement? Because Mostowski absoluteness theorem comes to mind (it's like Shoenfield, but weaker, and with less assumptions). –  Asaf Karagila Apr 13 '13 at 23:33
I don't understand what $0^\sharp$ is, so that surely can't be down-to-earth! –  Zhen Lin Apr 13 '13 at 23:34
I can't understand the Riemann Hypothesis! Is that not down to earth? :-) –  Asaf Karagila Apr 13 '13 at 23:35
Nope, I don't understand that either. (It would be extremely surprising if it does turn out to be decided by the universe axiom, however!) I guess what I want to understand is how it is that the existence of "big" sets can affect "small" sets. –  Zhen Lin Apr 13 '13 at 23:40
Well, if $0^\#$ exists then (lightface) $\Sigma^1_1$ games are determined, and then some. But these are stronger assumptions than universes axiom; and you may disagree with the down-to-earth-ness of their consequences. –  Asaf Karagila Apr 13 '13 at 23:44