No hay una definición (en realidad, una descripción de cómo se podría definir) de un punto fijo la fórmula de la lógica. La fórmula está en inflacionario punto fijo de la lógica (IFP) en este caso, pero también se podría haber escrito en menos de punto fijo de la lógica (LFP).
Quiero transformar esta fórmula en un Infinitary la Fórmula de la Lógica con un número finito de variables. Infinitary Lógica de $\mathcal{L}_{\infty \omega}$ es una extensión de Primer Orden (FO) de la Lógica que permite la conjunción y la disyunción sobre conjuntos infinitos de FO fórmulas.
Dado un grafo $G=(V,E)$ queremos expresar si existe un camino entre el$x$$y$$\mathcal{L}_{\infty \omega}$. Para ello, definimos FO fórmulas que expresan si existe un camino de longitud $n$ entre $x,y$:
$$ \psi^n(x,y) := \exists z_1, \dots, z_n (Exz_1 \land Ez_2z_3\land\dots Ez_{n-1}y)$$
Por lo tanto,
$$ \mathrm{path}(x,y) := \bigvee_{n\in\mathbb{N}}\psi_n(x,y)\in\mathcal{L}_{\infty \omega}.$$
También es posible expresar $\psi^n$ sólo con $3$ distintas variables mediante la reutilización de la $x$ parámetro.
$$ \varphi_1(x,y) := Exy$$ $$ \varphi_n(x,y) := \exists z(Exz \land \exists x (z=x \land \varphi_{n-1}(x,y)))$$
Por lo tanto, $\varphi_i \in \mathrm{FO}^3$ forall $i$. Por lo tanto,
$$ \mathrm{path}(x,y) := \bigvee_{n\in\mathbb{N}}\varphi_n(x,y)\in\mathcal{L}_{\infty \omega}^3$$
que es un infinitary la fórmula de la lógica con $3$ variables distintas.
Ahora para la transformación de punto fijo fórmulas lógicas en infinitary fórmulas con finito de variables existe una construcción en general (p. 214). Con esta construcción, si un punto fijo del operador se expresa por una $\mathrm{FO}^k$ puede ser expresado en $\mathcal{L}_{\infty \omega}^{2k}$. Para anidada punto fijo operadores tenemos que aplicar la construcción de dos veces resultando en $(2k)^2$ variables. Quiero definir explícitamente con menos variables. Una ruta de acceso de la fórmula en la LFP o IFP tiene al menos $3$ variables para la construcción en general daría $6$ variables para el infinitary fórmula. Sin embargo, $ \mathrm{path}(x,y) \in\mathcal{L}_{\infty \omega}^3.$
La fórmula de la IFP en sí es técnica y grandes así que vamos a simplificar a la idea general: queremos definir un conjunto inductivo $W^{\infty}$. $W_0$ es constante, depende de algunos parámetros y
$$ 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\}$$
Así que tenemos el punto fijo del operador para la definición de $W_{n+1}$, y en un punto fijo del operador anidada dentro de la definición de la ruta de acceso. Trato de definir en un $\mathcal{L}_{\infty \omega}^k$ formula de la misma manera que hemos definido de la segunda versión de $\mathrm{path}$ pero sigo corriendo en círculos. No podemos definir la ruta de acceso de la fórmula sin que se referirá a $W$ ...
