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
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
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
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
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. 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. public. formulation the idea is probably due to Prawitz. Best, Grisha