The axiom De Morgan’s Law says that for any and , if not ( and ), then (not ) or (not ). 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 , in the statement of DML we might as well assume and to be propositions. However, it is not quite as obvious whether it matters if the “or” is truncated or not, in other words whether
is equivalent to
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:
Note that truncation or its absence is irrelevant in WEM, since and are mutually exclusive so that is always a proposition.
Let in DML, and notice that always holds.
WEM implies that binary sums of negations have split support:
By WEM, either or . In the first case, is just true. In the second case, either or . In the first subcase, is again just true. In the second subcase, we have and , whence and in particular is a proposition.
DML implies untruncated-DML,
Combine the two lemmas.
Revision on September 2, 2014 at 12:44:56 by Mike Shulman. See the history of this page for a list of all contributions to it.