202504210004

Tags : Finite Model Theory

Stages

---

Fixed Point Logics compute sets by using a formula to describe an operator on the collection of subsets of the universe, which is applied on the empty set repeatedly until a fixed point is reached.

We now define a way to compare when different points of the universe enter the set defined using the fixed point operator, more specifically.

Consider a formula $\phi (R,\vec{x})$ such that all occurrences of $R$ are positive in $\phi$, hence it defines a monotone operator. Since we are working with finite models, $F_{\phi }$ reaches its fixed point after finitely many steps which we define to be $|\phi |$.

We now define a stage of a point as follows:

Definition

The stage of a point $x$ is the number $i$ such that $x\in X_i$ and $x\notin X_{i-1}$. This is generally written as $|x|$

Since $F_{\phi }$ reaches its fixed point after $|\phi |$ steps, for each point $x$ in the fixed point, we have that $|x|\le |\phi |$, hence for all points $y$ outside the fixed point we define the stage $|y|=|\phi |+1$.

We now define the operators $\prec$ and $⪯$ that compare the stages of points:

$$\begin{array}{rl}\vec{x}\prec \vec{y}& \equiv |\vec{x}{|}_{\phi }^{\mathfrak{A}}<|\vec{y}{|}_{\phi }^{\mathfrak{A}}\\ \vec{x}⪯\vec{y}& \equiv |\vec{x}{|}_{\phi }^{\mathfrak{A}}\le |\vec{y}{|}_{\phi }^{\mathfrak{A}}\text{ and }|\vec{x}{|}_{\phi }^{\mathfrak{A}}\le |\phi {|}^{\mathfrak{A}}\end{array}$$

The following extra operators need to be defined that will all be constructed simultaneously

$$\begin{array}{rl}\vec{x}\nprec \vec{y}& \equiv |\vec{x}{|}_{\phi }^{\mathfrak{A}}\ge |\vec{y}{|}_{\phi }^{\mathfrak{A}}\\ \vec{x}/⪯\vec{y}& \equiv |\vec{x}{|}_{\phi }^{\mathfrak{A}}>|\vec{y}{|}_{\phi }^{\mathfrak{A}}\text{ or }|\vec{x}{|}_{\phi }^{\mathfrak{A}}=|\phi {|}^{\mathfrak{A}}+1\end{array}$$

and

$$\vec{x}◃\vec{y}\equiv |\vec{x}{|}_{\phi }^{\mathfrak{A}}+1=|\vec{y}{|}_{\phi }^{\mathfrak{A}}$$

---

References