Definition:Unsatisfiable/Set of Formulas

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 collection $\FF$ of logical formulas of $\LL$ is unsatisfiable for $\mathscr M$ if and only if:

There is no $\mathscr M$-model $\MM$ for $\FF$

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

$\MM \not \models_{\mathscr M} \FF$


This article is complete as far as it goes, but it could do with expansion.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Expand}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.


Also known as

In sources where satisfiable is referred to as semantically consistent, unsatisfiable is correspondingly termed semantically inconsistent.


An unsatisfiable collection of logical formulas is also often referred to as contradictory.

However, this term is also commonly used to describe the notion of inconsistency in the context of a proof system.

It is therefore discouraged as a synonym of unsatisfiable on $\mathsf{Pr} \infty \mathsf{fWiki}$.


Also see


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Definition:Unsatisfiable/Set_of_Formulas&oldid=451324"