On 5/23/07, Alexander Kurz <kurz@mcs.le.ac.uk> wrote:

There clearly is a connection between hyperdoctrines and cylindric algebras.

yes, of course. Roughly speaking, they are equivalent: hyperdoctrines (HDs) are indexed category style algebraization of first order logic while cylindric algebras (CAs) are an equivalent fibrational formulation. To make it precise, we need to consider a few rather straightforward yet technically bulky generalizations of both notions, reproducing in HDs the classical context of CAs and vice versa. I'm traveling and do not have references at hand, but below is an outline of how it can be done (apologies for possible inaccuracies).

Does anybody knows work that relates the two? Or that makes use of a result from one area to prove something in the other?

The last question is interesting. If we are speaking about pure algebra, there is nothing exciting in "switching" between HDs and CAs: these are just different representation of the same algebraic theory. More accurately, HDs are equivalent to locally finite CAs, which are not equationally definable. Thus, HDs are much more manageable algebraically (but many-sorted). This trade-off between number of sorts and equational definability is probably the most/only interesting algebraic point. However, the main driving force of CA development was in the representation theorems, which are for CAs are much more intricate than Stone representation theorems for Boolean algebras. In the companion volume to the classical monograph by Henkin, Monk,Tarsky (where the great trio is joined by Andreka & Nemeti), there is a lot of interesting and not-easy-to-prove representation theorems (googling Andreka-Nemeti should provide references). I'm not aware of any similar results (or even interest in such results) for HDs. ZD == 8< == equivalence of HDs and CAs: a rough outline Let's fix a countable set V (of variables). Consider a simple version of the notion of hyperdoctrine, p:T-->BA^op is an indexed cat, where T=Pow_fin(V) is the category of finite subsets of V and mappings between them and BA is the category of Boolean algebras. Now we apply to p the Grothendieck construction and get a fibration \delta: G-->T. A straitforward check shows that G is a locally finite cylindric algebra (CA). (Special axioms regulating interactions of substitutions and bound variables hold because of Beck-Chevalle and Frobenius conditions). Conversely, if A is a locally finite cylindric algebra over V and a\in A, define \delta(a) = {x \in V| C_x(a) not= a} (C_x is cylindrification operator/quantifier). As a Boolean algebra, A is an order category and \delta is a fibration. Its indexed version gives an HD over a trivial algebraic theory (and with Boolean fibres). To get an equivalence result for non-trivial algebraic theories, the notion of CA over a variety was introduced (first by Boris Plotkin for Halmos' polyadic algebras, and then by Janis Cirulis for CAs). To extend equivalence for the classical HDs where fibres are intuitionistic, we need the notion of cylindric Heyting algebras. To extend the equivalence for CAs that are not locally finite, we need HDs over Ts being cats with any products (not necessary finite). Another version of equivalence results can be obtained if we replace CAs by polyadic algebras introduced by Halmos. One more delicate point is that CAs are equivalent to polyadic algebras with equality while there are also polyadic algebras without equality. Such things were popular at Riga algebraic seminar about twenty years ago. I think that then I wrote a preprint where all this was carefully formulated; hopefully, I still have a hard copy (never thought that anybody would need it :).

I would be greatful for any reference or comment.

Best wishes,

Alexander