Definition:Unsatisfiable/Formula

From ProofWiki
Jump to: navigation, search

Definition

Let $\mathcal L$ be a logical language.

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


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$


Also known as

Unsatisfiable formulas are also referred to as:

  • contradictions;
  • logical falsehoods;
  • logical falsities;
  • inconsistent formulas.

Because the term contradiction also commonly refers to the concept of inconsistency in the context of a proof system, it is discouraged as a synonym of unsatisfiable formula on $\mathsf{Pr} \infty \mathsf{fWiki}$.

The next two of these terms can easily lead to confusion about the precise meaning of "logical", and are therefore also discouraged on $\mathsf{Pr} \infty \mathsf{fWiki}$.


Also see