First Order Logic clauses decidability

Question

I know that First Order Logic is semi-decidable. However, if we work only with clauses is it correct to say that, due to the soundness and completeness of Resolution Principle, we achieved decidability ?

Answer 1

Short Answer: No.

Soundness and completeness do not imply decidability.

The resolution method can typically only show that some set of statements is inconsistent, rather than that it is consistent, and for decidability you need both. Put differently: The resolution method shows that FOL is 'semi-decidable', but not that it is (fully) decidable.

Long Answer: Still no.

Let $\Gamma$ be some set of FOL statements, and you want to see whether or not that set of statements is consistent using the Resolution method.

Soundness of the resolution method means that if by resolution you end up with the empty clause, then $\Gamma$ is inconsistent.

Completeness of the resolution method means that if $\Gamma$ is inconsistent, then by resolution you can end up with the empty clause (I say 'can', since whether you actually will end up with an empty clause depends on the order in which you choose clauses to resolve; that is, there are situations in which you method of choosing clauses to resolve will go on forever without ever getting to an empty clause, and yet there is a way to get to the empty clause by choosing the clauses to resolve in a different order)

Please note, then that soundness and completeness are only about the inconsistency of $\Gamma$, not about its consistency. That is, just because we have a complete method for inconsistency does not mean we have a complete method for consistency. Indeed, from the fact that FOL is undecidable, we know that the Resolution is not complete with regard to consistency.

OK, but why is that?

Well, it is true that for some sets of statements $\Gamma$, the Resolution method comes to a 'stop' in the sense that no more new clauses can be obtained using the Resolution rule. Trivial example: we start out with $\{ P(a) \}$ as our only clause. So, in those cases we can say that we cannot obtain the empty clause, and therefore the original set of statements $\Gamma$ is consistent.

However, for other clause sets we can keep obtaining new clauses indefinitely .. and hence the Resolution method never gets to a point where it can say for sure that it is impossible to obtain the empty clause, and hence it can't tell whether the original $\Gamma$ is consistent or not. Therefore, the Resolution method is not a (full) decision procedure... we only have semi-decidability'.