# How to express this statement in a first order language

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

• This is perfectly correct. – J.-E. Pin Mar 14 '16 at 13:59
• Ok thanks, do the $\exists$ symbols need any sort of bracketing do you think? – Connor Bishop Mar 14 '16 at 14:06
• @ConnorBishop: Depends on which conventions are used in the course/book you're following. Some authors prefer to put brackets around the quantifier, others put brackets around the formula it applies to; yet others use no brackets but a dot instead. – Henning Makholm Mar 14 '16 at 14:09

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
$$\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 )$$