Re: hyperdoctrines and cylindric algebras

Re: hyperdoctrines and cylindric algebras

[Thomas Streicher]

Couldn't one say that cylindric (and polyadic) algebras are awkward (from a
categorical point of view) formulations of posetal hyperdoctrines over
FinSet^op whose fibres are boolean algebras. So the pet objects of the
algebraic logicians are certain *presentations* of particular hyperdoctrines.
All this was worked out in a couple of papers by A. Daigneault beginning
of 70ies.
There is a lot of work by the algebraic logicians which I am not too familiar
with. There arises the question whether their work is of any use for questions
naturally arising to the categorical logician. That's how I understood Alex'
question and what I'd like to know myself.
Halmos was one of the first working on algebraic logic in the 50ies (polyadic
algebras) and was later positive w.r.t. categorical logic. That's what I have
heard of. Did he consider categorical logic as the "right formulation" of his
original aims? Maybe senior categorists do know about this?

Thomas

Re: hyperdoctrines and cylindric algebras

[Zinovy Diskin]

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

hyperdoctrines and cylindric algebras

[Alexander Kurz]

There clearly is a connection between hyperdoctrines and cylindric
algebras.

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

I would be greatful for any reference or comment.

Best wishes,

Alexander