A **Serre class** (of abelian groups) is a class of abelian groups closed under subgroups, quotients, and extensions. For instance, finitely generated groups and finite groups are both Serre classes.

However, in constructive mathematics, these are no longer examples, at least not with the usual definition of "finite" (= in bijection with $\{0,1,\dots,n\}$ for some $n\in\mathbb{N}$). In particular, finite sets are not closed under subsets and quotients, so there is no reason that finite groups should be either.

There are other weaker constructive notions of "finite", some of which are described here: subfinite, finitely indexed, subfinitely indexed. It seems that subfinitely indexed sets — the subquotients of finite sets — are closed under subsets, quotients, and finite products, so that the subfinitely indexed groups should be a Serre class even constructively. Classically, of course, all subfinitely indexed sets are finite.

My original question was:

Is there a Serre class of abelian groups in constructive mathematics which reduces classically to the finitely generated ones?

As pointed out by Ingo, this has a trivial and uninteresting answer; the real question is

Is there a description of the Serre envelope of the class of finitely generated abelian groups which is more explicit than the trivial inductive one?

decidablesubgroups and quotients bydecidablenormal subgroups. But you probably need fairly arbitrary quotients, yes? – Andrej Bauer May 29 '13 at 23:49don'twant to change the definition of Serre class. I don't think the application I have in mind (spectral sequences) will yield any decidability conditions. – Mike Shulman May 30 '13 at 5:21antisubgroupsas well as subgroups. – Andrej Bauer Jun 1 '13 at 19:07