FMT 5: the CFI theorem

Recall the following result from this post.

Theorem (Immerman-Vardi).  Over linearly-ordered, finite structures, IFP is equally expressive as PTime.

In this post we will prove the theorem of Cai, Fürer and Immerman that the above result does not extend to the class of all finite structures. Using a geometric argument, we show that the logic IFP+C cannot determine solvability of systems of linear equations modulo $2$.

The Immerman-Vardi theorem does not hold for all finite structures for a very silly reason: IFP cannot determine whether a pure set has even cardinality (this follows from the Ehrenfeucht-Fraisse game for $\Ll^k_{\omega,\infty}$, i.e., the $k$-pebble game). Because of that, it is at least necessary to extend IFP by the possibility of counting.

The logic IFP+C

The logic IFP+C is an extension of the logic IFP which allows to count, up to a polynomial threshold. For a finite structure $\str S$ with $n$ elements, let $[\str S]$ denote the structure whose universe are the elements $0,1,\ldots,n-1$, and which is equipped with two binary predicates: the linear order $\le$ and the successor relation $\textit{succ}$, whose symbols are distinct from the symbols used in $\str S$. By $\str S+[\str S]$ we denote the two-sorted structure, extending $\str S$ – whose elements are called nodes – by the counting sort $[\str S]$, whose elements are called numbers. If $\phi$ is a formula and $\bar x=(x_1,\ldots,x_k)$ are some of its free variable ranging over nodes and $i\in\NN$ then $\#_i\bar x.\phi$ is the element of the counting sort which is the $i$-th digit of the number of tuples $\bar x$ of $\str S$ which satisfy the formula $\phi$, in the base-$n$ encoding, where $n$ is the cardinality of $\str S$.

The syntax of IFP+C is defined by extending the syntax of IFP by the counting construct $\#_i\bar x.\phi$, and also allowing to use the relations $\le$ and $\textit{succ}$. To interpret such a formula over a structure $\str S$ means to interpret it over $\str S+[\str S]$, where the interpretation of the counting construct, the linear order and successor relation are as described above.

Example. To determine whether a pure set $X$ has even cardinality, we use a formula $\psi$ of IFP which holds in a linearly ordered structure if and only if it has even cardinality. The existence of such a formula follows from the Immerman-Vardi theorem, since parity is in PTime. It is also easy to explicitly write such a formula, by incrementally extending a unary predicate adding every second element. With the help of the formula $\psi$, we may define a formula of IFP+C which determines whether a pure set has even cardinality – it suffices to relativise $\psi$ to elements ranging over the counting sort. Note that the elements of the counting sort are the only ones that satisfy the relation $x\le x$. We haven’t even used the counting construct – only the counting sort was used for determining the parity. Indeed, in case $\str S$ is a pure set, the counting sort $[\str S]$ is simply a richer version of $\str S$, endowed additionally with the linear order, so in this case it makes sense to work directly with $[\str S]$.

In a similar fashion, one can define any PTime-computable query of pure sets using IFP+C.

Example. We describe an IFP+C formula which computes the radius of a given graph $G$, i.e. the minimal value $r$ such that there exists a node $v\in G$ whose $r$-neighbourhood contains all of $G$. To this end, using IFP we define a binary relation $D(u,v,r)$, where $v$ ranges over nodes and $r$ ranges through numbers, and such that the intended interpretation of $D(u,v,r)$ is $d(u,v)\le r$. This can be easily done with IFP: we start with $D$ containing all tuples $(u,u,0)$, where $u\in G$, and in the inflationary step, we add to $D$ tuples $(u,v’,r’)$ such that there already is a tuple $(u,v,r)$ in $D$ such that $v$ and $v’$ are connected by an edge and $r’$ is the successor of $r$. Using the relation $D(u,v,r)$, we define a formula $\phi(r)$ as $\exists v.\forall u.D(u,v,r)$. Finally, we define a formula $\psi(r)$ as $\phi(r)\land\neg \exists r'<r.\phi(r’)$. Then $\psi(r)$ holds if and only if $G$ has radius $r$.

