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.

>>16 and >>18, YES!!! Assuming something is true without proof only at the start is an axiom. What we do to test that axiom is called questioning, after the questioning comes the paradox where what we really weren't sure of the validity of the axiom, now has been proven and is now paradox. GOOD JOB!