Re: hyperdoctrines and cylindric algebras

["Zinovy Diskin" <zdiskin@cs.toronto.edu>]

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