Karel Stokkermans asked about a decision procedure for checking whether an arbitrary given first-order formula is classically equivalent to a geometric one. There is no such algorithm. The reason is that any such algorithm could easily be converted into an algorithm for testing (classical, first-order) validity, which is well-known to be undecidable. To test a formula A for validity, take a 0-ary predicate symbol P that doesn't occur in A, and let A' be the formula "A or not P". Then A' is equivalent to a geometric formula (namely "true") if and only if A is valid. So just test A' for geometricity and you'll know whether A is valid. (If, like some textbook authors, you don't believe in 0-ary predicate symbols, use P(x) instead, where P is unary.) Bill Lawvere asked whether there are "papers which also draw the conclusion that the 'standard' theories and presentations should really be positive ones, with negation as a cared-for particular rather than a blanket general". I assume he means papers where this is done for a purpose other than having geometric theories or the nice things that come with them, like classifying topoi. In a paper that Yuri Gurevich and I wrote long ago ["Existential fixed-point logic" in "Computation Theory and Logic", edited by Egon Boerger, Springer Lecture Notes in Comp. Sci. 270 (1987) pp.20-36], we found it convenient to adopt the following convention, which though not quite what Bill described, is similar in spirit: A first-order language (or signature or similarity-type) should have its predicate symbols classified into two sorts, positive and negatable. Negation can be applied only to atomic formulas whose predicate symbol is negatable. Homomorphisms are required to preserve the interpretations of all predicate symbols and to reflect the interpretations of the negatable ones. Andreas Blass