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 ************************************************************ On Thu, 24 May 2007, Zinovy Diskin wrote:
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).
...