Definition:Unsatisfiable/Set of Formulas
Contents
Definition
Let $\mathcal L$ be a logical language.
Let $\mathscr M$ be a formal semantics for $\mathcal L$.
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$
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information.
To discuss it in more detail, feel free to use the talk page.
If you are able to do this, then when you have done so you can 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 (see the proofread template for usage).
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
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.7$ First-Order Logic Semantics: Definition $\mathrm{II.7.13}$
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.5.2$: Definition $2.42$