The last example still does not even use the counting construct $\#x.\phi$; it only used the counting sort and its linear order.

Exercise. Define an IFP+C formula which holds in a graph if and only it has an even number of connected components. Hint (solution by Jarosław Błasiok): define a formula $N(a,b)$, where $a,b$ range over numbers, which holds if and only if there are exactly $a$ vertices whose connected component has cardinality $b$.

Because IFP over the counting sort can be simulated in PTime since the counting sort has the same size as the input structure, we have the following.

Fact. Any IFP+C-definable property of finite relational structures is in PTime.

The CFI theorem

Many natural properties of relational structures can be expressed by the logic IFP+C. For instance, this logic can count the size of a maximal matching in a graph (Anderson, Dawar, Holm, 2013).

The CFI theorem is about showing that not all PTime properties can be defined in IFP+C.

Theorem (Cai-Fürer-Immerman, 1992). There is a property of finite structures which is in PTime but is not definable in IFP+C.

By encoding relational structures into graphs, we get the following.

Corollary. There is a property of finite (simple, undirected) graphs which is in PTime but is not definable in IFP+C.

The property which cannot be defined in IFP+C is solvability of systems of linear equations modulo $2$. To make this precise, we need to specify how to encode a system of linear equations as a relational structure. For simplicity, we will consider only systems of linear equations, where each equation is either of the form $u+v+w=0$ or of the form $u+v=1$. Such a system can be viewed as a relational structure, whose elements are its variables, and there is a ternary relation $T$ and a binary relation $B$, where $T(u,v,w)$ holds for each equation $u+v+w=0$, and $B(u,v)$ holds for each equation $u+v=1$. We assume that the relations are symmetric, i.e., we do not distinguish the equations $u+v+w=0$ and $v+u+w=0$.

We will show that there is no formula of IFP+C which holds exactly in those systems which have a solution. On the other hand, it can be tested whether a system has a solution in polynomial time, using Gaussian elimination.

To prove that no formula of IFP+C can test solvability, we consider systems of a specific “normal form”. A system has normal form if

• For each variable $x$ there is a unique variable $y$ such that $x+y=1$ is an equation of the system; we write $y=\bar x$ and $x=\bar y$ and call $x$ and $\bar x$ duals of each other;
• If $u+v+w=0$ is an equation, then also $\bar u+\bar v+w=0$, $\bar u+v+\bar w=0$, $u+\bar v+\bar w=0$ are equations of the system. Note that all four equations are equivalent over (modulo $2$).

Example. Consider the system of linear equations $x+y+z=0, x+y+t=1$. The relational structure induced by the corresponding system in normal form has eight variables $x,y,z,t,\bar x,\bar y,\bar z,\bar t$, a binary symmetric relation which relates each element with its dual and a ternary relation $\set{(x,y,z),(\bar x,\bar y,z),(x,\bar y,\bar z),(\bar x,y,\bar t),(\bar x,y,t),(x,\bar y,t),(x,y,\bar t),(\bar x,\bar y,\bar t)}$.

Furthermore, we consider systems in normal form of a specific, torus-like shape.

Torus graphs

Consider the graph which delineates the $n\times n$ hexagonal tessellation depicted below – each hexagon is surrounded by six vertices and six edges, and the graph consists of vertices and edges.

The graph $T_n$ – where each vertex at the border is identified with the vertex opposite to it.

We view such a graph as a torus by identifying the leftmost vertices with the rightmost ones, and the vertices at the top with the vertices at the bottom. This gives a torus-like 3-regular graph with $2 n^2$ vertices, denoted $T_n$.

The only properties of the graphs $T_n$ that we use are that they are 3-regular, of increasing size, and for large $n$, do not have small edge separators splitting them into two big parts, as formalised in the following lemma. Appropriate tessellations of spheres or other surfaces would also work.

