# Semidecidability and NP-Hard

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 ?

• 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! – Raphael Mar 1 '18 at 9:08
• You should read about complexity classes $NP$ and $RE$. And what hardness is. – 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.
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.