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.
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.