Graedel and Gurevich introduced Metafinite Model Theory and studied capturing of NP on small cost Arithmetic structures. We found that the small cost condition is implicit in many Knowledge Representation and Constraint Modelling languages with arithmetic. As a consequence, the representation of some common problems in NP, such as Integer Factorization, requires binary encodings, which is unnatural for most people.
As a step toward addressing this problem, we proposed a logic that we call PBINT, which stands for Polynomially Bounded Integers. The logic is a variation on the Guarded Fragments. We prove that PBINT captures NP in the Metafinite setting without the small cost condition.
Based on a joint work with S. Tasharrofi and D. Mitchell.