Lemma 1. Fix a number $k$, and consider a set $X$ of at most $k$ edges in $T_n$, where $n$ is large enough. Then there is a connected component of $T_n-X$ of size at least $2 n^2-c k^2$, for some constant $c>0$ (independent from $k,n$).

If $n$ is large enough comparing to $k$, there is at most one such component, so in this case we can call it the big component of $T_n-X$.

Lemma 1 follows from a variant of the isoperimetric inequality, for the hexagonal, 3-regular tessellation of the plane: any closed path of length $k$ can enclose at most $O(k^2)$ vertices. This inequality can be proved combinatorially, but it also follows from the classical isoperimetric inequality.

Confusing systems of equations

Consider a system of linear equations whose variables are the edges of $T_n$, and where for each vertex of $T_n$ there is an equation $e+f+g=0$, where $e,f,g$ are its adjacent edges. By $S_n$ we denote the normal form of this system – it is obtained by adding the variables $\bar e$ for each edge $e$ of $T_n$, and the equations $e+\bar e=1$, and the equations $\bar e+\bar f+g=0,\bar e+ f+\bar{g}=0,$ and $e+\bar f+\bar{g}=0.$

For a vertex $v$ of $T_n$ with incoming edges $e,f,g$, consider the system as above, but in which the equation $e+f+g=0$ is replaced by $e+f+g=1$, which is actually represented by $\bar e+f+g=0$. By $S_n^v$ we denote the normal form of this system. Note that the systems $S_n$ and $S_n^v$ have exactly the same variables, i.e., the corresponding structures have the same domains.

An assignment to the variables of a system $S_n$ can be seen as selecting a set of edges of $T_n$ – those edges $e$ to which the assignment gives value $1$. An equation $e+f+g=0$ — where $e,f,g$ are the edges adjacent to a vertex $v$ — says that the number of selected edges adjacent with $v$ is even. Therefore, a solution of $S_n$ is any subgraph of $T_n$ whose every vertex has even degree, so a sum of cycles. For example, the empty set, corresponding to the assignment mapping each edge to $0$, is a solution of $S_n$. On the other hand, a solution of $S_n^v$ is a subgraph of $T_n$ whose every vertex has even degree and the vertex $v$ has odd degree. Such a graph does not exist (because the sum of degrees of the vertices of any graph is even), so the system $S_n^v$ has no solution. So we have:

Lemma 2. The system $S_n$ has a solution, and $S_n^v$ does not have a solution.

What is really essential about the systems $S_n$ and $S_n^v$ is that they locally “look” identical. This can be somehow expressed as follows.

Let $P$ be a set of edges of $T_n$, and let $\delta_P$ be the mapping of the domain of $S_n$ which “dualizes” all elements of $P$:

$$\tau_P(u)=\begin{cases}\bar u&\text{if u\in P or \bar u\in P}\\ u&\text{otherwise.}\end{cases}$$

Lemma 3. Let $P$ be a set of edges forming a path in the graph $T_n$ between two vertices $v$ and $w$. Then $\tau_P$ is an isomorphism between $S_n^v$ and $S_n^w$ which fixes all variables not laying on the path $P$.

The proof is similar as for the previous lemma. Note that the two lemmas do not depend on the choice of $T_n$ as the basis for the construction; they would hold for any other 3-regular graph as well, or even for any other graph. (3-regularity is only convenient because it gives rise to one ternary relation. It is possible to start from arbitrary graphs. Then the system $S_n$ would have equations with arbitrarily many variables per equation. To encode this using a finite signature, one could have nodes representing variables and nodes representing equations, and one binary relation joining an equation to each of its variables. The resulting graphs would precisely be the CFI graphs from the original construction.)

Counting infinitary logic

In the proof of the CFI theorem, we will actually show that a certain logic extending IFP+C cannot determine solvability. By $\Cc^{k}_{\omega,\infty}$, or $\Cc^k$ for short, we denote the $k$-variable counting logic with possibly infinite conjunctions and disjunctions, and counting quantifiers of the form $\exists^{\ge n}x.\phi$ (for each $n\in\NN$) whose semantics is “there exist $n$ distinct elements $x$ satisfying $\phi$”.

