Homotopy Type Theory
de Morgan's law (changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

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.

Lemma

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.

Proof

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

Lemma

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).
Proof

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.

Theorem

DML implies untruncated-DML,

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