This is a comment tangential to Michael Barr's message about quantifiers. His 2 1/2 examples can be improved to 3, because the condition he calls complementary to AC also implies classical logic. Recall that this condition reads: (exists x:X) (forall y:Y) f(x,y) iff (forall s: X --> Y) (exists x:X) f(x,s(x)). (*) The left-to-right implication here is trivial, but I claim the right-to-left implication implies (not not u) ==> u and thus Boolean logic. The easiest proof proceeds as follows in the internal logic. Given an arbitrary truth value u , let X={.|u}, i.e., X has at most one element and it's inhabited iff u, and let Y be empty. Then (not not u) implies the right side of (*) [vacuously: the existence of such an s implies not u ], while the left side of (*) implies u . For people who would like to banish the empty set at the cost of some simplicity (universal algebraists?), there is an alternate argument using only inhabited sets. Again, let a truth value u be given, let Y=2, i.e., a set with exactly two, definitely distinct elements, and let X be the quotient of Y in which the two elements have been identified iff u . Let f(x,y) mean that the canonical projection from Y to X sends y to x. Again, one can check that (not not u) implies the right side of (*) and that the left side of (*) implies u. It is curious that the same X, Y, and f as in this second proof are also used for the (internal) proof of Diaconescu's theorem that AC implies classical logic. Andreas Blass ablass@umich.edu