Lemma 4. A formula of IFP+C using $k$ variables can be converted into an equivalent formula of $\Cc^l$, where $l=O(k)$.

Proof. Almost the same as when converting IFP to a formula of $\Ll^{k}_{\omega,\infty}$. An inequality $(\#x.\phi)\le (\#y.\psi)$ is translated to $\bigvee_{m\le n}\exists^mx.\phi\land \exists^nx.\psi$. $\qed$

Remark. There is a game corresponding to the logic $\Cc^k$, which we define here, but we will not use it in the proof of the CFI theorem. The game is called the bijective $k$-pebble game, and is a modification of the $k$-pebble game. It is played by Spoiler and Duplicator on a pair of structures $(\str A,\bar v_0),(\str B,\bar w_0)$ with distinguished $k$-tuples of elements. Each of the players is the owner of $k$ pebbles numbered from $1$ to $k$, which can be placed on the nodes of the structures. Initially, the pebbles are placed on the positions described by the tuples $\bar v_0$, $\bar w_0$. In each round:

• Spoiler chooses picks one of his pebbles,
• Duplicator picks her pebble with the same label,
• Duplicator picks a bijection between the nodes of $\str A$ and the nodes of $\str B$,
• Spoiler places his pebble on a node of $\str A$ or $\str B$,
• Duplicator places her pebble the node which corresponds via the chosen bijection.

The winning condition is the same as in the $k$-pebble game: for Duplicator to win, she must make sure that after each round the mapping which maps the pebbles in structure $\str A$ to their corresponding pebbles (i.e. with the same label) in structure $\str B$ is a partial isomorphism.

Fact. For all $k\in \NN$,

1. The structures $(A,\bar v_0),(B,\bar w_0)$ are $\Cc^{k}_{\omega,\infty}$,-equivalent,
2. Duplicator has a winning strategy in the bijective $k$-pebble game on $(A,\bar v_0),(B,\bar w_0)$.

The proof of the CFI theorem

To finish the proof of the CFI theorem, we show the following.

Propostion. For any number $k$ and any fixed sentence $\phi$ of $\Cc^k$ there is a number $n$ such that $\phi$ holds in $S_n$ if and only if $\phi$ holds in $S_n^v$, for any $v\in T_n$.

Clearly, this proposition, together with Lemmas 2 and 4 imply the CFI theorem. In the original proof of the CFI theorem, a similar result to the one above was proved. Instead of systems of linear equations, the original proof uses graphs. Those graphs can be seen as an encoding of a system of linear equations. Also, the original proof used the bijective $k$-pebble games to show the above proposition. In the proof that we will now present, we use a more geometric argument.

In what remains, we fix a number $k$. The proof will proceed by induction on the structure of $\phi$, so we need to deal with formulas with free variables.

Let $\phi$ be a formula of $\Cc^k$, and let $\nu$ be a valuation of its free variables in $S_n$. We say that $\phi(\nu)$ ignores a vertex $v$ of $T_n$ if $\phi(\nu)$ holds in $S_n$ iff it holds in $S_n^v$.

For example, let $\phi=T(x,y,z)$ and let $\nu$ map $x,y,z$ to the three edges adjacent to a vertex $v$. Then $T(\nu)$ does not ignore $v$, since $T(\nu)$ holds in $S_n$ but not in $S_n^v$. On the other hand, $T(\nu)$ ignores $v’$, where $v’$ is any vertex different from $v$.

If $\nu$ is a valuation in $S_n$ or $S^n_v$, then by $[\nu]$ let us denote the set of edges $e$ of $T_n$ such that $e$ or $\bar e$ appears in $\nu$.

Let $n$ be large enough, so that $T_n-X$ has a unique big component for any set $X$ of size $k$ (that there is such a number $n$ follows from Lemma 1). In particular, if $\nu$ is a valuation of the free variables of a formula $\phi$ of $\Cc^k$, then $T_n-[\nu]$ has a unique big component.

Lemma 5. For any formula $\phi$ of $\Cc^k$ and for any valuation $\nu$ of its free variables in $S_n$, $\phi(\nu)$ ignores all vertices in the big component of $T_n-[\nu]$.

Lemma 5 implies the proposition (since for a sentence we can take the empty valuation $\nu$, for which $[\nu]=\emptyset$), so it remains to prove the lemma.

Proof. The following fact is crucial in the argument.

Fact. If $\phi(\nu)$ ignores some vertex $v$ in the big component of $T_n-[\nu]$, then it ignores every vertex $w$ in this component.

The fact follows from Lemma 3: the vertices $v$ and $w$ can be connected by a path $P$ which avoids $[\nu]$, so $\tau_P$ is an isomorphism between $S_n^v$ and $S_n^w$ which fixes all elements of $\nu$. Therefore, since $\phi(\nu)$ holds in $S_n^v$, $\phi(\nu)$ also holds in $S_n^w$.

We prove the lemma by induction on the structure of the formula $\phi$. The base case holds, since if $\phi=T(x,y,z)$ and $\nu$ maps $x,y,z$ to some elements of $S_n$, then $T(\nu)$ ignores any vertex except for perhaps the unique vertex $v$ such that $[\nu]$ are the three edges incident with $v$. The formula $B(x,y)$ ignores all vertices of $T_n$.

Obviously, a formula $\phi$ ignores a vertex of $T_n$ if and only if $\neg\phi$ ignores it, which deals with the case of negation.

Suppose now that  $\phi=\bigvee_{i\in I} \phi_i$ is a formula with $k$ free variables, and let $\nu$ be a valuation of these variables in $S_n$. Then, by inductive assumption,  $\phi_i(\nu)$ ignores the vertices in the big component of $T_n-[\nu]$. Therefore, the formula $\phi(\nu)$ also ignores those vertices.

The interesting case is existential quantification, i.e. when $\phi$ is of the form $\exists x.\psi$. Let $\nu$ be a valuation of the free variables of $\phi$. We show that $\phi(\nu)$ ignores every $v$ in the big component of $T_n-[\nu]$.

If $\phi(\nu)$ holds in $S_n$, then the valuation $\nu$ can be extended to $x$, yielding a new valuation $\nu’$ such that $\psi(\nu’)$ holds in $S_n$. By inductive assumption, $\psi(\nu’)$ ignores the vertices in the big component $B$ of $T_n-[\nu’]$. Therefore, $\psi(\nu’)$ holds in $S_n^v$, for every vertex $v\in B$. In particular, $\phi(\nu)$ also holds in $S_n^v$, for every vertex $v\in B$. Observe that because $[\nu]\subset[\nu’]$, the big component of $T_n-[\nu]$ contains $B$, so $\phi(\nu)$ holds in every vertex $v$ of the big component of $T_n-[\nu]$, by the fact stated above.

The case when $\phi(\nu)$ does not hold in $S_n$ is similar – then we show that $\phi(\nu)$ does not hold in $S_n^v$, for every vertex $v$ of the big component of $T_n-[\nu]$.

The remaining case is the case of the counting quantifier $\exists^{\ge k} x.\phi$. This case is very similar to the case of existential quantification considered above.$\qed$

Remark. A slightly stronger result also holds: IFP+C (or $\Cc^k$) cannot determine solvability of linear systems of equations even if the variables are almost linearly ordered, by a relation $\preceq$ which is transitive, total, and such that $x\preceq y\preceq x$ if and only if $x=y$ or $x=\bar y$. In other words, $\preceq$ is a linear order on the set of dual pairs of variables. The proof of this stronger result is exactly the same as above – observe that the isomorphism $\tau_P$ used in the Lemma 3 preserves $\preceq$.

Exercise. Prove that the proposition holds using bijective $k$-pebble games.