How to express this statement in a first order language

Question

Let $L$ be a first order language with no non-logical symbols.

For each $n\in\Bbb{N}$ explain how to express the following in L

"There are at least $n$ elements in the domain"

So my intial thinking was:

$\exists x_1 \exists x_2 ... \exists x_n (\neg(x_1=x_2)\wedge\neg(x_1=x_3)\wedge...allPossiblePairs)$

This seems abit messy can anyone suggest something tidier

Answer 1

What you describe can generally be considered the "standard" straightforward solution. However, you can get a shorter formula (with only $O(n)$ symbols rather than $\Omega(n^2)$ symbols) by using a trick: First express

There are at most $k$ elements in the domain

as

$$ \exists x_1 \cdots \exists x_k \forall y ( y=x_1 \lor \cdots \lor y=x_k ) $$

Negating this produces a formula for "There are at least $k+1$ elements in the domain":

$$ \forall x_1 \cdots \forall x_k \exists y ( y\neq x_1 \land \cdots \land y\neq x_k ) $$