I would like to comment on Vaughan Pratt's
1. Defense of Choice ... Using Choice lets you prove more theorems, but they also shorten existing proofs, sometimes significantly. There is no shortage of examples,...
Write CD(L) for complete distributivity of a complete lattice L. Write CCD(L) for constructive complete distributivity of L, by which is meant that \/:DL--->L has a left adjoint, where DL is the lattice of down-closed subsets of L, ordered by inclusion. It is easy to show that CD==>CCD but many times in joint work with Fawcett, Rosebrugh and Marmolejo I have been led back to the more interesting AC<==>(CD<==>CCD) * Without choice there is not much that one can prove about CD. In fact, without choice there is a severe shortage of infinite L satisfying CD(L). (Recall that AC is equivalent to `for every set X, CD(PX), where P denotes power set'.) My experience suggests that all theorems about CD follow from constructively proveable theorems about CCD after invoking *. Those that my colleagues and I have discovered have reasonably ``short'' proofs, if one starts with some basic knowledge of adjunctions. Allow me to discharge the facile comment that by *, any theorem that has been proved constructively about CCD (examples exist) proves that ``Using Choice lets you prove more theorems'' because that is not the point of this note. Rather, I think that * and similar results show that some of the definitions and concepts that seem to arise rather ``naturally'' from traditional set-based Mathematics are not particularly natural. Stepping further away from Mathematics, I think that twentieth century Mathematics has frequently sacrificed useful generalization for excessive abstraction. RJ Wood