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.

>>1
If you can count it, it's finite.

presto, definition