Just came back from a visit to Flavio Ferrarotti in Hagenberg, Austria. Hagenberg is an inspirational mixture of a traditional countryside village and a high-tech software campus. Flavio works in finite model theory and during our discussions I was reminded of the beautiful formalism of Choiceless Polynomial Time with Counting invented by Gurevich and Shelah. Basically it is programming with sets, much like in the programming language SETL, but in a logical way, i.e., atomic data elements are abstract entities and not numbers that can be compared, added, multiplied, and so on.
The conjecture is that not every polynomial-time database query can be expressed in Choiceless Polynomial Time with Counting; for nonboolean queries, this has been proved by Benjamin Rossman but it remains open for boolean queries.
Yuri Gurevich actually conjectures that there is no language for the polynomial time boolean queries, but proving this is of course quite a challenge, in view of the fact that there does exist a language for the NP boolean queries (existential second-order logic, compare Fagin's Theorem).
More recently, Anuj Dawar and collaborators investigated an interesting alternative approach, based on adding primitives from linear algebra (notably, computing the rank of a matrix) to fixpoint logic. I have not followed this closely but would be interested in hearing the latest feeling/opinion on this development. It would be great if Anuj could chime in with a brief comment bringing us up to date on this matter!
Jan, thank you for inviting me to comment on this. It is great to see this blog up and running.
The relationship between choiceless polynomial time with counting (CPTC) on the one hand and fixed-point logic with rank (FPR) on the other is certainly interesting. Neither one has been shown included in the other, and it would be really interesting to show separations. One point I should stress is that the primitives from linear algebra that are added to fixed-point logic are operators for the rank of a matrix *over finite fields*. The reason is that this is what fixed-point logic with counting (FPC) is unable to express. Linear algebra over the rationals turns out to be easier to define and most of what we want to do is already definable in FPC.
For most recent work on CPTC and FPR, I strongly recommend Wied Pakusa's PhD thesis available from his webpage:
https://logic.rwth-aachen.de/People/Pakusa/