Two given languages $L_1$ and $L_2$ are called recursively separable iff there exists a recursive languge $R$ such that $L_1 \subseteq R$ and $L_2 \cap R = \emptyset$.
Now consider first order logic, and some finite axiomatisation of $\mathbb N$ in it (surely this is way to weak, as we have no induction). Then we have three sets, 1) the set of valid sentences, i.e. the ones derivable the the rules of first order logic, 2) the set of provable sentences using the axioms of $\mathbb N$, and the set of truth sentences, i.e. the ones fullfilled by $\mathbb N$. Also as a superset of all these, we have the set of first order sentences that have some model, and contrary to that the set of sentences that are unsatisfiable, i.e. have no model, which equals (by Completeness of first order logic) the set of inconsistent sentences.
Now, the following holds:
Theorem: The set of unsatisfiable sentences and the set of sentences provable from the choosen axioms of $\mathbb N$ are not recursively separable.
From this it follows that the set of provable sentences from the axioms itself, as well as the set truth sentences, as well as the set of satisfiable sentences, are all not recursive/decidable.
But does this implies that the set of valid sentences is not decidable? This is states in the classic text Computational Complexiy by Cristos H. Papadimitriou, on page 133. But as this set is a proper subset of the provable sentences, I do not see that this is implied by the above Theorem? Or am I missing anything?