In the meantime, we studied Ehrenfeucht-Fraisse games, finite variable logic, k-pebble games and 0-1 laws. The relevant material is in Libkin’s book, in chapters 3, 11.1, 11.2 and 12.

Now we come back to the study of logics capturing known complexity classes.

**Reminder. **

- IFP=LFP=PTime over linearly ordered finite structures.
- ESO=NP over all finite structures (ESO can guess a linear order)
- TCL=NLogSpace over linearly ordered structures.

What about e.g. LogSpace? We define the logics DTCL and STCL.

## Transitive Closure Logics

**Theorem. **Over linearly ordered structures, DTCL=LogSpace and STCL=SymLogSpace.

SymLogSpace (also called SL) is the class of languages which are log-space reducible to the problem of undirected graph reachability. Equivalently, those are languages accepted by *symmetric *Turing machines.

In 2004 Omar Reingold showed that undirected graph reachability is in LogSpace. This immediately implies the following.

**Theorem. **LogSpace=SymLogSpace.

**Corollary. **Over linearly ordered structures, STCL=DTCL.

The following remains a wide open problem in complexity theory.

**Conjecture. **LogSpace≠NLogSpace. Equivalently, undirected reachability is not decidable in LogSpace.

This equivalent to saying that DTCL≠TCL over linearly ordered finite structures.

The following results show that restricting to linearly ordered structures really makes the problem much more difficult.

**Theorem. (Grädel, McColm) **DTCL⊈TCL over all finite structures.

**Proof.** Excercise.

**Fact. **LFP,IFP⊊ESO over all structures.

$\newcommand{\ll}{\mathcal L^\omega_{\infty,\omega}}$Indeed, ESO can test whether a pure set has even size. Over pure sets, IFP and LFP are hopeless, since $LFP,IFP⊆\ll$ cannot test parity.

# Partial Fixpoint Logic

Consider a relational operator (see this post) $F: P(\str A^k\times Q)\to P(\str A^k\times Q)$. The *partial fixpoint *of $F$ is defined as $F^n(\emptyset)$ if $n$ is such that $F^n(\emptyset)=F^{n+1}(\emptyset)$, and as $\emptyset$ if no such number $n$ exists. Partial Fixpoint Logic (PFP) is the extension of First Order logic by the partial fixpoint operator, which given a formula $\phi$, constructs the partial fixpoint of the relational operator $F_\phi$ (formally, the logic is defined analogously to LFP, but there is no monotonicity restriction, and partial fixpoints are used instead of least fixpoints).

**Theorem. **PFP captures PSpace over linearly ordered structures.

**Corollary 1. **The following conditions are equivalent:

- PFP=ESO over linearly ordered finite structures,
- NP=PSpace.

Observe that whereas ESO⊆PFP over linearly ordered structures (since NP⊆PSpace), ESO⊈PFP over all finite structures, since again evenness of a pure set cannot be expressed in PFP. Indeed, also PFP⊆$\ll.$ Therefore, it is trivial to separate ESO from PFP over all finite structures, although this separation is not the one that would correspond to the conjecture NP⊊PSpace. This also shows that PFP heavily relies on the linear ordering, unlike ESO, which can guess a linear ordering.

**Lemma. **IFP,LFP,PFP⊆$\ll$

**Corollary 2. **The following conditions are equivalent:

- LFP=PFP over linearly ordered finite structures,
- PTime=PSpace.

One could think that it should be easy to separate PFP from LFP over all finite structures, similarly as it was easy to show IFP⊊ESO, DTCL⊊TCL. This is not the case.

**Theorem (Abiteboul-Vianu). ** LFP=PFP over all finite structures if and only if PSpace=PTime.

One direction is easy:

If LFP=PFP then this also holds over linearly ordered structures, and hence PTime=PSpace over words, so also PTime=PSpace as normal complexity classes.

The other direction is more difficult. Assuming that PTime=PSpace, we get that LFP=PFP over linearly ordered structures. We want to prove that PFP⊆LFP over all structures.

