“Almost all” quantifier

Suppose I enlarge the first-order logic with an "almost all" quantifier, let's denote it by G, ie.:

$G_x P(x) \iff$ for all but finitely many x, P(x)

Syntax for G is the same as for other quantifiers.

Suppose I am working over the first-order theory of natural numbers. For every sentence $T$ using $G$, does there exist a sentence $S$ over "standard" first-order logic, such that $S \iff T$ in every countable model of natural numbers?

-
If you want to have more insight on this quantifier take a look at the paper "Decidability of the Natural Numbers with the Almost-All Quantifier" by Marker and Slaman (the link is arxiv.org/abs/math/0602415 ) –  boumol Sep 7 '11 at 13:28
@bourmol That's not really very on topic. Marker and Slaman add an "alomst all" quantifier but they delete the "for all" and "there exists" quantifiers. This makes the logic much weaker than standard logic. We talked about this some at math.stackexchange.com/questions/50625 –  David Speyer Sep 7 '11 at 13:41
@David: Thanks for the correction, you are right. By the way, anybody knows a reference for the $\Pi_2$-completeness of the problem of determining in general whether a diophantine equation has infinitely many solutions? This is claimed by JDH at the end of the stackexchange link. –  boumol Sep 7 '11 at 13:59
In Mazur, B. Questions of decidability and undecidability in number theory. J. Symbolic Logic 59 (1994), no. 2, 353–371. Mazur says that it is open whether deciding if a diophantine equation has infinitely many solutions is $\Pi_2$-complete. –  Dave Marker Sep 8 '11 at 12:00
@boumol: End of page 357 and the beginning of the next page. –  Emil Jeřábek Sep 8 '11 at 13:34

No. For example, Robinson’s Q + $\forall x\,G_y\,x<y$ is a categorical theory (its only model up to isomorphism is the standard model of arithmetic), hence it is not equivalent to any first-order sentence (or theory).
EDIT: In order to avoid confusion: my answer above assumes that “every countable model of natural numbers” in the OP is interpreted so that it includes at least one nonstandard model of true arithmetic. The Marker and Slaman paper mentioned in the comments seemingly contradicts what I wrote as they call the almost-all quantifier to be a fragment of first-order logic. The explanation is that they only care about validity in the standard model $\mathbb N$: then $G_x\,\phi(x)$ is equivalent to the first-order formula $\exists u\,\forall x\,(u\le x\to\phi(x))$. However, this equivalence is not valid in any nonstandard model of arithmetic.
The OP is somewhat sloppy, but gives a definition of the semantics: $M\models G_x\phi(x)$ iff $M\models\phi(a)$ for all but finitely many $a\in M$. Obviously, if you change the definition of any notion involved in the question, it may change the answer. In some contexts it might make sense to simply define the almost-all quantifier as $\exists u\,\forall x\,(u\le x\to\phi(x))$, but (1) this is not what the question says, (2) it would make the question pointless as the definition would already give a trivial answer, and (3) it would not give an extension of first-order logic in general, ... –  Emil Jeřábek Sep 7 '11 at 15:13
Re Kaveh's question. This answer is perfectly valid, but I want to point out that usually, in the context of arithmetic, when we say "finitely many" we mean "for a bounded set in the model", and if I saw $\forall^\infty$ or $\exists^\infty$ in this setting I would assume the quantifiers are the usual definitional extension of the object language. It's not surprising that it should be impossible to define metafiniteness within an arbitrary model of arithmetic; it it was possible, it would mean that either every element of the model is metafinite, or else some induction axiom should fail. –  Carl Mummert Sep 7 '11 at 18:30