Definition:Unsatisfiable/Formula

From ProofWiki
Jump to navigation Jump to search

Definition

Let $\LL$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\LL$.


A logical formula $\phi$ of $\LL$ is unsatisfiable for $\mathscr M$ if and only if:

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

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

$\MM \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