A short sequel to EWD 863
 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.