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.

Hmm, not logic-fag but I'll try anyway.

Let's use a language L=(in, f) where in is a binary relation symbol and f is a unary function symbol (the rest of FOL-language is implicit, hope you understand my notation). In addition I assume we  need a collection S of axioms for set theory.

So what about:

A(X):= for all (x in X):  (f(x) in z)  [f:X->X]
B(X):= for all (x,y in X): ((f(x) = f(y)) -> (x=y)) [f is injective]
C(X):= exists (x in X): ( for all (y in z): (f(y) != x))[f(X) is a proper subset]
D(X):= A(X)&B(X)&C(X) [X is finite (?)]

Can we find a model for S and the sentence 'exists X: D(X)' ? If S = ZF?

(Waiting for logician in shining armor to clear up mess)