Unsatisfiability ($\mathrm{Mod}(\Gamma )=\varnothing$)

A logical formula or a collection of formulas is 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\wedge \neg p$ is unsatisfiable because neither truth value of $p$ makes both parts true. The logical formula $p\vee 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, $\phi$ is valid exactly when $\neg \phi$ is unsatisfiable. Likewise, $\Gamma \models \phi$ exactly when $\Gamma \cup \{\neg \phi \}$ is unsatisfiable. This turns entailment questions into searches for countermodels or contradiction certificates.