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.

>>13
Here you go: suppose, for contradiction, that the class of finite sets is axiomatizable: let S be the set of wffs meaning "X is finite".  Then union S with all the wffs "X has size at least n" for each natural number n; call the union S_1.  S_1 is finitely satisfiable, obviously: in a finite subset S_0, there is some largest n that appears, so S_0 is satisfied by a model with n elements.  Then by compactness, S_1 is satisfiable.  But a model X for S_1 is clearly infinite, though we should have X satisfying S - contradiction.