From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3066 Path: news.gmane.org!not-for-mail From: Robert Seely Newsgroups: gmane.science.mathematics.categories Subject: Re: intuitionism and disjunction Date: Fri, 3 Mar 2006 15:20:49 -0500 (EST) Message-ID: References: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: ger.gmane.org 1241019076 7113 80.91.229.2 (29 Apr 2009 15:31:16 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:31:16 +0000 (UTC) To: Categories List Original-X-From: rrosebru@mta.ca Fri Mar 3 17:00:13 2006 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 03 Mar 2006 17:00:13 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52) id 1FFHLE-0002Ed-31 for categories-list@mta.ca; Fri, 03 Mar 2006 16:57:36 -0400 In-Reply-To: Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 12 Original-Lines: 47 Xref: news.gmane.org gmane.science.mathematics.categories:3066 Archived-At: On Fri, 3 Mar 2006, Paul B Levy wrote: > Admittedly, if we follow John's suggestion of weakening beta-eta laws into > morphisms a la Neil Ghani, then we won't need a bi-ccc any more. All I am > saying is that, *if* we require the eta law for function types, then we > should also require it for sum types. A couple of remarks about this. First the trivial one: "bi-ccc" is a misleading term (I've used it myself, with the same confusion induced in others), when all you mean is a ccc with coproducts. More importantly, when you look at the structure of proofs in intuitionist logic, you find that sum and product are not really dual - though I have to admit this is very much a matter of presentation. The problem is an old one: Zucker (in the early 70's I think) pointed out that normalization steps are not the same as cut elimination steps, particularly for disjunction. I looked at this in my 1977 thesis, using natural deduction (in the Gentzen-Prawitz formulation) for the logic (this has the advantage over the sequent calculus of giving a category without need for any equivalence relation on derivations). Taking eta and beta (one an expansion, the other a reduction) as 2-cells, I looked at the 2-categorical structure of the connectives (and quantifiers, though really forall and exists are very similar respectively to conjunction and disjunction, not surprisingly). It's easy to see that conjunction is a weak adjoint without any further structure, but disjunction is NOT - unless you add some permuting conversions (equivalences): in fact exactly the permuting rewrites Prawitz had already identified earlier. And function types are a mess in this setting, unless you make the conjunction a real product (again by introducing equivalences - this time just beta and eta). You can find a sketch of all this in two extended abstracts I published: one in the Durham 1977 Category Meeting ("Applications of sheaves ...", SLNM 753), and the other in LICS 1987. (Both are available on my webpage.) (BTW - this was all done long before Ghani looked at the matter ... Barry Jay also subsequently looked at this. But the higher dimensional structure of intuitionist logic is still largely un-studied, and merits serious attention.) -= rags =- --