show/hide this revision's text 2 Added explanation of satisfiability relation; added 120 characters in body

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.
show/hide this revision's text 1

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.