903

A short sequel to EWD863

EWD903 · 1984–1987 · PDF · source transcription · Source language: English.


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