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