Algorithm to determine if a Diophantine Equation has an infinite number of solutions

Question

In their paper , Marker and Slaman, proved the decidability of the the theory of the natural numbers with the quantifier "for all but finitely many", One can obviously encode the question of whether any diophantine equation has an infinite number of solution as the question of whether a statement belonging to this language is satisfied by the Naturals or not. Since they proved the theory is decidable we know that such algorithm exists. My question is: Has any one tried to come up with an efficient algorithm for that ?

Link to the paper: http://www.math.uic.edu/~marker/aa-v3.pdf

Answer 1

There is a fundamental error in this question.

For a one-variable diophantine equation, the question whether it has infinitely many solutions is rather trivial to answer (and the answer is the same over $\mathbb{Z}$ and over $\mathbb{R}$, as Carl pointed out).

The situation is different with more than one variables. The basic reason for this is that $$\exists^\infty x \exists^\infty y \cdots$$ does not mean

There are infinitely many pairs $x, y$ such that $\cdots$

It rather means,

There are infinitely many $x$ for each of which there are infinitely many $y$ such that $\cdots$

In fact, it is not possible to say there are infinitely many pairs (triples, quadruples, etc.) in the fragment of first-order logic that Marker and Slaman consider in their paper (for the reason that David pointed out).

Answer 2

The question of whether a diophantine equation has infinitely many solutions is at least hard as the question of whether a diophantine equation has any solutions, and is therefore undecidable. (As JDH comments below, in a certain technical sense, the question of whether there are infinitely many solutions may be harder.)

Proof: Let $F(x_1, x_2, \ldots, x_m)=0$ be any diophantine equation. Then $F=0$ has a solution if and only if $F(x_1, x_2, \ldots, x_{m-1}, y-z)=0$ has infinitely many solutions.

Your error is equating "infinitely many" with the much larger "all but finitely many".

UPDATE: As Mohammed points out "It is false that all but finitely many bagels are delicious" is equivalent to "infinitely many bagels are not delicious". And the theorem of Marker and Slaman is for all first order statements, not just for diophantine equations, so we should be able to use this rewording.

On skimming their paper, the first thing that I notice is that they have the quantifier $\forall^{\infty}$ ranging over a single integer variable, not over a $k$-tuple of integers, so you can say "For all but finitely many $x$, the following holds for all but finitely many $y$..." but can't directly say the stronger "For all but finitely many ordered pairs $(x,y)$..." But I'm not sure whether this is the heart of the difference, or just a minor technical issue.