$\mathfrak{A} \models \phi \iff |A| = n$ for any $n$.

Question

For any $n$ write a such formula $\phi$ that $$\mathfrak{A} \models \phi \iff |A| = n$$

My solution: $$\phi = (\exists a_n \in A \wedge \exists a_{n-1} \in A \setminus \{a_n\} \wedge ... \wedge \exists a_1 \in A \setminus \{a_n, ..., a_2\} \neg \exists a \ a \in A \setminus \{a_n, .., a_1\} )$$

Is it correct?

Answer 1

It expresses the right idea, but it isn’t correct if you’re supposed to find a formula in first-order logic with equality: quite apart from anything else, the underlying set $A$ isn’t available to you in the formal language. You need to say something like this:

$$\exists x_1\,\exists x_2\,\ldots\,\exists x_n\,\forall x_{n+1}\,\left(\bigwedge_{1\le k<\ell\le n}\neg(x_k=x_\ell)\land\bigvee_{1\le k\le n}(x_{n+1}=x_k)\right)\;.$$

The big conjunction is an abbreviation for

$$\begin{align*} &\neg(x_1=x_2)\land\neg(x_1=x_3)\land\ldots\land\neg(x_1=x_n)\\ &\qquad\land\neg(x_2=x_3)\land\neg(x_2=x_4)\land\ldots\land\neg(x_2=x_n)\\ &\qquad\;\vdots\\ &\qquad\land\neg(x_{n-1}=x_n)\;, \end{align*}$$

and the big disjunction works is a similar abbreviation.

It may be intuitively more appealing to move the universal quantifier immediately in front of the big disjunction:

$$\exists x_1\,\exists x_2\,\ldots\,\exists x_n\,\left(\bigwedge_{1\le k<\ell\le n}\neg(x_k=x_\ell)\land\forall x_{n+1}\,\left(\bigvee_{1\le k\le n}(x_{n+1}=x_k)\right)\right)\;.$$

This is equivalent to the other version.