Counting with one variable

Abstract This chapter introduces the notion of counting quantifiers, and presents some fundamental results in the theory of integer linear programming. We explain the notion of the minimal basis of an integer linear programming instance, and obtain bounds on the values occurring in it. We also introduce the notion of the footprint of a solution, and obtain an upper bound on its cardinality. These results will be used throughout the remainder of the book. In the present chapter, they enable us to show that the one-variable fragment of first-order logic with counting quantifiers has the finite model property, and that its satisfiability problem is in NPTime. We additionally consider the numerical syllogistic, a subfragment of the one-variable fragment with counting quantifiers, originally investigated by A. De Morgan. We show that its satisfiability problem is NPTime-hard.