How much of mathematical General Relativity depends on the Axiom of Choice?

Question

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.

Answer 1

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).

• https://cgraph.inters.co/

Answer 2

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:

• Ye, F. (2011). Semi-Riemannian Geometry. In: Strict Finitism and the Logic of Mathematical Applications. Synthese Library, vol 355. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-1347-5_8

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").

Answer 3

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?

Reference(s)

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