Definition:Unsatisfiable

From ProofWiki
Jump to: navigation, search

Definition

Let $\mathcal L$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\mathcal L$.


Unsatisfiable Formula

A logical formula $\phi$ of $\mathcal L$ is unsatisfiable for $\mathscr M$ iff:

$\phi$ is valid in none of the structures of $\mathscr M$

That is, for all structures $\mathcal M$ of $\mathscr M$:

$\mathcal M \not\models_{\mathscr M} \phi$


Unsatisfiable Set of Formulas

A collection $\mathcal F$ of logical formulas of $\mathcal L$ is unsatisfiable for $\mathscr M$ iff:

There is no $\mathscr M$-model $\mathcal M$ for $\mathcal F$

That is, for all structures $\mathcal M$ of $\mathscr M$:

$\mathcal M \not\models_{\mathscr M} \mathcal F$


Unsatisfiable for Boolean Interpretations

Let $\mathbf A$ be a WFF of propositional logic.


$\mathbf A$ is called unsatisfiable (for boolean interpretations) if and only if:

$v \left({\mathbf A}\right) = F$

for every boolean interpretation $v$ for $\mathbf A$.


In terms of validity, this can be rendered:

$v \not\models_{\mathrm{BI}} \mathbf A$

that is, $\mathbf A$ is invalid in every boolean interpretation of $\mathbf A$.


Also see