Expressive power of unary counters

We compare the expressive power on finite models of two extensions of first order logic L with equality. L(Ct) is formed by adding an operator count{x:φ}, which builds a term of sort ℕ that counts the number of elements of the finite model satisfying a formula ϕ. Our main result shows that the stronger operator count{t(x): ϕ}, where t(x) is a term of sort ℕ, cannot be expressed in L(Ct). That is, being able to count elements does not allow one to count terms.This paper also continues our interest in new proof techniques in database theory. The proof of the unary counter combines a number of model-theoretic techniques that give powerful tools for expressivity bounds: in particular, we discuss here the use of indiscernibles, the Paris-Harrington form of Ramsey's theorem, and nonstandard models of arithmetic.