# 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
• As I know, the original proof of FLT uses Universes. But maybe much less (PA?) is required. – Martín-Blas Pérez Pinilla Mar 20 '17 at 13:09