Monday, 07.12.2015
10:30

11:30
Room 9222
The search for a logic which captures polynomial time is one of the most important challenges in finite model theory. During
the last years, significant new insights were obtained by the systematic study of the descriptive complexity of queries from
(linear) algebra. These investigations were initiated in 2007 by a striking result of Atserias, Bulatov, and Dawar, who showed
that fixedpoint logic with counting (FPC) cannot define the solvability of linear equation systems over finite Abelian groups.
Their result triggered the development of new candidates for capturing polynomial time, for instance of rank logic (FPR),
which was introduced by Dawar, Grohe, Holm, and Laubner in 2009. Before that, only few other candidates had been proposed,
of which certainly the most important one is Choiceless Polynomial Time (CPT), developed by Blass, Gurevich, and Shelah in
1999. This thesis continues the search for a logic capturing polynomial time in the light of the following leading questions.
(1) How can the algorithmic principles for solving linear equation systems be captured by logical mechanisms (such as operators
or quantifiers)? (2) Are there interesting classes of structures on which the solvability of linear equations systems can
be used to capture polynomial time? Ad (1), we study the interdefinability of linear equation systems over finite Abelian
groups, rings, and modules. Our aim is to transform linear equation systems over these algebraic domains into equivalent linear
equation systems over simpler domains, such as fields, or cyclic groups, via a reduction which is definable in fixedpoint
logic. For linear equation systems over ordered Abelian groups, rings, and modules, and also for certain interesting classes
of unordered commutative rings, we obtain a reduction to cyclic groups. Moreover, we establish a reduction to commutative
rings for the general case. Further, we study rank logic (FPR), which extends FPC by operators to compute the rank of definable
matrices over finite fields. Our main result validates a conjecture of Dawar and Holm: rank operators over different prime
fields have incomparable expressive power. An important consequence is that rank logic, in the original definition with a
distinct rank operator for every prime, fails to capture polynomial time, and should be replaced by a more powerful version
with a uniform rank operator. We further show that, in the absence of counting, solvability quantifiers are weaker than rank
operators. Ad (2), we introduce a class of linear equation systems, so called cyclic linear equation systems, which are structurally
simple, but general enough to describe the CaiFürerImmerman query, and thus separate FPC from polynomial time. Our main
result is that CPT can express the solvability of cyclic linear equation systems. Further, we use this definability result
to show that CPT captures polynomial time on structures with Abelian colours, a class containing many of the known queries
which separate FPC from polynomial time. Our result further solves an open question of Blass, Gurevich, and Shelah: the isomorphism
problem for multipedes is definable in CPT.