Directed cycles - logic first order sentence with three variables - proof of existence some sentence

Question

Let $C$ denotes directed cycles over sygnature consisting of one relational symbol $E(x,y)$ - there exists directed edge from $x$ to $y$.

Prove that for each natural $n$ there exists first order formula $\phi_n$ such that it contains only three variables (we can arbitraly requantify them), such that for each finite directed cycle $C$ we have: $C,x:a,y:b,z:c\models \phi_n(x,y,z) \Leftrightarrow C$ has $3n$ edges and directed distances: $d(a,b)=d(b,c)=d(c,a)=n$.

First of all I can't how to start. I have no idea what denotes $x:a$. $x=a$ ? $a,b,c$ are fixed ? The second thing is that I have never so far prove existence of formula, what makes this exercise undoable for me. However I think that this one may be very informative. Can you help me, please ?

Answer 1

I think that the symbol :

$C,x:a,y:b,z:c \vDash \varphi_n(x,y,z)$

means that the directed cycle $C$ with vertex $a,b,c$ satisfy the formula $\varphi_n(x,y,z)$ when we assign to the variables : $x, y, z$ respectively the denotations : $a, b, c$.

A more "usual" notation for the satisfaction in a structure $\mathcal M$ of a formula $\varphi$ with free variables : $x_1, \ldots, x_n$ would be :

$\mathcal M \vDash \varphi [a_1, \ldots, a_n]$.

Answer 2

The meaning of $$ C,x : a,\, y:b,\, z:c \models \varphi_n(x,y,z) $$ is the one suggested by @MauroALLEGRANZA.

A formula of $\mathsf{FO}^k$ uses no more than $k$ variables. We first describe a formula $\psi_n(x,y)$ of $\mathsf{FO}^3$ that claims the existence of a path of length $n$ between $x$ and $y$. The formula is defined inductively. We let $\psi_1(x,y) := E(x,y)$, and, for $n>0$,

$$ \psi_{n+1}(x,y) := (\exists z \,.\, E(x,z) \wedge \exists x \,.\, x = z \wedge \psi_n(x,y)) \enspace. $$

(This re-use of $x$ is a standard trick in the study of logics with finitely many variables.)

Finally, we write,

$$ \varphi_n(x,y,z) := \psi_n(x,y) \wedge \psi_n(y,z) \wedge \psi_n(z,x) \enspace. $$

Note that this scheme does not extend to the case of four or more equidistant vertices on a cycle.