# Tautology iff Negation is Unsatisfiable

## Theorem

Let $\mathbf A$ be a WFF of propositional logic.

Then $\mathbf A$ is a tautology iff its negation $\neg \mathbf A$ is unsatisfiable.

## Proof

### Necessary Condition

Let $\mathbf A$ be a tautology.

Let $v$ be a boolean interpretation of $\mathbf A$.

Then $v \left({\mathbf A}\right) = T$.

Hence, by definition of the boolean interpretation of negation:

- $v \left({\neg \mathbf A}\right) = F$

Since $v$ was arbitrary, it follows that $\neg \mathbf A$ is unsatisfiable.

$\Box$

### Sufficient Condition

Let $\neg \mathbf A$ be unsatisfiable.

Let $v$ be a boolean interpretation of $\neg \mathbf A$.

Then $v \left({\neg \mathbf A}\right) = F$.

Hence, by definition of the boolean interpretation of negation:

- $v \left({\mathbf A}\right) = T$

Since $v$ was arbitrary, it follows that $\mathbf A$ is a tautology.

$\blacksquare$

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 2.5$: Theorem $2.39$