5
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.