What's the first-order logical expression of this statement?

Question

Definition: a set $X$ is finite if and only if it has cardinality $n$ for some natural number $n$

"Let $X$ and $Y$ be finite sets. Then $X \cup Y$ is finite and $\#(X \cup Y) \le \# X + \# Y $" ($\#X$ means the cardinality of $X$)

What's the first-order logical expression of this statement?

Answer 1

Asaf Karaglia's question in comments is very relevant: what predicates and constants do you have in your language?

Meaning, can I write $\#X=n$ in a formula to mean that the cardinality of $X$ is $n$? Can I write $\mathbb{N}$ for the set of natural numbers? Can I use the order of natural numbers as a given? I assume I can use all of this, although it would not be specially problematic to assume both the cardinality equality and the order as not given (things are not as simple if $\mathbb{N}$ is not available).

So what I would write is $$\forall X\forall Y\Big(\exists n\exists m(m\in\mathbb{N}\wedge n\in\mathbb{N}\wedge \#X=m\wedge\#Y=n)\rightarrow \exists p(p\in\mathbb{N}\wedge \#(X\cup Y)=p\wedge p\leq m+n)\Big).$$ That is:

• for any two sets corresponds to $\forall X\forall Y$;
• the assumption that both $X$ and $Y$ are finite corresponds to $\exists n\exists m(m\in\mathbb{N}\wedge n\in\mathbb{N}\wedge \#X=m\wedge\#Y=n)$, meaning there exist ($\exists m\exists n$) natural numbers ($m\in\mathbb{N}\wedge n\in\mathbb{N}$) that equal the cardinalities of $X$ and $Y$ ($\#X=m\wedge\#Y=n$);
• the conclusion that $X\cup Y$ is finite and has its cardinality bounded by $m+n$ corresponds to $\exists p(p\in\mathbb{N}\wedge \#(X\cup Y)=p\wedge p\leq m+n)$, meaning there exists ($\exists p$) a natural number ($p\in\mathbb{N}$) which equals the cardinality of $X\cup Y$ ($\#(X\cup Y)=p$) and is bounded by $\#X+\#Y$ ($p\leq m+n$).