Transforming Nested Fixed-Point Formulas into Infinitary Logic Formulas with Finitely many Variables There is a definition (actually a description of how it could be defined) of a fixed-point logic formula. The formula is in inflationary fixed point logic (IFP) in this case but it could also be written in least fixed point logic (LFP).
I want to transform this formula into a Infinitary Logic Formula with finitely many variables. Infinitary Logic $\mathcal{L}_{\infty \omega}$ is an extension of First Order (FO) Logic which allows conjuction and disjunction over infinite sets of FO formulas.
Given a graph $G=(V,E)$ we want to express whether there is a path between $x$ and $y$ in $\mathcal{L}_{\infty \omega}$. Therefor, we define FO formulas that express whether there is a path of length $n$ in between $x,y$:
$$ \psi^n(x,y) := \exists z_1, \dots, z_n (Exz_1 \land Ez_2z_3\land\dots Ez_{n-1}y)$$
Hence,
$$ \mathrm{path}(x,y) := \bigvee_{n\in\mathbb{N}}\psi_n(x,y)\in\mathcal{L}_{\infty \omega}.$$
It is also possible to express $\psi^n$ with only $3$ distinct variables by reusing the $x$ parameter.
$$ \varphi_1(x,y) := Exy$$
$$ \varphi_n(x,y) := \exists z(Exz \land \exists x (z=x \land \varphi_{n-1}(x,y)))$$
Thus, $\varphi_i \in \mathrm{FO}^3$ forall $i$. Therefore,
$$ \mathrm{path}(x,y) := \bigvee_{n\in\mathbb{N}}\varphi_n(x,y)\in\mathcal{L}_{\infty \omega}^3$$
which is a infinitary logic formula with $3$ distinct variables.
Now for transforming fixed-point logic formulas into infinitary formulas with finite variables there is a general construction (p. 214). With this construction if a fixed point operator is expressed by a $\mathrm{FO}^k$ it can be expressed in $\mathcal{L}_{\infty \omega}^{2k}$. For nested fixed point operators we have to apply the construction twice resulting in $(2k)^2$ variables. I want to define it explicitly with fewer variables. A path formula in LFP or IFP has at least $3$ variables so the general construction would yield $6$ variables for the infinitary formula. However, $ \mathrm{path}(x,y) \in\mathcal{L}_{\infty \omega}^3.$
The formula in IFP itself is technical and big so we will simplify it to the general idea: We want to inductively define a set $W^{\infty}$. $W_0$ is constant dependent on some parameters and 
$$ W_{n+1} := \{ v \in V \mid \textrm{There is a path } \in V \setminus W_n \cup \{v\}\textrm{ from fixed } v_1 \textrm{ to fixed } v_2\}$$
So we need the fixed point operator for the definition of $W_{n+1}$ and a fixed-point operator nested inside for the definition of the path. I try to define it in a $\mathcal{L}_{\infty \omega}^k$ formula in the same manner we defined the second version of $\mathrm{path}$ but I keep running in circles. We can't define the path-formula without refering to $W$ ...
 A: Given a set $W \subseteq V$ depending on two parameters $v_1,v_2$ we assume that we have a formula $\psi_W$ s.t.
$$ v \in W \Leftrightarrow G\models\psi_{W}(v_1,v_2,v).$$
When define
\begin{align*}
\varphi_1(v_1,v_2,v,\psi_W) := &Ev_1v_2, \\
\varphi_n(v_1,v_2,v,\psi_W) := &\exists v'(Ev_1v'~\land~\exists 
v_1(v_1=v'~\land~\varphi_{n-1}(v_1,v_2,v,\psi_W))~\land\\
& v  \neq v'~\land~\forall v''(\psi_W(v_1,v_2,v'')\Rightarrow v'\neq v''),\\
\mathsf{path}(v_1,v_2,v,\psi_W):= & \bigvee_{n\in\omega}\varphi_n(v_1,v_2,v,\psi_W).
\end{align*}
Hence,
$$ G \models \mathsf{path(v_1,v_2,v,\psi_W) \Leftrightarrow } \textrm{ There is a } v_1,v_2\textrm{-Path in } V\setminus W\cup\{v\}.$$
We define the constant $W_0$ with some FO-formular $\psi_{W_0}$. Furthermore, we assume that for $n$ there is formular $\psi_{W_n}$ that describes the set w.r.t. to $v_1,v_2$ in the above mentioned fashion.
\begin{align*}
\psi_{W_{n+1}}(v_1,v_2,v) := \mathsf{path}(v_1,v_2,v,\psi_W)
\end{align*}
Hence, we can define the fixed point $W_\infty$ of the sequence $W_1 \subseteq 
W_2\subseteq\dots W_n = W_{n+1} := W_\infty$ as
\begin{align*}
\mathsf{winfty}(v_1,v_2,v) := \bigvee_{n\in\omega}\psi_{W_n}(v_1,v_2,v) \in \mathcal{L}_{\infty\omega}^5.
\end{align*}
