= Unsatisfiability
{title2=$\operatorname{Mod}(\Gamma)=\varnothing$}
A <logical formula> or a collection of formulas is \b[unsatisfiable] when no permitted interpretation makes all of it true. The permitted interpretations come from the chosen semantics: <Boolean valuations> for <propositional logic>, or structures and variable assignments for <first-order logic>. <Unsatisfiability> is therefore a semantic property; a <refutation> is a syntactic proof of that property.
For example, $p\land\neg p$ is unsatisfiable because neither truth value of $p$ makes both parts true. The <logical formula> $p\lor q$ is satisfiable, although it is false in the valuation assigning false to both letters. Thus being false in one interpretation does not establish <unsatisfiability>. In <classical propositional logic>, $\varphi$ is valid exactly when $\neg\varphi$ is unsatisfiable. Likewise, $\Gamma\models\varphi$ exactly when $\Gamma\cup\{\neg\varphi\}$ is unsatisfiable. This turns entailment questions into searches for countermodels or contradiction certificates.
Back to article page
