< [[nlab: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. +-- {: .un_lemma} ###### Lemma DML implies [[weak excluded middle|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} ###### Proof Let $B=\neg A$ in DML, and notice that $\neg(A\wedge \neg A)$ always holds. =-- +-- {: .un_lemma} ###### 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} ###### 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. =-- +-- {: .un_theorem} ###### Theorem DML implies untruncated-DML, $$ \prod_{A,B} \neg(A \wedge B) \to (\neg A + \neg B) $$ =-- +-- {: .proof} ###### Proof Combine the two lemmas. =--