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.
 A: 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.  
A: (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.)
