Reverse Mathematics of the Nielsen-Schreier Theorem

by Rodney G. Downey, Denis R. Hirschfeldt, Steffen Lempp, and Reed Solomon

Status: published in Proceedings of International Conferences on Mathematical Logic, Novosibirsk State University Press, 2002, pp. 59 - 71.

Availability: DVI and PostScript

Abstract. The Nielsen-Schreier Theorem states that every subgroup of a free group is free. To formalize this theorem in weak subsystems of second order arithmetic, one has to choose between defining a subgroup in terms of a set of group elements and defining it in terms of a set of generators. We show that if subgroups are defined by sets, then the Nielsen-Schreier Theorem is provable in RCA0, while if subgroups are defined by generators, the theorem is equivalent to ACA0.