I'm afraid that still some clarification is needed. Standard hyperdoctrines (HDs) and standard cylindric algebras (CAs) are not equivalent by the following two groups reasons. (1) How we model logic/predicates. In HDs, objects in fibers are predicates of finite arities, the logic is intuitionistic and we are interested in proofs (arrows) rather than just provability (partial order). In CAs (of dimension \alpha = enumeration of some predefined set of variables), elements are to be thought of as predicates of arity \alpha, the logic is classical and we are interested in the partial order of provability (CAs are Boolean algebras with an extra structure). (2) How we model algebra/terms. In an HD T-->Cat^op, the algebraic base T is an *arbitrary* finitary algebraic theory. In CAs, the algebraic base is *the trivial* finitary algebraic theory over \alpha, whose only operations are projections. The difference is quite evident , and I believe that the actual question was not about the difference but rather about how to figure out the commonalities (and formulate equivalence if it can be formulated). Result 1: adjusting HDs to CAs and PAs (polyadic algebras). The following three notions are equivalent: -- locally finite CA (of dimension \omega), -- locally finite PA with equality, -- HD, whose fibers are Boolean algebras and the algebraic base has no morphisms other than projections. The condition of being locally-finite can be removed if we define HDs over algebraic bases having countable (rather than just finite) products. Result 2: adjusting CAs/PAs to HDs. The following three notions are equivalent: -- HD, whose fibers are posets, -- locally finite "polyadic Heyting algebra" with equality over a variety, -- locally finite "cylindric Heyting algebra" over a variety. Many similar equivalence results in-between and around the two above can be formulated. Roughly, anything that can be defined for poset HDs in the fibred fashion, can be reproduced for CA/PAs in the globalistic fashion (via the Grothendieck construction) and vice versa. However, the HD formalism is much more flexible as can be seen already from the two results above. Result 1 is conceptually and technically easy. Result 2 is equally easy conceptually but is much more intricate technically. Defining polyadic Heyting algebras needs a certain technical work, which is essentially nothing but reproducing the basic Lawvere's observation of quantifiers as adjounts in the global Heyting algebra setting. In general, the notion of CA of an infinite dimension is conceptually messy: elements are predicates of infinite arities while quantifiers and variable substitutions are finitary (and even worse, substitutions are not a basic notion and need to be derived via diagonals, see Janis Cirulis' papers. But once again, the main concern of developing CAs was to algebraize semantics -- algebras of relations, rather than syntax and proof theory). Halmos' polyadic algebras are conceptually more consistent in this sense (and probably because in their design the syntactical side was taken more seriously) . Despite all these technical differences, HDs are CAs/PAs are close in the sense that they both follow the same basic idea of algebraizing logic: the algebras are generated by signatures and axioms (theories). In a bit more detail: a signature \Sigma of operation and predicate symbols of finite arities freely generates an HD, which is then factorized by the congruence generated by the axioms (in the categorical jargon, the result would be called the classifying HD of the theory). The "classifying" CA can be also generated in this way but not freely because expressing finiteness of the arities needs additional conditions that cannot be captures equationally (it is a well-known fact that the class of locally finite CA of an infinite dimension is not a variety, it is not a quasi-variety too). If we consider signatures in which all symbols have the same countable arity \omega, then the corresponding CA is freely generated by \Sigma (and then factorized by the theory congruence). The main advantage of HDs over locally finite CAs is that the finiteness of the arities is captured equationally (the trade-off is that HDs are algebras over graphs while CAs are algebras over sets). Note that the dimension/set of variables is a parameter in the above. An essentially different way of algebraizing logic is when variables are generators while the signature is a parameter. Semantically it means that a model is an evaluation of variables, another evaluation, even in the same carrier set, is another model. This is how validity of implications is defined. Theories in such logic are congruences (in contrast to Birkhoff's fully invariant congruences, when we talk about the equational logic), and we may call this way of algebraizing logic "congruental" (the term introduced by Blok and Pigozzi in their seminal work on algebraic logic). If Sign denotes a category of signatures and Log is a category of logics algebraically defined in a suitable way, then the HDs/CAs' way of algebraizing logic can be presented as a binary functor Sign x Set^op --> Log (signature elements are generators, the set of variables is a parameter). In congruental logic, we have a dual situation described by a functor Set x Sign^op --> Log (variables are generators, the signature is a parameter). Details can be found in my paper http://www.cs.toronto.edu/~zdiskin/Pubs/WAAL-97.pdf full of conjectures (deep insights are also possible :-). Zinovy On 5/28/07, Bill Lawvere <wlawvere@buffalo.edu> wrote:

Hyperdoctrines (in many variants) were introduced as an algebraic aspect of "proof theory" and as such are definitely not equivalent to cylindric algebras (or polyadic algebras or even various categorical formulations of logic). They involve fibered categories whose fibers are cartesian closed (and with adjoints between the fibers etc.). The poset reflection of these fibers are Heyting algebras. This reflection process was intuited already by Curry and was later called "the Curry-Howard isomorphism" even though this is a serious misnomer because it is very far from being an isomorphism.

(See my paper Adjoints in and among bi-categories, Logic & Algebra, Lecture Notes in Pure and Applied Mathematics. 180:181-189. Ed. A. Ursini, P Agliano, Marcel Dekker, Inc. Basel, 1996, as well as the author's commentary on my paper Adjointness in Foundations, as reprinted in TAC. Recent papers of Matias Menni further clarify these developments, which were partly inspired by work of Hans Laeuchli.)

Conceptually, the problem of presentation of a theory in algebraic logic by means of primitive predicates and axioms can be viewed as taking place in two steps: first the presentation of a hyperdoctrine with non-trivial fibers, and then the further collapse by imposing the condition that projection maps act as inverse to diagonal maps (within each fiber). This process can be localized. The problematic existential quantifier which is the core problem of proof theory: ("there exists a proof of ....") is thus split into several parts to be studied separately.

I hope the above helps to clarify the relationship between two levels of categorical algebra.

Bill

************************************************************ F. William Lawvere, Professor emeritus Mathematics Department, State University of New York 244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA Tel. 716-645-6284 HOMEPAGE: http://www.acsu.buffalo.edu/~wlawvere ************************************************************