Re: hyperdoctrines and cylindric algebras (Correction)

Re: hyperdoctrines and cylindric algebras (Correction)

[Zinovy Diskin]

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

Re: hyperdoctrines and cylindric algebras (Correction)

[Bill Lawvere]

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

...