# 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$ ...

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*}