A [**geometric theory**](https://ncatlab.org/nlab/show/geometric%20theory) is made up of sequents of restricted form: It may only be of the form $$\phi \vdash \psi$$
possibly with free variables (which are implicitly taken universal closure). $\phi, \psi$ are *geometric formulae* which can only involve $\top, \bot, =, \exists, \wedge$ (binary conjunction) and $\bigvee$ (arbitrary disjunction). Geometric theories enjoy some good properties. In particular, it plays well with *geometric morphisms*, hence the name.


My question is: **is there a (complete, sound) deductive system that involves *only* geometric sequents**? I think we can do this just by writing down the obvious rules. But I'm not familiar with infinitary disjunction. I'm also not quite sure once it gets to the predicative logic part.


Is there any existing work on this? An answer or a pointer to relevant material is welcome.



Deductive system involving only geometric sequents
For geometric theories in a countable fragment, (axiomatized by countably many sequents where the disjunctions are also countable), there exists a sound and complete system that appears already in Makkai and Reyes "First-order categorical logic". In page 159, it is described in the section "Completeness of a one-sided system for coherent logic". One should be aware that what Makkai and Reyes called there "coherent" is what we call now "geometric". Also, although they use a Gentzen style sequent calculus, their system is easily seen to be equivalent to the system of geometric logic through sequents as described in the question, which appears, e.g. in Johnstone's "Sketches of an Elephant" section D1.3


If one removes the countability condition, then the system is no longer complete for usual set models but there is still a completeness theorem in terms of models in toposes (and, in fact, in terms of Boolean-valued models). In the same book Makkai and Reyes also treat these cases.


If one insists in having a complete system in terms of set models even when the theory has $\kappa$ sequents for some uncountable $\kappa$, the workaround is to relax the notion of geometric formula to that of a $\kappa$-geometric formula, in which conjunctions are not necessarily finitary, but of size less than $\kappa$. These are preserved by the $\kappa$-geometric morphisms, which are those geometric morphisms whose inverse image additionally preserves all $\kappa$-small limits. The deductive system in this case features a new infinitary rule and is described in my paper "Infinitary generalizations of Deligne's completeness theorem", The Journal of Symbolic Logic, volume 85, Issue 3, pp. 1147 - 1162.


