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.

  • 2
    $\begingroup$ Can't you just negate your first formula? $\endgroup$ – martini Dec 10 '15 at 16:25
  • 1
    $\begingroup$ @martini I guess you could if you assume "every possible relation exists". The first relation isn't equivalent to "the universe is infinite", it just implies that. $\endgroup$ – DanielV Dec 10 '15 at 16:29
  • 1
    $\begingroup$ Finiteness is not a first-order property. The following may help: math.stackexchange.com/questions/1222319/… math.stackexchange.com/questions/894/… $\endgroup$ – Amir.H Kiani Dec 10 '15 at 16:45
  • 2
    $\begingroup$ Just negate the existence of surjective non injective functional relations. $\endgroup$ – nombre Dec 10 '15 at 16:51
  • 1
    $\begingroup$ @DanielV I think your sentence is equivalent to "the universe is infinite", at least assuming the axiom of choice . . . $\endgroup$ – Noah Schweber Dec 11 '15 at 6:39

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$.

  • $\begingroup$ You can turn this into a second-order sentence asserting that the domain is finite - that is, $\exists S \exists F . . . $" - but you cannot do this in a first-order manner. Along these lines, note that there are infinite $\{S, F\}$-structures which do not satisfy your sentence - for instance, interpret $F$ and $S$ as the emptyset. $\endgroup$ – Noah Schweber Dec 11 '15 at 5:46
  • $\begingroup$ @NoahSchweber Non-empty F now assured by $\exists a,b: F(a,b)$. Non-empty S then assured by next line, $\forall a,b: [F(a,b) \implies S(a) \land S(b)]$ $\endgroup$ – Dan Christensen Dec 11 '15 at 6:00
  • $\begingroup$ You're missing my point - I was giving an example of a structure which does not satisfy your sentence. My point is, there is no first order sentence $\varphi$ in any language $L$ which is true in exactly the infinite $L$-structures. (Actually, I was misreading your sentence in my previous comment - I thought you did include an axiom saying $F$ was nonempty.) $\endgroup$ – Noah Schweber Dec 11 '15 at 6:31
  • 1
    $\begingroup$ The proof of this is a straightforward application of compactness - consider the theory $T$ which is $\neg \varphi$ together with the sentences "there are at least $n$ elements" for every $n\in\mathbb{N}$. $\endgroup$ – Noah Schweber Dec 11 '15 at 6:32
  • $\begingroup$ @NoahSchweber See changes $\endgroup$ – Dan Christensen Dec 11 '15 at 6:35

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.

  • $\begingroup$ Theorem: If a theory has arbitrarily large finite models ,it has an infinite model. So if a theory has no infinite model there must be an upper bound on the size off the model. This does not mean however that the value of the l.u.b. is decidable. $\endgroup$ – DanielWainfleet Dec 10 '15 at 17:59
  • $\begingroup$ @user254665 Actually, for finite theories this is decidable: if there is a model of size $n$, we can find it, and if there is no model of size $\ge m$, then the theory proves the sentence "there is no model of size $\ge m$." So there is a Turing machine $\Phi$ such that, if $T$ is (a real coding) a finite theory with no infinite models, $\Phi^T(0)$ is the sup of the sizes of the models of $T$. $\endgroup$ – Noah Schweber Dec 11 '15 at 5:48
  • $\begingroup$ Note that the restriction to finite theories is necessary: we can find a computable function $f$ from numbers to theories such that (1) $f(n)$ never has a model of size $\ge 3$, and (2) $f(n)$ has a model of size $2$ iff $n$ is in the Halting Problem. The finiteness assumption is used in my claim that "if there is a model of size $n$, we can find it" - checking whether a single sentence holds in a finite model is recursive. $\endgroup$ – Noah Schweber Dec 11 '15 at 5:50

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!


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.

  • $\begingroup$ Note the shift here: the other definitions of finiteness are of the form "there is no function such that . . . " whereas this one is of the form "there is some function such that . . ." $\endgroup$ – Noah Schweber Dec 11 '15 at 6:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.