Cardinality of finite sets in first order set theory

Question

How would one determine if two finite sets have the same cardinality using first order set theory? Would there be a formula for showing that $$ F(x,y) \iff |x|=|y|?$$

Answer 1

Remember that a function is a set of ordered pairs with a certain property (namely, being functional).

We can write the following formulas:

1. $\varphi_0(x)$ states that $x$ is an injective function.
2. $\varphi_1(x,y)$ states that $x$ is a function and its domain is $y$.
3. $\varphi_2(x,y)$ states that $x$ is a function and its range is $y$.

Now write $F(x,y)$ as $\exists f\big(\varphi_0(f)\land\varphi_1(f,x)\land\varphi_2(f,y)\big)$. I leave you to write $\varphi_0,\varphi_1$ and $\varphi_2$ as an exercise in formalization. Note that this whole thing really depends on how you encode functions, which is usually dependent on how you encode ordered pairs.

Note that "finite" has no role here, by the way.