1096

Potter’s proof of disjunction’s symmetry

EWD1096 · 1987–1991 · PDF · source transcription · Source language: English.

Dr. Walter M. Potter of Southwestern University, Georgetown, TX 78626, taught me that the symmetry of the disjunction can be derived from my other axioms:

        P ≡ Q
=         {idempotence of ∨}
        (P ≡ Q) ∨ (P ≡ Q)
=         {∨ distributes forwards over ≡}
        (P ≡ Q) ∨ P ≡ (P ≡ Q) ∨ Q
=         {∨ distributes backwards over ≡, twice}
        P ∨ P ≡ Q ∨ P ≡ P ∨ Q ≡ Q ∨ Q
=         {idempotence of ∨, twice}
        P ≡ Q ∨ P ≡ P ∨ Q ≡ Q       ;

From the first and the last line (and the properties of ≡) follows
        [Q ∨ P ≡ P ∨ Q]      .

Q.E.D.

Austin, 4 March 1991

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