Im studying the semidecidability of First Order logic.

According to wiki

A logical system is semidecidable if there is an effective method for generating theorems (and only theorems) such that every theorem will eventually be generated. This is different from decidability because in a semidecidable system there may be no effective procedure for checking that a formula is not a theorem

The semidecidability seems to me exactly equal to halting problem, which is NP-HARD. 1) Is it correct ? 2) So also First Order Logic is NP-HARD ?

  • $\begingroup$ The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! $\endgroup$ – Raphael Mar 1 '18 at 9:08
  • $\begingroup$ You should read about complexity classes $NP$ and $RE$. And what hardness is. $\endgroup$ – rus9384 Mar 1 '18 at 18:35

A language $L$ is semidecidable if there is a Turing machine that on input $x$, halts if $x \in L$, and doesn't halt if $x \notin L$. It is decidable if there is a Turing machine that on input $x$, halts at an accepting state if $x \in L$, and halts at a rejecting state if $x \notin L$. It's not hard to check that every decidable language is also semidecidable.

A logical system is semidecidable (decidable) if the language of all theorems in the system is semidecidable (decidable).

Being semidecidable is an upper bound on the complexity of a language. Being NP-hard is a lower bound on the complexity of a language. If all you know about a language is that it is semidecidable, you cannot deduce that it is NP-hard, just as you cannot conclude that $x \geq 0$ from the inequality $x \leq 1$.

The halting problem is $\Sigma_1^0$-complete, which means that it is semidecidable (an upper bound), and moreover, every semidecidable language can be reduced to it using a computable reduction (a lower bound). To be equivalent to the halting problem, you need both an upper bound on your language and a lower bound on your language. The language of theorems in a logical system is guaranteed (by definition) to be semidecidable, but it could also be decidable, in which case it is definitely not equivalent to the halting problem.

Finally, you don't explain what you mean by First Order Logic, but assuming that it can express propositional tautologies, then the corresponding language of theorems is definitely NP-hard, by reduction from SAT. In fact, the language of true quantified Boolean formulas, known as TQBF, is known to be PSPACE-complete.

  • $\begingroup$ What i meant was if FOL SAT problem is np hard $\endgroup$ – Qwerto Mar 1 '18 at 8:58
  • $\begingroup$ I'm still not sure what you mean by that. If you mean TQBF, then it's not only NP-hard, but actually PSPACE-complete. $\endgroup$ – Yuval Filmus Mar 1 '18 at 9:02

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.