From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/182 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: Horizontal line notation. Date: Thu, 19 Mar 2009 15:08:02 -0700 Message-ID: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1237513219 24368 80.91.229.12 (20 Mar 2009 01:40:19 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 20 Mar 2009 01:40:19 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Fri Mar 20 02:41:36 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1LkTjp-0006tU-5v for gsmc-categories@m.gmane.org; Fri, 20 Mar 2009 02:41:33 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LkT8a-0002Kj-Po for categories-list@mta.ca; Thu, 19 Mar 2009 22:03:04 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:182 Archived-At: Mac Lane corresponded with Mints nearly three decades ago on the relationship between coherence and proofs. One manifestation of the connection is as the often-mentioned Curry-Howard isomorphism. More recently Kosta Dosen and Zoran Petric have written at length about the relationship in their 2004 book Proof-Theoretical Coherence. I asked Grisha a few questions to see if he felt any of Gentzen's work suggested categorical intuitions, which he answered as follows, essentially in the negative: the connections came much later. (I was surprised by his statement that the sequent calculus is not close to adjunctions, given that the adjoints of the diagonal functor correspond so well to introduction and elimination of logical connectives, and likewise for quantifiers. I'll ask him about that next time I see him, which may be a couple of weeks since we're in Spring break, at which point van Benthem may be here. Grisha's suggestion to ask Prawitz is a good one.) Vaughan -------- Original Message -------- Subject: categories and Gentzen systems Date: Wed, 18 Mar 2009 12:41:56 -0700 (PDT) From: Grigori Mints gmints at stanford edu Hi Vaughan, you may use these comments as you like. > You and Mac Lane had some interaction on this some time ago. > What's > your understanding of what Gentzen had in mind? MacLane's initial understanding of the connection between categories and logic is summarized in the first of two papers below, his summary of our correspondence is in the second paper. MacLane S. Topology and logic as a sourse of algebra, Bull. Amer. Math. Soc. 82, 1976, no 1, 1-40 MacLane S., Why commutative diagrams coincide with equivalent proofs, in: Contemporary Mathematics, v. 13, 1982, 387-401, American Mathematical Society, Providence MacLane was a graduate stuident in Gottingen at the same time as Gentzen. If Gentzen had some ideas very close to categorical treatment of logical deductions, it seems unlikely to me Mac Lane would forget. > Is it just an accident > that the sequent calculus as conceived by Gentzen turned out to be > convenient to express adjunctions, or did Gentzen independently invent > symmetric monoidal categories? I do not see any analogy in Gentzen's writing, even in very recent publication by Jan von Plato of the first vesrion of Gentzen's dissertation containing quite modern normalization proof for natural deduction. By the way, it is not sequent calculus but natural deduction which is close to formulation in terms of adjunctions. Still there is a significant distance between the latter two, bridged in the work by several authors in the years 1970-1980. > Also what was the interaction if any between Goedel's Dialectica > interpretation of S4 and Gentzen's interpretation of his sequent > calculus? Did either man derive any inspiration of this kind from the > other? You mean Godel's Dialectica interpretation of the intuitionistic logic. It is completely unlikely that Gentzen was not aware of the effective (Brouwer-Heyting-Kolmogorov) interpretation of intuitionistic logical connectives, but again I do not see any evidence of this is his writings. His first consistency proof for arithmetic contains game-theoretic semantics, but that is a different matter. Godel certainly derived some inspiration from Gentzen's writings, he comments about this in detail in Zilsel's report. Gentzen's main work was finished long before the ideas of realizability (Dialectica is one of them) which made BHK interpretation explicit became public. > Does Prawitz have > a view on what Gentzen was thinking that got him (Gentzen) to something > so like category theory? Again, no indication in Prawitz' writings, but you can ask him. He certainly is deeply influenced by Gentzen's idea that the meaning of logical connectives is given by introduction-elimination rules. In this formulation the idea is probably due to Prawitz. Best, Grisha