A question about formulating first order axioms for group theory.

Let T be a first order theory whose set of axioms is one of the standard finite sets of axioms for an arbitrary group. Is it possible to have an axiomatizable first order extension of T which would characterize just those groups that are finite, simple and "sporadic"? In other words I am asking whether the properties of being finite, simple and "sporadic" can each be expressed by a recursively enumerable (or perhaps even finite) set of first order axioms? I realize, of course, that if we know the "Monster" to be the largest such group and know its cardinal number, then our task becomes considerably simpler. But I would consider this to be cheating and don't want to assume that we have such knowledge. I confess that I don't know much about group theory and have never seen a clear precise statement of what it means for a group to be "sporadic". Otherwise I would have refrained from asking these questions which I suspect will all sound stupid to a group theorist.

-
The key problem seems to me that, naively, finite and simple are second-order properties, whereas sporadic naively might mean "not part of a nice infinite family of finite simple groups" or "not a cyclic group, an alternating group, or a Chevalley group" or something else that's hard to axiomatize elegantly. There are indeed many first-order axiom systems whose only models are the 26 finite simple sporadic groups, but by completeness they are all equivalent. –  Will Sawin Oct 20 '12 at 20:31
Presumably, what you are looking for is a relatively elegant axiom system in which the proof of the classification of finite simple sporadic groups is possible and that proof approximates the standard proof of the classification in ZFC. I have no idea if such a thing is possible. –  Will Sawin Oct 20 '12 at 20:34

Because there are only finitely many sporadic simple groups, you can write, for each of them, a first-order sentence characterizing it up to isomorphism, and then you can form the disjunction of those sentences. But you don't want to build into your sentences our knowledge of the sporadic groups, and then you run into the theorem that, if a first-order theory has arbitrarily large finite models, then it also has infinite models. So any first-order characterization of the sporadic simple groups must depend on the fact that there are only finitely many of these groups.

You also asked about characterizing, in a first-order way, the individual properties "finite", "simple", and "sporadic" (in contrast to just characterizing their conjunction). That is certainly impossible for "finite", by the theorem I quoted above. I would expect that it's also impossible for "simple" and "sporadic", but I don't know that for sure.

-
The question of whether "sporadic" is first-order seems ill-formed to me, since I'm not sure there's a definition of sporadic in the first place, but towards showing the non-first-orderness of simplicity: is the ultraproduct of a sequence of increasingly large simple groups, by a non-principal ultrafilter, known to be simple? I would guess that it would generally not be simple, but I can't prove that. –  Noah S Oct 20 '12 at 22:55
In fact, isn't the ultraproduct of the finite cyclic groups of prime order not simple? –  Noah S Oct 20 '12 at 22:56
Specifically, it is infinite, so has proper non-trivial subgroups, and is abelian, so every subgroup is normal; but since each finite cyclic group of prime order is simple, if there were a first-order characterization of simplicity, the ultraproduct would have to also be simple, so we're done. (Or have I made a mistake somewhere?) –  Noah S Oct 20 '12 at 23:33
I was taking "simple" to include "non-abelian", as group-theorists sometimes do, but as I probably shouldn't. –  Andreas Blass Oct 21 '12 at 0:26
The ultraproduct of non-abelian simple groups need not be simple. This is discussed in an earlier mathoveflow question: mathoverflow.net/questions/32908/… –  Dave Marker Oct 21 '12 at 14:40

(Too long for a comment:)

The answer comes down to exactly what "sporadic" means in this context, and how much we're allowed to know about the sporadic groups.

In particular, if we can't assume that we know that there are only finitely many sporadic groups, then we definitely don't "have" (whatever that means) any set of sentences (finite, r.e., or otherwise) capturing the finite sporadic groups, since any set of first-order sentences with arbitrarily large finite models has infinite models. That is, either we know that there are only finitely many "sporadic" groups (again, whatever that means), or we cannot possibly have an axiomatization of them.

On the other hand, if we do assume that we know that there are only finitely many sporadic groups, then we know right away that there exists such an axiomatization (in fact, a finite one), even though we don't know what it is.

The interesting case would be the following: given a definition of "sporadic," how much knowledge of finite group theory do we have to have in order to come up with an axiomatization of precisely the finite simple sporadic groups? Now merely knowing there are finitely many is not enough; whereas the whole classification is definitely enough, but possibly overkill. Note that this is a tricky question to formalize: how do we talk about limiting our knowledge of finite group theory? I suppose one could ask for pairs (axiomatization of finite simple sporadic groups, proof that said axiomatization actually works) that are reasonably short; that might yield something interesting, but my group theory is nowhere near good enough to speculate.

(Another way to approach this problem would be to work in some extremely limited axiom system - say, a weak subsystem of $RCA_0$ - in which the classification of finite simple groups doesn't go through, and try to construct an axiomatization there. But there is no reason I know of to believe that the classification, hard as it is, doesn't go through in such simple systems, so this approach is probably doomed to failure.)

-
Thanks to both of you for pointing out so clearly what is really involved in finding first order axioms for the finite, simple and sporadic groups. Since there are arbitrarily large finite simple groups (all the cyclic groups of prime order, for example) any first order axioms can only exist if "sporadic" groups are included in the right way. But what is the right way? Noah has focussed on the real question here better than I did. –  Garabed Gulbenkian Oct 21 '12 at 19:19