My question is fairly simple, and may at first glance seem a bit silly, but stick with me. If we are given the rationals, and we pick an element, how do we recognize whether or not what we picked is an integer?

Some obvious answers that we might think of are:

A. Write it in lowest terms, and check the denominator is 1.

B. Check that the p-adic valuation is non-negative, for all p.

C. Decide whether the number is positive (or negative) and add 1 to itself (or -1 to itself) until it is bigger than the rational you picked. (If these multiples ever equaled your rational, then you picked an integers.)

Each of these methods has pluses and minuses. For example, in option A we presuppose we know how to write an arbitrary rational number q as a quotient of integers and reduce. In C, we have issues with stopping times. etc..

To provide some context for my question: We know, due to the work of Davis, Putnam, Robinson, and Matijasevic, that the positive existential theory of $\mathbb{Z}$ is undecidable. The same question for $\mathbb{Q}$ is not entirely answered. One approach to this new question is to show that that, using very few quantifiers, one can describe the set of integers inside the rationals; and then reduce to the integer case. For example, see Bjorn Poonen's paper "Characterizing integers among rational numbers with a universal-existential formula." There, he finds a way to describe the p-valuation of a rational number (i.e. he finds a way to encode option B in the language of quantifiers and polynomials on the rationals). I'm wondering if there are other characterizations of the integers which would follow suit.