Reverse mathematics of the fundamental group

[Timothy Y. Chow]

This post is related to my recent post about covering spaces, but it is 
different enough that I thought I should start afresh.

Before I get to the main question(s), let me remark that I have been 
reading J. P. May's book, "A Concise Course in Algebraic Topology."  I 
have found this to be quite an illuminating book, because it demonstrates 
how a 21st-century topologist thinks about first-year graduate-level 
algebraic topology.  To quote from the Introduction:

    Our understanding of the foundations of algebraic topology has
    undergone subtle but serious changes since I began teaching this course
    [around 1970].  These changes reflect in part an enormous internal
    development of algebraic topology over this period, one which is
    largely unknown to most other mathematicians, even those working in
    such closely related fields as geometric topology and algebraic
    geometry.  Moreover, this development is poorly reflected in the
    textbooks that have appeared over this period.

Without going into too many details about these internal developments 
(which, not being an expert, I have only a vague grasp of anyway), I can 
say that algebraic topologists have, more than once, revamped and 
redefined what their main objects of study are.  Some of the earlier 
phases involved ignoring phenomena which, if not pathological, were 
intractable.  For example, there was a shift in attention from 
homeomorphism to homotopy equivalence, and from homotopy groups to stable 
homotopy groups.  Spaces were assumed to be compactly generated.  Instead 
of studying arbitrary spaces, one focused on CW complexes.  Later phases 
often focused on trying to find the "right" category to work in, which 
might involve introducing new objects of study.  Spectra are perhaps the 
most prominent example.  (FOM readers might be interested in the 
"foundational mini-crisis" around 1990 when it was discovered that certain 
desirable axioms for spectra were inconsistent: see L. Gaunce Lewis Jr., 
"Is there a convenient category of spectra?" J. Pure Appl. Alg. 73 (1991), 
233-246.)  J. P. May mentions that for homotopy theorists, Quillen's 
closed model categories are now the standard framework for much of the 
basic theory (model categories are not discussed in "A Concise Course" but 
they are studied in the sequel, "More Concise Algebraic Topology").

These advanced developments have not radically changed the first-year 
graduate material, but they have influenced May's ideas of which concepts 
deserve more emphasis and which approaches to proving things seem more 
natural and conducive to generalization.

Having said all that, I admit that I mainly want to focus on the 
fundamental group here, and in particular on aspects that May does not 
treat all that differently from other authors.  But I wanted to describe 
May's book because it's what I'm looking at right now, and because I think 
May has given a lot of thought to how to present this material from a 
21st-century perspective.

---

Now to specifics.  Let's consider Brouwer's fixed-point theorem.  As FOM 
readers all know, this theorem has been of foundational interest almost 
since its inception.  Initial controversies centered around intuitionism. 
The reverse mathematics story is that Brouwer's theorem is equivalent to 
WKL_0, and the unprovability in RCA_0 is traceable to Orevkov's 
"computable counter-examples."

But how does an algebraic topologist think about Brouwer's theorem? 
Well, they're not really bothered by the law of the excluded middle or by 
uncomputability.  For them, it's a simple corollary of a fact about 
fundamental groups.  Think in terms of the contrapositive: Suppose we have 
a map f from the disk into itself with no fixed point.  Then we draw a 
line connecting x to f(x) and we continue it to the boundary of the disk. 
If f were continuous, this would give a retract of the disk onto the 
circle; applying the fundamental group functor, this would give a 
homomorphism from Z to 0 to Z which sends 1 to 0 to 1, but this is absurd.

Interestingly, one key step of the argument---moving from x to f(x) and 
continuing to the boundary---has a constructive and computable feel to it. 
If, as reverse mathematicians, we're hunting for where the uncomputability 
snuck in, it seems that we should be looking at the computation of the 
fundamental group.

The way the fundamental group of the circle S^1 is usually computed is by 
observing that the real line R is a universal covering space for S^1. 
Maps from [0,1] to S^1 are uniquely lifted to maps from [0,1] to R. 
Here's where maybe something sneaky is occurring, because compactness is 
needed.  Certainly one way to proceed is to invoke Heine-Borel, so we 
could claim that this is the point where we make the jump from RCA_0 to 
WKL_0 and then onto Brouwer.

However, I'm a bit uneasy about accepting this narrative too quickly.  I'm 
not sure about the right way to deal with the fundamental group in 
second-order arithmetic.  On the face of it, the fundamental group has an 
uncountable feel to it.  Moreover, from May's point of view, once you have 
the basics of the fundamental group and covering spaces in place, you're 
in a position to apply it to graphs, and then the Nielsen-Schreier theorem 
falls out immediately.  As Andrew Swan helpfully pointed out here on FOM, 
if you have a free group and you want to say that a subgroup *given by 
generators* is free, then the unsolvability of the word problem rears its 
head, forcing you out of RCA_0 into...WKL_0?  No, apparently now you're in 
ACA_0 territory.  So where did *that* sneak in?

All this is to say is that there seems to be a disconnect between what the 
algebraic topologists think are the key steps and where the reverse 
mathematicians say you need a new axiom.  Well, it's not news that logical 
strength doesn't always line up with what our mathematical intuition says 
is "the hard part."  Nevertheless, I wonder if there is a way to treat 
this material about the fundamental group and covering spaces (which May 
says is "one of the few parts of algebraic topology that has probably 
reached definitive form") that sounds like a good story to both a 
topologist and a reverse mathematician.

Tim