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
For myself, the short answer is I don't know. Perhaps I ought to, since I've made lots of geometric theries out of classical ones, but in practice the problem goes further than a strict answer to the question would provide. One often needs not just to transform the theories within a fixed language but to tranform the language itself. A simple example is negation as "cared-for particular" to use Bill's phrase. It is especially true once one starts using the full geometric logic, with infinitary disjunctions (unlike the coherent logic in Mac Lane and Moerdijk). One then sees, for instance, that geometric logic is actually weak second order, with universal quantification bounded over finite sets. Steve Vickers. http://www.doc.ic.ac.uk/~sjv/