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?