We have a graph as a structure and $2$ constants in our signature, $\tau = (E^2, s^0, t^0)$.
I have to create a formula for every even $k$ such that there is a path with length $k$ from $s$ to $t$, the formula shouldn't have more than $2$ variables.
I guess it would already help a lot to get a formula for $k = 4$, then I can try to generalize it myself. The only thing I have so far is $∃a∃b∃c(¬a = b ∧ ¬a = c ∧ ¬b = c ∧ E(s, a) ∧ E(a, b)∧ E(b, c) ∧ E(c,t))$, this has $3$ variables and doesn't seem useful at all. I don't even know if I'm supposed to use the constants that way. I guess an idea could be to look at a vertex and check if it has an incoming and outgoing edge and then you go to a different vertex and check if it's connected with the other vertex and so on. But I don't know how to do that. And then you could perhaps do something with cardinality ∃a∃b∃c(¬a = b ∧ ¬a = c ∧ ¬b = c ∧ ∀x(x = a ∨ x = b ∨ x = c)), not sure if that helps at all.
I believe the trick is that you can reuse the variables. According to the usual rules of the predicate calculus, if an occurrence of a variable is bound by an "inner" quantifier, then an "outer" quantifier doesn't bind it---the occurrence is "invisible" to the outer quantifier.
Using this, here's a formula insuring a path from $s$ to $t$ of length at most 4.
$$\exists x(E(s,x)\wedge\exists y(E(x,y)\wedge\exists x(E(y,x)\wedge\exists y(y,t))))$$
As for exactly length 4: well, the above guarantees a path of length 4, just not without repeated nodes and edges. If that's also a requirement, then I'm out of ideas.
Of course, reusing variables like this is a bad idea from a readability standpoint.