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 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