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.



How much of mathematical General Relativity depends on the Axiom of Choice?
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](https://arxiv.org/abs/1309.7591), and Willie Wong, in [A comment on the construction of the maximal globally hyperbolic Cauchy development](https://arxiv.org/abs/1310.1318) (the latter having been mentioned by Asaf Karagila in the [comments](https://mathoverflow.net/questions/453123/how-much-of-mathematical-general-relativity-depends-on-the-axiom-of-choice#comment1172084_453123)).


More generally, an analogous, but non-exhaustive, discussion has appeared earlier over at [M.SE10102](https://math.stackexchange.com/q/10102 "Where do we need the axiom of choice in Riemannian geometry?") and [MO45928](https://mathoverflow.net/q/45928 "Does Arzelà-Ascoli require choice?") 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](https://arxiv.org/abs/2010.15632) by Asaf Karagila and [the answer by Cloudscape](https://mathoverflow.net/a/218133/2622) to [MO45928](https://mathoverflow.net/q/45928 "Does Arzelà-Ascoli require choice?"), 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](https://math.stackexchange.com/q/10102 "Where do we need the axiom of choice in Riemannian geometry?") and [MO](https://mathoverflow.net/q/45928 "Does Arzelà-Ascoli require choice?") discussions).


* <https://cgraph.inters.co/>


