PBINT, A Logic for Modelling Search Problems Involving Arithmetic

Motivated by computer science challenges, Grädel and Gurevich [13] suggested to extend the approach and methods of finite model theory beyond finite structures, an approach they called Metafinite Model Theory. We develop this direction further, in application to constraint specification/modelling languages. Following [27], we use a framework based on embedded model theory, but with a different background structure, the structure of arithmetic which contains at least (ℕ; 0, 1, + , ×, < , || ||), where ||

x

|| returns the size of the binary encoding of

x

. We prove that on these structures, we can

unconditionally

capture NP using a variant of a guarded logic. This improves the result of [27] (and thus indirectly [13]) by eliminating the small cost condition on input structures.

As a consequence, our logic (an idealized specification language) allows one to represent common arithmetical problems such as integer factorization or disjoint scheduling naturally, with built-in arithmetic, as opposed to using a binary encoding. Thus, this result gives a remedy to a problem with practical specification languages, namely that there are common arithmetical problems that can be decided in NP but cannot be axiomatized naturally in current modelling languages. We give some examples of such axiomatizations in PBINT and explain how our result applies to constraint specification/modelling languages.