HOME

A short sequel to EWD 863

Show original manuscript

In EWD863, I left at the end the derivation of de Morgan's Laws as an exercise to the reader. The following proof, however, is too beautiful to remain unrecorded. I recall —with numbers as in EWD863— the axioms
[ P ∧ Q  ≡  P  ≡  Q  ≡  P ∨ Q ]
(9)
[ P ∨ ¬Q  ≡  P ∨ Q  ≡  P ] (14)
and the theorems
[ ¬¬Q ≡ Q ] (19)
[¬(P ≡ Q) ≡ ¬P ≡ Q ] . (20)

From (14), we derive with P := ¬P and P,Q := Q,P respectively:
[ ¬P ∨ ¬Q  ≡  ¬P ∨ Q  ≡  ¬P ]
[ Q ∨ ¬P  ≡  Q ∨ P  ≡  Q ] ;
from those two with Leibniz's Principle (and symmetry of v and ≡ )
[ ¬P ∨ ¬Q  ≡  ¬P  ≡  Q  ≡  P ∨ Q ] ;
from that one with (20)
[ ¬P ∨ ¬Q  ≡  ¬( P  ≡  Q  ≡  P ∨ Q ) ] ,
and finally with (9)
[ ¬P ∨ ¬Q  ≡  ¬( P ∧ Q ) ] . (25)

With (19) —and [¬P ≡ ¬P], which is a syntactic descendant
of [ P ≡ P ]—
[ ¬P ∧ ¬Q  ≡  ¬( P ∨ Q ) ] (26)
follows readily from (25).

  Austin, 2 Dec. 1984

prof.dr.Edsger W.Dijkstra
Department of Computer Sciences
The University of Texas at Austin
Austin, TX 78712-1188
United States of America

PS. The single substitution P,Q := ¬Q,P into (14), yielding

[ ¬Q ∨ ¬P  ≡  ¬Q ∨ P  ≡  ¬Q ]

would have sufficed in subsequent combination with (14).
(End of PS.) EWD.