SAT in finite model theory without order

Question

It is well known in finite model theory that without an order on the input, the expressivity is very limited. For example it is known that $FO(<,\textit{PFP})$ is equal to PSPACE, and $FO(\textit{PFP})$ (without any order in the input) is only PSPACE-relational, a notion defined by Abiteboul and Vianu when they proved their theorem:$FO(\textit{IFP},<)=FO(\textit{PFP},<)$ iff $FO(\textit{IFP})=FO(\textit{PFP})$. (Equivalently P = PSPACE iff P-relational = PSÄCE-relational.)

Relational machines are Turing machines with a finite number of relations. As in a database, a relation is a set of tuples of elements from a finite universe. The machine can check if a relation is empty (if a table is empty), perform Boolean operations over the relations (union, intersection, join, projection), and the usual Turing machine operations. Note that the input of relational machines is given in the relations and not on the tape. It is well known that PSPACE-relational ($FO(\textit{PFP})$) can not even compute parity, hence is less expressive than PSPACE.

One can define queries with relational machines, but one can also define functions, the answer of a function being the content of some relations and of the tape at the end of the computation. Such a machine has the property that if there are two elements $a$ and $b$ of the input such that there is an isomorphism $\phi$ sending $a$ to $b$ and $b$ to $a$, then it is never possible to distinguish $a$ from $b$. In particular in every relation $R$ of the output, if $R(a,\overline x)$ is true, then $R(b,\phi(\overline x))$ is also.

The reason for this is that the allowed operations (union, intersection, projection and join) all respect the isomorphism. Hence the output respects every isomorphism respected by the input.

In $(a\lor b)\land(\neg a\lor\neg b)$, $a$ and $b$ are symmetric, and the function $\phi$ switching $a$ and $b$ is clearly an isomorphism of the input. Suppose there exists a function to compute satisfying assignments for $3-SAT$ instances, and whose output is $P$ (the set of variables assigned to true in a correct assignment). Then we would either want to have $P=\{a\}$ or $P=\{b\}$. However, the isomorphism means that $P$ contains either both $a$ and $b$, or neither.

Hence we have proved that there is no PSPACE-relational function that can output an assignment to a 3-SAT instance.

My question is: how do you prove that there is no PSPACE-relational (i.e. $FO(\textit{PFP})$) that accepts only the input which has a satisfying assignment? The question is different, since I don't intend to compute the assignment and I do not ask to see $a$ or $b$ in the output, I just want to see "accept" or "reject. And contrary to the usual world of Turing machines, it is not equivalent to know if an answer exists and to find the answer, because there is no way for us to use our relational machine for the question "is there an answer with $a=true$" because we can not differentiate $a$ from $b$.

Answer 1

The standard method for showing inexpressibility results for FO(PFP) (and for FO(LFP), by the way) is by using the fact that FO(PFP) is embedded in the finite-variable infinitary logic $\mathrm{L}^\omega_{\infty\omega}$. Here $\mathrm{L}^\omega_{\infty\omega}$ is the finite-variable fragment of $\mathrm{L}_{\infty\omega}$, where the latter is the class of (infinitary) formulas build from the atoms by means of negations, finitary or infinitary disjunctions and conjunctions of the type $\bigvee_i \phi_i$ and $\bigwedge_i \phi_i$, and existential and universal quantification. The logic $\mathrm{L}^k_{\infty\omega}$ is the collection of all formulas in $\mathrm{L}_{\infty\omega}$ that involve at most $k$ variables (quantified or not), and $\mathrm{L}^\omega_{\infty\omega} = \bigcup_k \mathrm{L}^k_{\infty\omega}$.

It is known that FO(PFP) $\subseteq \mathrm{L}^\omega_{\infty\omega}$ (see Theorem 7.4.2 in Ebbinghaus and Flum book "Finite Model Theory"). Thus, if you prove that something is not expressible in $\mathrm{L}^k_{\infty\omega}$ for any $k$, then you also prove that it is not expressible in FO(PFP).

Now, how does one prove inexpressibility results for $\mathrm{L}^k_{\infty\omega}$? By playing the $k$-pebble games. These are Ehrenfeucht-Fraissé-type of games where the number of rounds is unbounded but each player has at most $k$ pebbles that he can re-use (see Ebbinghaus and Flum book again for details).

After all this background, now we can show that CNF-SAT is not expressible in $\mathrm{L}^k_{\infty\omega}$ for any $k$. For every fixed $k$, we need to find a satisfiable CNF formula $F_k$ and an unsatisfiable CNF formula $G_k$ such that $F_k \equiv^k_{\infty\omega} G_k$, where $A \equiv^k_{\infty\omega} B$ means that the Duplicator has a winning strategy for winning the $k$-pebble game on the structures $A$ and $B$ (here we need to fix some sensible way of encoding CNF formulas as finite structures: let's say we encode them as their bipartite incidence graph with elements representing clauses on one side, elements representing variables on the other, and 2 types of binary relations indicating which variables appear in which clauses and under what sign). I claim that an explicit choice of $F_k$ and $G_k$ is possible. But instead I will give you an indirect proof.

It is trivial to see that $K_k \equiv^k_{\infty\omega} K_{k+1}$, where $K_a$ denotes the clique-graph on $a$ vertices. In particular EVENNESS is not definable in $\mathrm{L}^\omega_{\infty\omega}$. It is also known that CNF-SAT is NP-complete under first-order reductions (see Theorem 7.16 in Immerman's "Descriptive Complexity" book). Since trivially EVENNESS is in NP, this means that there is a first-order reduction from EVENNESS to CNF-SAT. Since first-order reductions (in pure first-order logic, without built-in linear-order or anything as it is the case in Theorem 7.16 from Immerman's book) preserve expressibility in $\mathrm{L}^\omega_{\infty\omega}$ backwards, the result follows: if CNF-SAT were expressible, EVENNESS would also be; a contradiction.