# Refutation in first order logic

Consider the following statement

In FOL, we can reduce entailment checking to satisfiability checking:

$$S \models S' \iff S \land \neg S'$$ is satisfiable (This proof strategy is called refutation).

Is the above statement true? If yes, then I got confusion because of the following steps

$$S \models S' \iff S\implies S'$$ is true

$$S \models S' \iff \neg S \lor S'$$ is satisfiable

$$S \models S' \iff \neg( S \land \neg S')$$ is satisfiable

$$S \models S' \iff S \land \neg S'$$ is unsatisfiable

Which one is true?

• This is a math question, and belongs in Mathematics. – Yuval Filmus Feb 3 '19 at 15:38
• @YuvalFilmus I disagree. Logic is fundamental to CS. – David Richerby Feb 3 '19 at 16:40

## 1 Answer

This looks like a typo in your source, and your derivation looks correct. So the corrected statement should be:

$$S \models S' \iff S \land \neg S'$$ is unsatisfiable

or

$$S \models S' \iff {\boldsymbol \neg} (S \land \neg S')$$ is satisfiable