Homotopy Type Theory
de Morgan's law

The axiom De Morgan’s Law says that for any AA and BB, if not (AA and BB), then (not AA) or (not BB). 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 AA and BB to be propositions. However, it is not quite as obvious whether it matters if the “or” is truncated or not, in other words whether

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

is equivalent to

A,B¬(AB)¬A+¬B. \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.


DML implies weak? excluded middle?:

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

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


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


WEM implies that binary sums of negations have split support:

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

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


DML implies untruncated-DML,

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

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.