Logical Consequence Union Negation

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $U$ be a set of propositional formulas.

Let $P$ be a propositional formula.

Let $U \models P$ denote that $U$ is a semantic consequence $P$.


Then:

$U \models P$

iff:

$U \cup \left\{{\neg P}\right\}$ has no models.


Proof

Sufficient Condition

Suppose that $U \models P$.


Let $\mathcal M$ be a model such that:

$\mathcal M \models U \cup \left\{{\neg P}\right\}$


Then from Logical Consequence with Union, we have that:

$\mathcal M \models U$

and by definition of semantic consequence:

$\mathcal M \models P$

So we have that $\mathcal M \models P$ and $\mathcal M \models \neg P$

By definition of contradiction, it follows that there can be no such model.


So $U \models P$ is a sufficient condition for $U \cup \left\{{\neg P}\right\}$ to have no models.

$\Box$


Necessary Condition

Suppose that $U \cup \left\{{\neg P}\right\}$ has no models.


There are the following possibilities:

  • $\neg P$ has no models, in which case it is itself a contradiction.

Hence from Tautology and Contradiction, $P$ is a tautology.

Hence $P$ is true under every model.

Hence whatever $U$ may be, every model of $U$ is also a model of $P$:

$U \models P$


  • $U$ has no models, in which case every model of $U$ is also a model of $P$ vacuously, and so:
$U \models P$


  • There exists at least one model of $U$, but each one does not model $\neg P$.

Let $\mathcal M$ be such a model.

We have that:

$\mathcal M \not \models \neg P$

so by definition of negation:

$\mathcal M \models P$

Thus $\mathcal M \models U$ implies that $\mathcal M \models P$.

Hence by definition:

$U \models P$


In all cases $U \models P$.


So $U \models P$ is a necessary condition for $U \cup \left\{{\neg P}\right\}$ to have no models.

$\blacksquare$


Sources

"Evidently $\mathbf A$ is a semantic consequence of $\mathbf H$ if and only if the set $\mathbf H \cup \left\{{\neg \mathbf A}\right\}$ has no models."