# First Order Logic - Logical Consequence and Paradox

When we use the Resolution Principle we try to deduce a logical consequences from 2 clauses.

The set of clauses is unsatisfable , if we get a empty clause.

What i dont understand is : in practice, an empty clause is simply false. So, what proof that the set of clauses is unsatisfable is a paradox , am i correct ?

ps:i intend the paradox as the fact that a model of the clauses should be the model of a false statement.

pss: if it's true. How is possible that a logical consequence can lead to a paradox ? This seems mathematically strange to me :S

• The empty clause is simply a contradiction: thus, by definition, it is unsatisfiable. – Mauro ALLEGRANZA Feb 13 '18 at 12:50
• The resolution rule resolves two clauses $\lnot p \lor q$ and $p \lor r$ deriving the "resolvent" $q \lor r$. It is a logical rule, and thus it is sound, i.e. derives true conclusion from true premises. Thus, if we derive the empty clause, i.e. $\bot$, we have proved that the originals et $S$ of clauses is unsatisfiable (i.e. contradictory) because only a contradiction con entail $\bot$. – Mauro ALLEGRANZA Feb 13 '18 at 13:00
• Recall that $S \vDash \alpha$ (reading: the formula $\alpha$ is a logical consequence of the set $S$) means: every interpretation that satisfies all of $S$ also satisfies $\alpha$. If $\alpha$ is $\bot$, it is unsatisfiable. Thus, if we have $S \vDash \bot$, we have to conclude that also $S$ is unsat. – Mauro ALLEGRANZA Feb 13 '18 at 13:01
• Conclusion: no paradox at all. – Mauro ALLEGRANZA Feb 13 '18 at 13:07
• @MauroALLEGRANZA Sorry but I don't quite understand why 'Only a contradiction can entail ⊥'...the definition of logic entailment/consequence as I understand is that, (for $\psi \vDash \phi$)for all the truth assignments that satisfies $\psi$, they also satisfy $\phi$. But for ⊥ it will always be false, so how can there be any truth assignment that satisfies it? Even if $\psi$ is always false, the best we could say seem to be that $\psi$ is logically equivalent to ⊥, instead of entailing ⊥. – Daniel Mak Mar 22 '18 at 5:19

However, when you try to figure out whether some statement $\varphi$ follows from a set of statements $\Gamma$, you first negate the statement $\varphi$, and then put everything into clauses. Then, when you derive the empty clause, you have shown that the set of statements $\Gamma \cup \{ \neg \varphi \}$ is unsatisfiable, and that means that $\varphi$ is a logical consequence of $\Gamma$.
In other words, to use the resolution method to check for logical consistency you set it up as kind of a proof by contradiction: assume that $\varphi$ is not true, and if that leads to a contradiction, then you have proven $\varphi$