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?

  • $\begingroup$ not recursively inseparable as in recursively separable? $\endgroup$ – Ariel Apr 3 '18 at 15:56
  • 1
    $\begingroup$ @Ariel Sorry, typo! $\endgroup$ – StefanH Apr 3 '18 at 15:57

The chosen finite axiomatization of $\mathbb N$ is consistent, since $\mathbb N$ is a model for them. Hence, any sentence provable from it must be satisfiable (e.g. by $\mathbb N$).

From this, we get that the set of provable sentences is disjoint from the set of unsatisfiable formulas.

Hence, the set of unsatisfiable formulas must be undecidable, otherwise we would have separability (taking $R$ to be the set of unsatisfiable formulas), and we would contradict the theorem.

Hence, the set of valid formulas must be undecidable as well, since we have the reduction "$P$ unsatisfiable $\iff \lnot P$ valid" (also mentioned by SimonJ above).


Suppose the set of valid sentences is decidable, then so is the set of satisfiable sentences, I believe, as:

$\varphi$ is satisfiable iff $\neg \varphi$ is not valid.

Thus if the set of satisfiable sentences is not decidable, the set of valid sentences cannot be.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.