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.

>>5
Looks right to me, except for the minor omission of "not"s in the statement of D(X);  and I think you've highlighted the distinction between the result I mentioned and what we're trying to formalize.  A model A of ZF is necessarily infinite, while a finite subset X in the model A should satisfy the wff D(X).  And I'm not sure if the function symbol is necessary, since we can talk about functions as sets of ordered pairs within the language of set theory.

On the other hand, our result from class stated that no set of wffs exists such that a structure is finite iff it satisfies the wffs.  That is, regardless of what relation/function symbols the structure is endowed with.  This is a somewhat different statement than saying that finite sets are not definable within ZF.

Also, when I talked about finiteness not being definable, I may have been thinking of the finite elements in the nonstandard model of arithmetic.  My apologies, for I am still very confused by all this :/