Quantifiers in Limits

The standard definition of lim z→∞F(z)=∞ is an ∀∃∀ sentence. Mostowski showed that in the standard model of arithmetic, these quantifiers cannot be eliminated. But Abraham Robinson showed that in the nonstandard setting, this limit property for a standard function F is equivalent to the one quantifier statement that F(z) is infinite for all infinite z. In general, the number of quantifier blocks needed to define the limit depends on the underlying structure ℳ in which one is working. Given a structure ℳ with an ordering, we add a new function symbol F to the vocabulary of ℳ and ask for the minimum number of quantifier blocks needed to define the class of structures (ℳ,F) in which lim z→∞F(z)=∞ holds.