Subject: categories: geometric formulas

From: Andreas Blass <[email-masked]>
Date: Mon, 8 Mar 1999 17:54:20 -0500 (EST)

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