how can we express finiteness as a first order property?

Question

I don't know much about set theory but I read that in ZFC a set is finite when there are no bijections from the set to a proper subset of itself. It seems to me however that quantifying over subsets or over all functions is not first order (correct me if I'm wrong). So is it possible to express finitess as a first order property? Thanks

Answer 1

The sentence $\psi(A)$ given by $$\forall x(x\subset A\land x\neq A\to \forall f(f\text { is a function from }A \text{ to }x\to f\text{ is not injective}))$$ is first order, and is true iff $A$ is finite.

Answer 2

But all the elements of the universe are sets. Functions too. In set theory the power set is just an element, and its elements are also just ordinary objects too.

So when you say "quantify over all subsets and functions" we really just quantify over objects of the universe of sets. So it is a first order statement saying that certain objects do not exist in the universe.

From a[n internal] set theoretic perspective, second order logic means quantifying over proper classes.