# Homotopy Type Theory de Morgan's law

The axiom De Morgan’s Law says that for any $A$ and $B$, if not ($A$ and $B$), then (not $A$) or (not $B$). This is the only one of the four implications making up the classical de Morgan’s laws that is not constructively provable.

Since negations are always propositions?, and propositional truncation? preserves $\times$, in the statement of DML we might as well assume $A$ and $B$ to be propositions. However, it is not quite as obvious whether it matters if the “or” is truncated or not, in other words whether

$\prod_{A,B} \neg(A \wedge B) \to (\neg A + \neg B)$

is equivalent to

$\prod_{A,B} \neg(A \wedge B) \to \Vert \neg A + \neg B\Vert.$

In fact, these are equivalent by the following argument due to Martin Escardo. Let DML refer to the second, truncated version.

###### Lemma

DML implies weak? excluded middle?:

$\prod_{A} \neg A + \neg\neg A.$

Note that truncation or its absence is irrelevant in WEM, since $\neg A$ and $\neg\neg A$ are mutually exclusive so that $\neg A + \neg\neg A$ is always a proposition.

###### Proof

Let $B=\neg A$ in DML, and notice that $\neg(A\wedge \neg A)$ always holds.

###### Lemma

WEM implies that binary sums of negations have split support:

$\prod_{A,B} \Vert \neg A + \neg B \Vert \to (\neg A + \neg B).$
###### Proof

By WEM, either $\neg A$ or $\neg\neg A$. In the first case, $\neg A + \neg B$ is just true. In the second case, either $\neg B$ or $\neg\neg B$. In the first subcase, $\neg A + \neg B$ is again just true. In the second subcase, we have $\neg\neg A$ and $\neg\neg B$, whence $(\neg A + \neg B) = 0$ and in particular is a proposition.

###### Theorem

DML implies untruncated-DML,

$\prod_{A,B} \neg(A \wedge B) \to (\neg A + \neg B)$
###### Proof

Combine the two lemmas.

Created on September 2, 2014 at 12:44:56. See the history of this page for a list of all contributions to it.