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

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?

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

• Models in model theory are nonempty, and first order logic assumes a nonempty universe :) Accommodating the empty universe is easy, but it's a triviality and an added nuisance. – BrianO Oct 14 '15 at 21:01
• @BrianO This is not a universal convention. For example, Hodges' well-known book Model Theory allows empty structures (quite rightly, in my view). – Alex Kruckman Oct 14 '15 at 21:06
• I didn't realize that Hodges allows it. Chang-Kiesler and others don't. Hodges can't devote much time talking about it, as there's nothing to say: $\vdash \exists x (p \vee \neg p)$ is a theorem of first order logic, so empty models ... have certain shortcomings. – BrianO Oct 14 '15 at 21:10
• @Alex With n=1 I would have only one element.. right? then how can I saturate a two place predicate? And does such a prove by induction rule out all the (im)possible finite models? The fact is that no finite domain would be a model of that. Correct? – Spike Spiegel Oct 14 '15 at 21:32
• @BrianO Well, $\exists x\, \top$ is a theorem of first-order logic when it's set up for a semantics that rules out empty structures. It's also possible to give a proof system (a slightly less elegant one, it's true) with all the usual nice properties for a semantics that includes empty structures. Hodges (and most every other model theory book I know except Chang & Keisler) sidesteps this whole issue by not even mentioning first-order proofs. This is model theory, after all... – Alex Kruckman Oct 15 '15 at 0:03

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.

• Yes the language has to include equality because "R is irreflexive" can be expressed in it :) – BrianO Oct 14 '15 at 21:07

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.