Why is first-order logic (without arithmetic) VALIDITY only recursively enumerable, and not recursive?

Question

Papadimitriou's "Computational Complexity" states that VALIDITY, the problem of deciding whether a first-order logic (without arithmetic) formula is valid, is recursively enumerable. This follows from the completeness and soundness theorems, which equate VALIDITY and THEOREMHOOD, the latter being the problem of finding a proof for a formula, which had previously been shown to be recursively enumerable.

However, I am not seeing why VALIDITY is not recursive as well, because given a formula $\phi$, one could run two Turing Machines for THEOREMHOOD, one on $\phi$ and the other on $\neg \phi$, concurrently. Since at least one of them is valid, it is always possible to decide whether $\phi$ is valid, or not valid. What am I missing?

Note: this question refers to first-order logic without arithmetic, so Gödel's Incompleteness Theorem does not have a bearing here.