Fix a relational signature $\Sigma$ and any number $k$ larger than the maximal arity of the symbols in $\Sigma$.

Consider any formula $\phi$ of PFP over $\Sigma$, which uses $k$ variables. We need to show that $\phi$ is equivalent to some formula of LFP over all structures.

Step 1.

Show that LFP can compare types with respect to the much stronger logic $\ll.$ What does that mean? Note that there are infinitely many types, unlike the types of formulas of bounded quantifier rank. $\newcommand{\llk}{\mathcal L^k_{\infty,\omega}}$

If $\bar a,\bar b$ are two $l$-tuples of elements of some structure $\str A$ and if $k\ge l$, let us write $\bar a\sim_k\bar b$ if they satisfy exactly the same formulas of the infinitary logic $\llk$ with $k$ variables.

**Fact. **The following conditions are equivalent for two $l$-tuples $\bar a,\bar b$ of a structure $\str A$

- $\bar a\sim_k \bar b$,
- $\bar a$ and $\bar b$ satisfy exactly the same formulas of $FO^k$,
- Duplicator wins the $k$-pebble game on $(\str A,\str A)$ with initial configuration $(\bar a,\bar b)$.

**Proposition 1. **For every $k,l$ (with $l\le k$) the relation $\sim_k$ over $l$-tuples is definable in LFP.

## Step 2.

Show that in fact an LFP formula can linearly order the $\sim_k$-equivalence classes of $l$-tuples:

**Proposition 2. **For every $k,l$ (with $l\le k$) there is a linear quasi-order $\preceq_k$ over $l$-tuples which is definable in LFP, and whose equivalence classes are the equivalence classes of $\sim_k$.

## Step 3.

For a given structure $\str A$, using the quasi-linear order $\preceq_k$ define a structure $\str A^*$, which has the following properties:

- Its signature $\Sigma^\ast$ depends only on the signature $\Sigma$
- Its elements are the equivalence classes of $k$-tuples of elements of $\str A$ with respect to $\sim_k$, so they correspond to configurations in the $k$-pebble game, modulo equivalence.
- It is linearly ordered by $\preceq_k$.
- It has unary relations encoding the atomic types of the $k$-types
- It has binary relations $S_1,\ldots,S_j$, where $S_j$ connects $[\bar a]$ with $[\bar b]$ if the tuples $\bar a$ and $\bar b$ only differ on the $j$-th coordinate.

This allows to recover the properties of the original structure $\str A$, so that the following holds.

**Proposition 3. **Any sentence $\phi$ of PFP/LFP using $k$ variables can be converted into a sentence $\phi^*$ of PFP/LFP, so that for all $\str A$,

$$\str A\models \phi\quad\iff\quad \str A^*\models \phi^*.$$

Conversely, any sentence $\psi^*$ of PFP/LFP can be converted into a formula $\hat\psi$ of PFP/LFP so that for all $\str A$,

$$\str A^*\models \psi^*\quad\iff\quad \str A\models \hat\psi.$$

As a side note we remark that is not difficult to show the following.

**Proposition.** $\str A$ and $\str B$ are equivalent with respect to $\llk$ if and only if $\str A^*$ and $\str B^*$ are isomorphic.

Because of this, $\str A^*$ can be seen as a canonical structure with respect to $\llk$-definability.

Let us show how to conclude the proof of the Abiteboul-Vianu theorem.

Suppose that PTime=PSpace and consider a formula $\phi$ of PFP, using $k$ variables. Let be the formula $\phi^*$ of PFP from the last proposition. Since PTime=PSpace, over linearly ordered structures, the formula $\phi^*$ is equivalent to a formula $\psi^*$ of LFP. The formula $\psi^*$ lifts to a formula $\hat\psi$ of LFP. The resulting formula $\hat\psi$ is equivalent to $\phi$ one over any structure $\str A$. This ends the proof of the theorem.