Logic question - finiteness definable?

In my undergrad logic course, we came across a couple of results about finiteness not being definable, using compactness of 1st order logic.  In particular, I remember the class of finite sets not being axiomatizable (in the sense that there's no set of wffs S such that A |= S iff A is a finite structure).

This runs contrary to what I've seen in discussions of set theory, i.e. defining a subset of A as {x in A : x is finite}.  But can we construct a first order wff P(x) meaning "x is finite"?  I guess I'm just asking for a formal justification of definitions like this.  Any help would be appreciated.

>>8
lol oops that 'not' was of course meant to be there. Also I see how I didn't really answer your question. I wouldn't be very surprised if finiteness is non-axiomatizable but I'd like to see a proof.

Given a number n it should be easy to make axioms so that any model for them has n elements, but it's a very different thing to axiomatize the existence of such a number in FOL.