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:

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.

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.

12more comments