One of the cornerstones of the mathematical formulation of General Relativity (GR) is the result (due to Choquet-Bruhat and others) that the initial value problem for the Einstein field equations is solvable and it admits a essentially unique maximal (globally hyperbolic) development (GHD).

The proofs I have seen of this all seem to make use of the Axiom of Choice (AC) in a nontrivial way (usually, Zorn's lemma is applied twice: first to prove the existence of a setwise maximal solution, then to prove the existence of a common GHD given two solutions, from which one then infers the result). Hence the question as in the title: how much AC is really needed for all of this?

The question can be interpreted mainly in two ways:

  1. Literally. Since a lot of analysis is dependent from some form of AC, and a few results from PDE theory are needed for the theorem, I'm skeptical that this interpretation has an easy answer: backtracking all the applications of AC seems unfeasible.

  2. Restricting the question to "natural scenarios": maybe one needs the full force of AC to prove the theorem for completely general initial data, but restricting to a natural class of data it turns out that we can make explicit choices in the arguments necessary.

Any reference, observation or comment is welcome.

EDIT: It seems that Zorn's lemma is not really needed after all. I'm fairly convinced by now that the complete theorem can be proved in ZF+DC (i.e. that all the analysis needed for the theorem can be done in that context) but also that actually checking everything to see that this is the case would be a painstakingly long process. I am still very interested in the absoluteness approach hinted at by Gro-Tsen, Dorais, Chow and Hanson, but that is material for a new question.

  • 9
    $\begingroup$ Your question would be clearer without so many UAs. $\endgroup$ Commented Aug 20, 2023 at 15:17
  • 20
    $\begingroup$ doi.org/10.1063/1.4833375 $\endgroup$
    – Asaf Karagila
    Commented Aug 20, 2023 at 15:17
  • 21
    $\begingroup$ @YemonChoi Agreed, but still my comment is true. The question (and comments) would be clearer without unexplained acronyms. It is not difficult to write the words general relativity, axiom of choice, etc. There seems to be no need for abbreviation at all. $\endgroup$ Commented Aug 20, 2023 at 15:36
  • 10
    $\begingroup$ I opened this question expecting, just from the title, an unmotivated "hopping on the bandwagon" question about how much Choice is needed for Hot Topic X. But it seems to me (as no expert in relativity, or, for that matter, the subtleties of Choice) that your motivation makes it into an excellent question. Thank you for the work you put into writing such a good question! $\endgroup$
    – LSpice
    Commented Aug 20, 2023 at 20:37
  • 14
    $\begingroup$ The existence of numerical general relativity algorithms that can be proven (assuming AC) to converge to genuine solutions (provided that they exist with suitable regularity) strongly suggests to me that any appearance of AC in the theory can be eliminated with sufficient effort. (Whether it is actually worth expending this effort is another matter.) $\endgroup$
    – Terry Tao
    Commented Aug 20, 2023 at 21:43

3 Answers 3


The dependence on AC through the use of Zorn's lemma in the proof of the Choquet-Bruhat–Geroch theorem on the existence of a maximal globally hyperbolic development for solutions of the Einstein equations has been eliminated around the same time by Jan Sbierski, in On the Existence of a Maximal Cauchy Development for the Einstein Equations — a Dezornification, and Willie Wong, in A comment on the construction of the maximal globally hyperbolic Cauchy development (the latter having been mentioned by Asaf Karagila in the comments).

More generally, an analogous, but non-exhaustive, discussion has appeared earlier over at M.SE10102 and MO45928 in the context of Riemannian geometry.

The conclusion seems to be that several fundamental results in functional analysis anyway use the axiom of choice or some version of it. Mathematical GR certainly uses the theory of linear (and nonlinear) elliptic and hyperbolic PDEs, which in particular relies on the theory of Sobolev spaces (and possibly also Schwartz distributions). The basic results where (to my knowledge) AC creeps in include

  • the Hahn–Banach theorem,
  • the countable additivity of Lebesgue measure (may be used in Sobolev theory),
  • the Arzelà–Ascoli and Fréchet–Kolmogorov theorems (used in Sobolev embeddings),
  • the Banach–Alaoglu theorem (as a step in applying Schauder-like fixed-point theorems),
  • the uniform boundedness principle,
  • and maybe others.

Most likely, the list is non-exhaustive. From the notes Zornian Functional Analysis or: How I Learned to Stop Worrying and Love the Axiom of Choice by Asaf Karagila and the answer by Cloudscape to MO45928, it seems that there are versions of these theorems that do not require AC under some hypothesis (like restricting to separable Banach spaces) or only a weakend version of it (like countable choice). I guess that it might be an open question, whether all of this dependence on AC could be eliminated under sufficiently reasonable hypothesis (say sufficient for the mathematical study of gravitational waves from astrophysical sources). If one could write a reasonable textbook on PDE theory without AC, then probably one could adapt the same methods to Mathematical GR.

For reference, below is the currently functional link to the online database of the consequence of AC. Not all the above theorems appear there by name, but maybe only in some equivalent version (cf. the previously mentioned M.SE and MO discussions).

  • 9
    $\begingroup$ I think it's important here to separate countable or dependent choice from full AC. Even lots of first year analysis depends, at least as written, on countable choice. Personally I think it's fine to take CC or even DC as simply "true", but carefully track any stronger uses of choice, which are extremely hard to imagine being physical. $\endgroup$ Commented Aug 21, 2023 at 7:19
  • 2
    $\begingroup$ See Martin Väth's answer to another MO question for more information about how much choice is needed for basic analysis. $\endgroup$ Commented Aug 21, 2023 at 12:07
  • 2
    $\begingroup$ @Z.M In the absence of choice, Dedekind reals and Cauchy reals are not the same. The traditional development of measure theory uses choice. I'm not sure if these count as "first year analysis" though. $\endgroup$ Commented Aug 21, 2023 at 20:25
  • 3
    $\begingroup$ @Z.M See Section 3 of Ruitenberg, Constructing roots of polynomials over the complex numbers. See also Richman, Constructive mathematics without choice, who showed that if you drop both choice and excluded middle, then even the fundamental theorem of algebra has issues. $\endgroup$ Commented Aug 21, 2023 at 22:55
  • 4
    $\begingroup$ @TimothyChow: You mean in the absence of LEM, I think. The Cauchy completion and Dedekind completion are equivalent in ZF. $\endgroup$
    – Asaf Karagila
    Commented Aug 22, 2023 at 6:56

It's not the headline theorem you wanted, but this gives at least a lower bound on what is possible in much weaker foundations than usually assumed, and also analyses a serious theorem in that setting:

This chapter develops the basics of differentiable manifolds and semi-Riemannian geometry for the applications in general relativity. It will introduce finitistic substitutes for basic topological notions. We will see that after basic topological notions are available, the basic notions of semi-Riemannian geometry, i.e., vector, tensor, covariant derivative, parallel transportation, geodesic and Riemann curvature, are all essentially finitistic already. Theorems on the existence of spacetime singularities are good examples for analyzing the applicability of infinite and continuous mathematical models to finite physical things. The last section of this chapter will analyze one of Hawking’s singularity theorems, whose common classical proof is non-constructive. The section will show that the proof can be transformed into valid logical deductions on statements about real spacetime from literally true premises about real spacetime, even if real spacetime is discrete at the microscopic scale. Therefore, the conclusion of the theorem is physically reliable for real spacetime, in spite of the fact that the common proof of the theorem appears to assume that spacetime is literally isomorphic with a classical differentiable manifold (and hence absolutely non-discrete).

The foundational system in this book is a fragment of arithmetic. Experts in mathematical general relativity would be better placed than me to discuss how restrictive the "Geodesic Stability Assumption" on page 260 is (this is, I believe, the rigorous version of what is intended in the above paragraph by "literally true premises about real spacetime").


My (attempt at an) answer goes in the direction of "2. natural restrictions".

First of all, as noted in the comments, provable in ZF are restrictions of AC to the language of second-order arithmetic. However, in this frugal language, one only has variables for natural numbers and subsets of $\mathbb{N}$. All other objects, like functions from reals to reals, have to be represented/coded and things get complicated rather quickly. Moreover, people have not studied much real analysis beyond the continuous in this context. Hence, this approach may not be suitable, but there is a more "middle of the road" solution, as follows.

Secondly, the following function classes are such that if $f:\mathbb{R} \rightarrow \mathbb{R}$ is an element, one can approximate (by definition) $f(x)$ for any fixed $x\in \mathbb{R}$ using nothing more than $f(q)$ for any $q \in \mathbb{Q}$:

Quasi-continuity, cadlag, Baire 1, effectively Baire 2, normalised bounded variation (and many more). (A)

Experience shows that any property of these function classes can be proved from second-order comprehension axioms (in a weak higher-order theory, see [1]), i.e. everything definitively takes place in ZF.

Thirdly and obviously, there are function classes for which the previous paragraph is false. Here are some examples:

Bounded variation, regulated, semi-continuous, cliquish, and Baire 2. (B)

To prove properties of these function classes, "actual AC not provable in ZF" may be needed.

In conclusion, if (A) suffices for your purposes, then AC can be omitted (and actually, second-order comprehension axioms are enough). If you need (B), then AC will pop up here and there.

Of course, what does "you need (B)" mean in the context of physics?


[1] Dag Normann and Sam Sanders, the Biggest Five of Reverse Mathematics, arxiv: https://arxiv.org/abs/2212.00489

  • $\begingroup$ Where do $L^2(\mathbb{R}^n)$ or $L^2([0,1]^n)$ functions fit in your (A) vs (B) dichotomy? One could also ask about smooth functions $C^\infty(\mathbb{R}^n)$, but these would need to be accompanied by Schwartz distributions on $\mathbb{R}^n$ as well. $\endgroup$ Commented Aug 23, 2023 at 9:50
  • $\begingroup$ I'm confused about your (A) vs (B) dichotomy. Bounded variation functions and semi-continuous functions are in Baire class 1, and Baire class 2 is the same as effective Baire class 2. These are all provable in much less than ZF (say, $Z_2$). $\endgroup$ Commented Sep 13, 2023 at 4:21
  • $\begingroup$ @ElliotGlazer the following third-order statement is consistent with RCA$_0^\omega$+ Z$_2$ and stronger systems: "there is a function of bounded variation on [0,1] that is totally discontinuous". Here, $\text{RCA}_0^\omega$ is Kohlenbach's base theory of higher-order RM, which is $L_2$-conservative over RCA$_0$. This implies that the usual hierarchy of function spaces looks VERY different in weak (and some strong) systems. $\endgroup$ Commented Sep 14, 2023 at 6:50
  • 1
    $\begingroup$ I see. Sifting through your papers, I think the arguments justifying my previous comment are formalizable in $Z_2^{\Omega},$ and that this theory is a conservative extension of $Z_2$ which has third-order objects in its ontology. Is my understanding correct? $\endgroup$ Commented Sep 14, 2023 at 7:40
  • 1
    $\begingroup$ Right that's why I think $Z_2^{\Omega}$ is the "right theory" for choiceless analysis. I expect choiceless analysis of the classes BV, semi-continuous, Baire class to go through under any subsystem of $Z_3$ containing the schema extending $\Pi^1_2$-CA to allow third-order parameters. $\endgroup$ Commented Sep 15, 2023 at 14:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.