Subject: categories: Re: geometric formulae and axioms

From: [email-masked] (Steven Vickers)
Date: Fri, 5 Mar 1999 10:15:45 +0000

>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/