Room 327

Counting, addition and other logical delights

Kamal Lodaya

IMSc

The complexity of checking whether a first-order logic property over finite words, FO[<], is satisfiable, grows with the input length as a tower of exponents. Integer addition can be coded using finite words and can be described in FO[<]. It is not definable using FO2[<] (FO with two variables). It is open whether this coding can be done using two variables and arbitrary numerical relations FO2[Num]. We design a two-variable logic using binary alphabetic relations which can express a key three-variable property, betweenness. This is sufficient to code addition, and we do not know of a smaller logic which can do it. The complexity of our logic (in terms of space) grows with the input length by a single exponent, and cannot be done better.

This is joint work with Andreas Krebs, Paritosh Pandya and Howard Straubing.