The class of connected graphs is not first-order axiomatizable 1. Context
I was given the following exercise:

Prove or disprove:
There is no first-order theory $\phi$ such that for all graphs $\mathfrak{G}$: $\mathfrak{G} \models \phi$ if and only if $\mathfrak{G}$ is connected.

That the class of connected graphs is not first-order axiomatizable in the language of graphs can be shown using the compactness theorem (For a proof see here.)
However, my tutor proposed the following basic first order axiomatization of connected graphs:
$$
\begin{split}
\forall x, y \in V (\exists f(f: \omega \to V (\exists n (\forall m > n (f(m)=z) 
&\land \forall m \leq n (f(m) \in V) \\
&\land f(0)=x \\
&\land f(n)=y \\
&\land \forall n>k( (f(k), f(k+1))\in E)))))
\end{split}
$$
2. Question

*

*Is this a first-order axiomatization of connected graphs?

Of course it is not even a well-formed formula.
Furthermore, my tutor didn't give the language they were using. The proof I refer to above works within the language of graphs, i.e. the language with signature $\{R\}$ and $R$ a 2-ary relation symbol. The sentence proposed by my tutor uses a different one. Is the class of graphs first-order axiomatizable in that language (whatever language that is)? What about connected graphs?
 A: $\S 1$. The class of connected graphs is not axiomatizable in first-order logic
As stated in the question, it is well known that the class of graphs is not first-order axiomatizable in the language of graphs. But what if we add more to the language? In other words, suppose $L$ is a first-order language containing a binary relation $R$ (for graphs), but possibly more. Can we construct an $L$-theory $T$ so that the models of $T$ are precisely connected graphs? Since $L$ contains other symbols, we have to say precisely what is meant by "a model of $T$ is a connected graph". The most natural meaning is: "if we take a model of $T$ and forget about all of the first-order structure except the interpretation of $R$, then we get a connected graph". Let's denote this process like this: If $A$ is an $L$-structure then $A{\upharpoonright}R$ is the $\{R\}$-structure obtained by only looking at the interpretation of $R$ (this is sometimes called a reduct). So the most natural way to understand the question is:

Is there an $L$-theory $T$ such that $\{A{\upharpoonright}R:A\models T\}$ is precisely the class of connected graphs?

So now that we have a precise question, I'll show that that there is no such theory $T$. The proof is basically the same. Suppose such a theory $T$ exists. Add two new constants $a,b$ to $L$, which produces a bigger languge $L'$. For any $n\geq 1$, let $\varphi_n$ be the $L'$-sentence saying there is no path from $a$ to $b$ of length at most $n$. Let $T'=T\cup\{\varphi_n:n\geq 1\}$. By our assumption, any finite subset of $T'$ has a model. To see this, fix $n\geq 1$. Consider the graph $G$ which is a path of length $n$. Then by our assumption there is $A\models T$ such that $A{\upharpoonright}R=G_n$. Make $A$ into an $L'$-structure $A'$ by interpreting $a$ and $b$ as the endpoints. Then $A'\models T\cup\{\varphi_k:k<n\}$.
Now, by the Compactness Theorem for First-Order Logic, $T'$ has a model $B$. So $B{\upharpoonright}R$ is not a connected graph, as witnessed by the interpretations of $a$ and $b$. But $B{\upharpoonright}L\models T$, which contradicts our assumptions.
$\S 2$. A failed attempt
Next I will make an attempt to formalize your tutor's idea, and see why it fails. As motivation, let's first observe a more obvious failed attempt at axiomatizing connected graphs:
$$
\forall x\forall y\bigg(x\neq y\rightarrow \exists n\geq 1\,\exists z_1\ldots z_n\big(x=z_1\wedge y=z_n\wedge \bigwedge_{k<n}R(y_k,y_{k+1})\big)\bigg)
$$
Although this sentence describes connectivity, it is not a first-order sentence because we have quantified over the number of variables used in the sentence, which is a no-no. What your tutor has done is try to disguise this quantification by viewing natural numbers as elements themselves and lists of variables as images of functions from natural numbers. But we have to make this rigorous, and the most natural way to do it is with sorts.
Let $L$ be a language with three sorts $V$, $N$, and $F$. I think of $V$ as the sort for vertices of graphs, $N$ as a sort for the natural numbers, and $F$ as a sort for functions from $N$ to $V$. In $L$ I have a binary relation $R$ on the $V$ sort (which I think of as the graph relation), a constant symbol $0$ in the $N$ sort (which I think of as the number $0$), a binary relation $<$ on the $N$ sort (which I think of as the ordering), and a unary function $s$ on the $N$ sort (which I think of as the successor function).
Side remark: The three sorts are motivated by the objects your tutor has attempted to quantify over: vertices, natural numbers, and functions from vertices to natural numbers. Part of the rules of first-order logic require that quantifiers only quantify over elements of structures, not higher order things like subsets and functions, or meta-things like natural numbers. So anything we want to quantify over has to be given a sort.
Let us continue. I will now write down a variation of the proposed axiom that looks like it will describe connected graphs. It's basically the same as what your tutor wrote, but I omit the confusing and/or superfluous parts. In the following sentence, $x,y$ are variables in the $V$ sort, $f$ is in the $F$ sort, and $k,n$ in the $N$ sort (I'm omitting the specification of this in the sentence itself to make things easier to read).
$$
\forall x \forall y \bigg(x\neq y\rightarrow \exists f \exists n \big(f(0)=x\wedge f(n)=y\wedge \forall k(0\leq k<n\rightarrow R(f(k),f(s(k)))\big)\bigg)
$$
So does it work? We might be optimistic since certainly I can take any connected graph and turn it into an $L$-structure satisfying this sentence. Specifically, let $G$ be a connected graph and consider the $L$-structure $A$ where $(V,R)$ is interpreted as $G$, $(N,<,0)$ is interpreted as $(\omega,<,0)$, and $F$ as all functions from $\omega$ to the vertex set of $G$. For any distinct $x$, $y$ in $G$, there is a path from $x$ to $y$, and so there is a function as in the sentence above.
The problem is the other direction, and the main point is that $(N,<,0)$ doesn't have to be interpreted as $(\omega,<,0)$. This is what I mean by saying "you can't quantify over natural numbers". You can quantify over elements that you might think are natural numbers in some structure, but not necessarily in others. For example, consider the graph $G$ that looks like two disjoint copies of $\mathbb{N}$ and edges between any element and its successor. This graph is disconnected but I can make it into an $L$-structure satisfying the sentence above. Interpret $(V,R)$ as $G$, and $(N,<,0)$ as the order $\omega+\omega^*$ (i.e., $\omega$ followed by $\omega$ in reverse order) with $0$ interpreted as the least element. $F$ is the set of functions from $\omega+\omega^*$ to the vertices in $G$.  For any distinct vertices $x$ and $y$, I can find a function as above. If $x$ and $y$ are in the same copy of $\mathbb{N}$ then it's easy. On the other hand, if they are in different copies then send $\omega$ to the interval $[x,\infty)$ and send $\omega^*$ to $[y,\infty)$.
Side Remark. There are dumber ways to show that the sentence above won't work because it doesn't specify anything about $R$ being a graph relation, or $<$ being a linear order, etc, etc, etc. So you can add all of this in, and the same counterexample goes through. You might try to add more axioms or more symbols to try to "force" the interpretation of $(N,<)$ to be $\omega$. But it won't work and $\S 1$ proves it.
