FOM: Predicativism, GR, ACA_0, Zorn's Lemma

[Matthew Frank]

Dear Jeff, Joe, and everyone else (--set theorists in particular please
look at the question at the end of the paragraph marked 1),

Jeff brought up a theorem in relativity and a comment of Bob Geroch, and
wondered if this might show some intellectual schizophrenia on his part.
I do not think it does; here is what he wrote to me on Jan. 13 about the
theorem in question:

[The theorem]
> (with Y. Choquet-Bruhat) asserts that, given
> initial data for Einstein's equation (say) on a 3-surface, there
> is a unique "maximal evolution" of that data (maximal in the
> sense that you evolve to a solution in which the original surface
> is a Cauchy surface, and the one guaranteed by the theorem is the
> largest, in that every other evolution fits inside of it).  The
> original proof of this used Zorn's lemma ("consider all possible
> evolutions, ordered by 'is an extension of'").  It certainly was
> non-constructive, and there was some discussion about this issue.
> But, it seems "quite clear" (i.e., we discussed it a few times in
> the relativity  meeting, but we, at least, never published
> anything on it) that one can modify the proof slightly and get
> rid of Zorn's lemma, making it about as constructive as anything
> else in mathematical physics.  It becomes about as constructive
> as the LUB of a sequence of numbers bounded above.  (In retrospect,
> perhaps we should have been more careful from the start, to avoid
> Zorn.)

My claim was that any theorem of mathematical physics could be recovered
predicatively or in ACA_0; that "anything in mathematical physics is
about as constructive as the LUB of a sequence of numbers bounded above"
is about the strongest confirmation you could ask from someone who doesn't
know the technical terms I used.

So now let me address in more detail:  1) the particular theorem in
general relativity; 2) the larger claim about predicative math and ACA_0;
and 3) "anything goes".

1) Independently of the note from Geroch, the statement of the theorem
makes it a bad candidate for something "in the standard development of GR
which depend[s] on Zorn's lemma".  It is a claim that there exists a
unique object satisfying a certain property, and in practice, Zorn's lemma
does not seem to be needed to prove such claims.  (I suspect that ZFC is
conservative over ZF for formulas of form "there exists a unique x such
that phi", or for most such formulas--does anyone know of any results like
this?)

The proof of the theorem (in chapter 7 of Hawking and Ellis, The Large
Scale Structure of Spacetime) falls into two parts.  The first (larger,
harder) part is a local theorem about embedding the 3-manifold ("space")
into a 4-manifold ("space-time") satisfying Einstein's equation; this is
PDEs, and uses the theory of Sobolev spaces.  Since continuous functions
are dense in the Sobolev spaces, there should be little difficulty in
making this predicative or ACA_0 (at least for someone who likes and is
good at this sort of analysis--not me!).  The second part is about putting
all the local developments together to get a maximal development, and this
is where Choquet-Bruhat and Geroch used Zorn's lemma.  One could
alternatively and predicatively argue as follows:  (This may well
need clarification; Bob Geroch probably had something simpler in mind.)

The topology of the 4-manifold whose existence the theorem proves is fixed
in advance as the 3-manifold x R.  So we can consider the set of all
metrics on that 4-manifold which satisfy Einstein's equation and coincide
with the 3-manifold at t=0.  Then restrict attention to a countable dense
subset M of those metrics.  Now fix a point p on the 3-manifold.  For each
metric g in M, consider the geodesic going through p and orthogonal to the
3-manifold.  The metric of the 4-manifold along that geodesic is given by
sixteen continuous functions f_{g,i}(t), where 1 <= i <= 16 and t is given
by distance to p.  For any g and g' in which the geodesic from p extends
as far as t, f_{g,i}(t) and f_{g',i}(t) will agree; so we can find some
universal f_{i}(t) which includes all of them.  Then the desired metric on
the 4-manifold is simply what we get by putting together all of the f's 
corresponding to the various points on the Cauchy surface.

I think I could do something similar for all of the interesting claims in
Hawking and Ellis or in Wald's book on General Relativity; if someone has
a question about a particular claim, I'd be willing to look at it.  (Note
in particular that Hellman discusses claims in section 9.4 of Wald's book,
which are treated more constructively in section 6.7 of Hawking and
Ellis's.)

2) Joe wanted to know on what I based my opinion that a more
satisfying mathematical treatment of quantum field theory would be easy to
recover predicatively.  I based this claim on my more general impression
that most of ordinary moathematics can be recovered predicatively and in
ACA_0, and that in turn is based on Feferman's work and on the reverse
mathematics literature respectively.

Feferman has shown how to do a good deal of mathematics predicatively, and
it looks very much like ordinary mathematics:  it is a good formalization.  
For continuous functions the change from least upper bounds of sets to
least upper bounds of sequences makes little difference.  Similarly, in
ordinary mathematics we rarely feel the urge to make impredicative
definitions; their lack, or a lack of an appropriate axiom of choice,
rarely seems to matter.  So I suspect that most ordinary mathematics can
be recovered predicatively, and I regard the claim that all of the
theorems of mathematical physics can be recovered predicatively as a good
test case of this.

So far, the reverse mathematics literature has found most results in
ordinary mathematics to be at or below ACA_0.  Harvey Friedman's recent
work on the reverse mathematics of Ulm theory (the theory of countable
abelian groups), showing much of it to be ATR_0, is a wonderful exception;
in particular it convinces me that there will not be a satisfying
constructive version of Ulm theory.  On the other hand, Ulm theory is
notably distant from any topic I know of in mathematical physics, and I
would say the same of the Pi^1_1-CA and ATR_0 results on p. 34 and p. 39
of Simpson's book.  

I know almost nothing about QED, and not enough about some aspects of
predicative mathematics, so I am not in a good position to develop QED
predicatively.  However, I predict that someone selects a good theorem
which the QED textbooks quote, and that if we asked the people more
knowledgeable about predicative mathematics how to recover it
predicatively, that they would not have too much difficulty in doing so.

3) Jeff stated that his sympathies are with the position "anything goes!",
and I have the same sympathies.  I am happy to see mathematics of any sort
applied in physics, whether constructive, predicative, impredicative,
using large cardinals, or whatever.  I also think that learning how to
work within some of the restricted frameworks, particularly the
constructive framework, can lead us to new ways of thinking and new
insights which are useful even for the classical mathematician.  At the
moment I think this is the best argument for pursuing constructive
mathematics, and that is the way in which I am pursuing it.

--Matt

P.S.  Thanks to both Jeff and Joe for the valuable comments!