I am reading Bjorn Poonen's very nice survey on Hilbert's Tenth problem (http://www-math.mit.edu/~poonen/papers/uniform.pdf), and while I believe I understand the mathematics well, I have widespread difficulties with the meta-mathematics of these questions. To illustrate them, and to ask a question that is answerable and whose answer might be helpful for me, let me focus on one little passage of this paper, that concerns not directly Matthiasevich's theorem that the tenth problem has a negative solution but an older, weaker version :
"[...] the work of K. Gödel, A. Church, and A. Turing in the 1930s made it clear that there was no algorithm for solving the [...] problem of deciding the truth of first-order sentences over $\mathbb{Z}$". (page 6)
What does that assertion exactly mean?
I understand well what an algorithm is and what a first-order sentence in arithmetic is. The difficult word in the quoted sentence is "truth".
Here is my tentative interpretation. Define a "platonist" as someone who believes that natural integers actually exist and that first order sentences about them are either absolutely true or absolutely false. I am such a person. So for a platonist, the passage quoted above would mean: "there is no Turing machine that take a first-order sentence as input and produces the output TRUE or FALSE according to wether the sentence is absolutely true or absolutely false." Ok. The problem is that this interpretation makes sense only for a platonist. I am not going to name names here, but I know very good mathematicians that are not platonists in the above sense.
Is there another (weaker) interpretation of the quoted sentence, that would make sense for pretty all mathematicians?
Or, is the statement from Poonen's paper simply rejected as non-sensical by those non-platonist mathematicians ?
I have in mind Gödel's incompleteness theorem itself, that comes in two versions: one for everyone, that says that there is a first-order arithmetical sentence that can not be proved nor disproved in, say, PA; and one stronger version for platonists that says that there is a first-order arithmetical sentence, that cannot be proved in, say, PA, but that is nevertheless true. But for the theorem of Gödel-Church-Turing quoted by Poonen I don't see what would be the version acceptable by everyone.
Edit: Many people seem to have great difficulties to understand my question. I am not sure I understand why. Let me try to explain it more from the "philosophical" point of view. I think anyone would agree that it is not self-evident that a first-order statement about numbers makes sense, and is either true or false independently of the system of axioms we choose. (Surely, a statement about sets does not necessary make sense, like "is the set of all sets an element of itself".) Actually, I do believe that any first-order statement about numbers makes sense, but for me this is like a religious belief, not something I would feel authorized to use in a serious mathematical theorem. Basically, like most number theorists I suppose, I work with ZF with the enumerable axiom of choice, and I feel pain in the stomach when occasionally I need to use the full axiom of choice or Grothendieck's axiom of universes (and in general, we convince ourselves that they are just used "to simplify the exposition", and that they could be avoided at the cost of just a lost in elegance). So when I see a statement like the one in boldface above, as a platonist I understand what it means, but I wonder if it is a reasonable statement that I can agree with with non-platonist colleagues.