Weak weak Koenig and covering spaces

[Andrew Swan]

> There are some basic results about finitely generated groups that have
> nice proofs using covering spaces.  Perhaps the simplest one is that a
> subgroup of a free group is free.  More sophisticated examples can be
> found in Serre's book "Trees."  Are any of these results unprovable in
> RCA_0?

Regarding the Nielsen-Schreier theorem (subgroups of free groups are
free) it isn't necessary to use covering spaces, or any topology at
all. There are direct proofs, including the original proof by
Schreier. (See also my paper at https://arxiv.org/pdf/2010.01187 for a
proof that uses ideas and intuitions from algebraic topology without
any actual topological spaces). The reverse mathematics has been
studied by Downey, Hirschfeldt, Lempp and Solomon in
https://www2.math.uconn.edu/~solomon/research/nielsen.pdf . They
showed that depending on how the theorem is formulated it is either
provable in RCA_0 or equivalent to ACA_0.

Best,
Andrew Swan