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.
Best Answer
There's a general "trick" for handling all issues of this sort. Take any mathematical theorem that a platonist regards as meaningful. Formalize it as a formal theorem T in ZFC. The formalist will now accept the sentence, "ZFC proves T."
Here, the only potentially confusing concept is that of truth. But to say that some first-order sentence of arithmetic is true just means that it is satisfied by the structure $\mathbb N$. The satisfaction relation, like all ordinary mathematics, is readily defined set-theoretically, as you can see in any textbook on logic. So the nonexistence of the algorithm in question can be expressed as a first-order sentence of set theory, and the formalist will agree that this sentence is a theorem of ZFC.
For some kinds of finitistic statements, the formalist doesn't have to do this little dance of translating "true" into formal set-theoretic terms and replacing "T" with "ZFC proves T." For example, in the sentence, "It is true that ZFC proves T," the formalist can use his "native" understanding of the word "true" and doesn't have to convert "ZFC proves T" into an arithmetic statement S and use the set-theoretic definition of truth to get a set-theoretic assertion whose ZFC-theoremhood he can agree with. But the little dance is always available as an option.
EDIT: Reading various comments to the original question and to other answers, I see that something more may need to be said about the satisfaction relation, even though it is standard textbook material. To say that a first order sentence $\phi$ is true, or that it belongs to $\mathrm{Th}(\mathbb N)$, means that it is satisfied by $\mathbb N$, where satisfiability is defined inductively. For example, $\exists x: \phi(x)$ is satisfied by $\mathbb N$ if there exists $x\in \mathbb N$ such that $\phi(x)$ is satisfied by $\mathbb N$. Further details may be found here.
Now, you might complain that in order to "make sense" of the satisfiability relation, you have to "make sense" of $\mathbb N$. However, you don't have to believe in $\mathbb N$ as some kind of platonically existing thing in order to correctly manipulate sentences about $\mathbb N$. Any sufficiently powerful set-theoretic meta-theory will suffice to carry out the definition of $\mathbb N$ and the satisfaction relation. ZFC is the standard choice but you could use something else if you prefer. A way to assert the existence of $\mathbb N$ in the first-order language of set-theory is as follows: $$\exists x:(\emptyset \in x \wedge \forall y\in x: (y\cup\lbrace y\rbrace\in x))$$ Here I've used various abbreviations, e.g., $\emptyset\in x$ expands formally to $\exists z : (z\in x \wedge \neg \exists w: (w\in z))$. Similar but more complicated formalizations can be produced for "set of first-order sentences of arithmetic" and "$\mathbb N$ satisfies $\phi$." As long as you know the axioms and rules of inference for ZFC, you can verify that the existence of $\mathrm{Th}(\mathbb N)$ is provable in ZFC. (Note: This is NOT the same as saying that every true sentence of arithmetic is provable in ZFC, which is absolutely false!) And once you have $\mathrm{Th}(\mathbb N)$, you can simply interpret "x is true" as $x\in \mathrm{Th}(\mathbb N)$. In particular, there is nothing mysterious about truth; it is just a mathematical concept formalizable in ZFC like any other mathematical concept.