How it can be formally proved that a formula of First Order Logic with identity has only infinite models?

Question

I have an irreflexive and transitive relation $R$. Then I want to prove that $\forall x \exists y (xRy)$ has only infinite models. I have an intuitive idea for which the relation $R$ cannot be reflexive (cause transitivity + symmetry implies reflexivity), then we know that everything is not related to everything. In this sense we cannot have a closed circle of relation and clearly there it must be an element of the domain such that there is nothing else that is related to it. We could then add another element but the same reasoning still apply.

How can I prove this formally?

Answer 1

The language includes equality, right? So show that there exist $x_1,x_2$ with $x_1\ne x_2$. Then show that there exist $x_1,x_2,x_3$ with $x_1\ne x_2$, $x_1\ne x_3$ and $x_2\ne x_3$.

For every $n$ there is a $\phi_n$ that says "there exist at least $n$ things". Show by induction that each $\phi_n$ is provable from your axioms.

Answer 2

Nitpick: The empty structure is a model of your axioms. But I'll assume you're working with the convention that all first-order structures are non-empty.

Try proving by induction on $n$ that in any model $M$, there is a chain $a_1,a_2,\dots,a_n$ of distinct elements such that $a_i R a_{i+1}$ for all $1\leq i < n$. Note that non-emptyness is required for the base case $n=1$!

Answer 3

Suppose $(M, <)$ is a model of your theory "R is irreflexive", "R is transitive", and $\forall x \exists y \: xRy$.

Because $M \models \forall x \exists y xRy$, for every $x \in M$ there's a $y \in M$ for which $x < y$. Using the principle of countable Dependent Choice, we can define a sequence $(a_n)_{n \in \mathbb{N}}$ as follows:

Let $a_0$ be any element of $M$;

given $a_n$, let $a_{n+1}$ be some element in $M$ for which $a_n < a_{n+1}$.

Note: by convention, even by many people's definition, models are nonempty. If your definition allows empty models (I assume it doesn't), then there's an empty model of your theory too. In any case, let's assume $M$ is nonempty,so that $a_0$ can be chosen.

By induction, using transitivity of $<$, $$ n < m \implies a_n < a_m \;\;\;\;\;\text{for $n, m \in \mathbb{N}$} $$ and then by irreflexivity of $<$, all the $a_n$ are distinct.