EWD 1096

Potter’s proof of disjunction’s symmetry

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:

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

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


Austin, 4 March 1991

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