Yes, this question is disussed in Kieslers' paper on "Generalized Atomic Formulas" from the early 1960s. The third name , which I prefer, for the class is simply "positive" formulas. They are of course a key tool in the Presentations of a Positive Theory. This may not agree exactly with some previous uses of the term "positive", since the not-so-innocuous use of universal prefixes has been eliminated along with the excessive burden that had been put on the single element "TRUE"; the presentation machinery for positive theories must involve a BINARY relation of entailment (for each admitted arity of formula) in place of the single 0-ary relation of provability. This is actually a simplication rather than a complication although that may not have been clear in the 1930s As far as expressive power is concerned, one can say that for Boolean models (as opposed to models in more general toposes) positive theories are as general as what have been called "standard presentation first order theories" : Any particular negation occurring in a presentation of one of the latter can be replaced by a new primitive relation symbol, nailed to what it is to negate by the usual pair of lattice (hence positive) new axioms. The geometric role of positive theories is that via the classifying-topos construction they provide a standard way to geometrically visualize models of arbitrary theories via the algebraic-geometry paridigm (ie via the body of mathematics created by Kan, Isbell, Grothendieck, and Yoneda in the decade 1954-1964). Of course, one of the theories which most interested the model theory pioneers Birkhoff, Robinson, and Tarski was the theory of commutative rings, so this extension may seem as natural to us as it did to them. Kiesler's paper shows us that the explicit relation between positivity and preservation under morphisms was recognized clearly quite a long time ago. Are there papers which also draw the conclusion that the "standard" theories and presentations should really be the positive ones, with negation as a cared-for particular rather than a blanket general ? Whether the possibility of recursive presentability of a given mathematical concept might vary under this change is not clear to me.(Of course "quantifier elimination" in some cases changes to an exceptional "quantifier definability"). Also, the original question concerning whether (for example) the inclusion, of a positive theory into the associated theory in the doctrine which has negation and universal quantifiers, is itself recursive qua inclusion, probably has a negative answer, but I don't have a reference. Bill ******************************************************************************* F. William Lawvere Mathematics Dept. SUNY wlawvere@acsu.buffalo.edu 106 Diefendorf Hall 716-829-2144 ext. 117 Buffalo, N.Y. 14214, USA ******************************************************************************* On Tue, 2 Mar 1999, Karel Stokkermans wrote:

Dear category theorists,

Recently I came across geometric formulae (built up from atomic formulae using only conjunction, disjunction and existential quantification). I would know like to know whether there is any way to decide whether an arbitrary given first order formula is (classically) equivalent to a geometric formula (or geometric axiom: phi -> psi where phi and psi are both geometric formulae). I've looked in the book by Mac Lane and Moerdijk but didn't discover a general decision method. Any hints or references to relevant literature would be much appreciated.

Best regards, Karel Stokkermans