Re: hyperdoctrines and cylindric algebras (Correction)

[Bill Lawvere <wlawvere@buffalo.edu>]

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).
>

...