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 | |
| [ ¬P ∧ ¬Q ≡ ¬( P ∨ Q ) ] | (26) |
| follows readily from (25). |