Cardinality of the set of formulas of a first-order language I know that every first-order language contains endless terms since it contains in particular a countable infinite amount of variables.
Are there always endless many formulas in a first-order language? More precisely, what is the cardinality of the set of formulas of a first-order language?
 A: Yes - for example, for any $n$ the expression $$\forall x(x=x\wedge x=x\wedge ...\wedge x=x\mbox{ ($n$ times)})$$ is a formula (indeed, a sentence).
Of course, this is a bit silly since all the resulting sentences are equivalent to each other; we can do much better. One important example is the following: for each $n$ consider the sentence $$\psi_n\equiv\exists x_1,...,x_n[(\bigwedge_{1\le i<j\le n}x_i\not=x_j)\wedge\forall y(\bigvee_{1\le k\le n}y=x_k)].$$ For each $n$, the sentence $\psi_n$ says "There are exactly $n$ many elements in the universe."

Note that all of this works over the empty language (= no non-logical symbols, only variables, Booleans, quantifiers, equality, and parentheses). In general, the set of first-order formulas over a language of cardinality $\kappa$ has cardinality $\max\{\aleph_0,\kappa\}$.
The above does, however, require an infinite collection of variables. If we have a single unary function symbol $f$ on hand, we only need one variable to get infinitely many inequivalent sentences: consider $$\theta_n\equiv \forall x(f(f(...(f(x))...))=x\mbox{ $n$ times}).$$
EDIT: one can reasonably ask what happens if we only have relation symbols and finitely many variables. Here we run into an interesting syntactic issue: how we treat "rebinding" of variables suddenly matters. 


*

*If we disallow "rebinding" of variables (e.g. $\forall x(...\exists x(...))$, where we "reset" the role of $x$ once we hit the $\exists$), then from finitely many variables and relation symbols we can only produce finitely many formulas up to logical equivalence. 

*If we allow rebinding however, then things are messier: for example, in the language with a single binary relation symbol $E$ we can write for each $n$ a formula $\varphi_n(x,y)$ which says "$x$ and $y$ have $E$-distance $n$." Specifically, we set $\varphi_0(x,y)$ to be $x=y$, set $\varphi_1(x,y)$ to be $E(x,y)\wedge x\not=y,$ and for $n>0$ set $\varphi_{n+1}(x,y)$ to be $$\exists z(E(x,z)\wedge\exists x(z=x\wedge\varphi_n(x,y)))$$ (note the crucial "reuse" of $x$). So here we get infinitely many inequivalent formulas from just three variables and one binary relation! Finite-variable logics have a lot of hidden subtlety, and the example above is taken from Libkin's book on finite model theory.
