Formulating that the universe is finite without establishing an upper limit

Question

There is a fairly common example of a 2nd order formula that is only true in a universe with infinite domain:

$$\begin{align} \exists R \quad & \forall x && \lnot xRx \\ \land & \forall x \exists y && x R y \\ \land & \forall x \forall y && x R y \implies \lnot y R x \\ \land & \forall x \forall y \forall z && x R y \land y R z \implies x R z \\ \end{align}$$

And it is fairly easy to establish a formula that is only true in a finite universe:

$$\exists x \forall y~ x = y$$

which has only 1 element in the universe, or

$$\exists x_1 \exists x_2 \forall y ~x_1 = y \lor x_2 = y$$

which has no more than 2 elements in the universe. Is there a formula that only holds when the universe is finite without putting an upper finite limit on its size? In other words, it would be consistent with any formula of the form $\exists x_1 \dots \exists x_n \forall y ~ x_1 = y \lor \dots \lor x_n = y$ ? I would be interested even if the formula was a higher order (quantified over relations or functions) formula; however, I am mostly interested in formulas with no free variables and no unquantified constants.

Answer 1

The logical predicate $S$ forms a "finite system" if and only if:

$$\begin{array} {rl} % \forall F ~:~ & \left(\begin{array} {rrrl} % & \forall a,~ b ~:~ & F(a,~ b) & \implies S(a) \land S(b) \\ \land & \forall a ~:~ & S(a) & \implies \exists b ~:~ (S(b) \land F(a,~ b)) \\ \land & \forall a,~ b,~ c ~:~ & F(a,~ b) \land F(a,~ c) & \implies b=c \\ \land & \forall a,~ b,~ c ~:~ & F(a,~ b) \land F(c,~ b) & \implies a=c \\ \implies & \forall a ~:~ & S(a) & \implies \exists b ~:~ (S(b) \land F(b,~ a)) \\ % \end{array}\right)\end{array}$$

You might think of this as the second-order predicate logic version of Dedekind finite, with $F$ being a kind of "mapping" from $S$ to $S$.

Answer 2

The answer is negative. It is a well-known theorem (see for example here) that the class of all finite structures is not elementary, i.e. there is not first-order theory $T$ such that its models are all and only the finite structures.

This is a typical example of the limits of the expressive power of first-order logic with respect to second-order logic.

Answer 3

As remarked above, there is no first-order sentence which will do the job. On the other hand, we can get second-order examples; the negation of the sentence at the beginning of your post, or Dan Christensen's example, will both do the job.

. . . Unless the axiom of choice fails!

WAIT, WHAT?

So here's the deal: consider the second-order sentence "There is an injection from the universe to itself which is not a surjection." (This is basically the sentence from Dan's answer.) It is not the case that this sentence is true in every infinite universe, if the axiom of choice fails! It is consistent that there are infinite Dedekind-finite sets - infinite sets with no non-surjective self-injections. (It can get worse - there can be amorphous sets, which are infinite sets which cannot be partitioned into two infinite subsets!)

These "quasi-finite" sets might make you worry: is there a second-order sentence which characterizes exactly the finite sets, without any choice?

The answer, luckily, is yes: a set $X$ is finite iff there is a binary relation $R$ on $X$ such that:

• $R$ is a linear order - that is, transitivity, reflexivity, totality, and antisymmetry hold;

• $R$ has a first and last element, and every non-last element has a successor; and

• every surjective map from $X$ to itself is injective.

Clearly any finite set satisfies the above. Meanwhile, if a set $X$ existed which was not finite but satisfied the above, we could consider the subset $Y$ of $X$ consisting of all the elements of $X$ reachable by applying "successor" to the first element of $X$ finitely many times. If $X$ is infinite, then $Y$ has order type $\omega$, and so we can apply the usual "Hilbert's Hotel" argument.

It is a good exercise to express the definition of finiteness given above in second-order logic.