Re: Horizontal line notation.

[Vaughan Pratt <pratt@cs.stanford.edu>]

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