From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3771 Path: news.gmane.org!not-for-mail From: Bill Lawvere Newsgroups: gmane.science.mathematics.categories Subject: Re: hyperdoctrines and cylindric algebras (Correction) Date: Mon, 28 May 2007 16:03:49 -0400 (EDT) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Trace: ger.gmane.org 1241019512 10212 80.91.229.2 (29 Apr 2009 15:38:32 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:38:32 +0000 (UTC) To: categories Original-X-From: rrosebru@mta.ca Tue May 29 06:08:13 2007 -0300 X-Keywords: Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 29 May 2007 06:08:13 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1HsxfH-0000eq-8S for categories-list@mta.ca; Tue, 29 May 2007 06:06:51 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 65 Xref: news.gmane.org gmane.science.mathematics.categories:3771 Archived-At: 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 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). > ...