Re: Horizontal line notation.

Re: Horizontal line notation.

[Jeff Egger]

Just to set the record straight...

> The horizontal line notation was introduced by Gerhard Gentzen in his
> logical sequent calculus. If a set of formulas S  implies a and b, then S
> implies a/\b and vice-versa which was written as:
>
> S |- a,b
> ______
> S |- a/\b

That's not quite correct: Gentzen uses
  a,b,... |- x,y,...
to mean "(a and b and ...) entails (x or y or ...)".
So what you have written is (if interpreted strictly
according to Gentzen's sequent calculus)
  if "S entails (a or b)" then "S entails (a and b)"
which is obviously incorrect.

What Gentzen would write is this:
S |- a       S |- b
-------------------
     S |- a/\b
(if "S entails a" and "S entails b", then "S entails
(a and b)"); he would also write (separately)
S |- a/\b
---------
 S |- a
(if "S entails (a and b)", then "S entails a") and
(again separately)
S |- a/\b
---------
 S |- b
(if "S entails (a and b)", then "S entails b").

The point here is that Gentzen did not actually intend
his  horizontal line notation to represent any sort of
bijection.  In fact, I rather suspect that he borrowed
the line from elementary-school arithmetic:
  24
  73
  92
----
 189.

[The only reason for writing
S |- a       S |- b
-------------------
     S |- a/\b
instead of
 S |- a
 S |- b
---------
S |- a/\b
is in case you want to append proofs of S |- a and
S |- b.  In this manner one represents (complete)
proofs as trees, where the leaves are axioms, and
the root is the theorem being proven.]

But I don't think the fact that Gentzen did not intend
this horizontal line notation to represent the bijection
which is obviously there should stop us from doing it:
it's a very convenient way of discussing adjunctions,
and there is as little chance of confusing the older
use of this symbol with the newer one as confusing
either with elementary school arithmetic.

Cheers,
Jeff.

Re: Horizontal line notation.

[Vaughan Pratt]

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

Re: Horizontal line notation.

[Mike Stay]

On Tue, Mar 17, 2009 at 5:28 AM, Jeff Egger <jeffegger@yahoo.ca> wrote:
>
> Just to set the record straight...
>
>> The horizontal line notation was introduced by Gerhard Gentzen in his
>> logical sequent calculus. If a set of formulas S  implies a and b, then S
>> implies a/\b and vice-versa which was written as:
>>
>> S |- a,b
>> ______
>> S |- a/\b
>
> That's not quite correct: Gentzen uses
>  a,b,... |- x,y,...
> to mean "(a and b and ...) entails (x or y or ...)".
> So what you have written is (if interpreted strictly
> according to Gentzen's sequent calculus)
>  if "S entails (a or b)" then "S entails (a and b)"
> which is obviously incorrect.
>
> What Gentzen would write is this:
> S |- a       S |- b
> -------------------
>     S |- a/\b
> (if "S entails a" and "S entails b", then "S entails
> (a and b)"); he would also write (separately)
> S |- a/\b
> ---------
>  S |- a
> (if "S entails (a and b)", then "S entails a") and
> (again separately)
> S |- a/\b
> ---------
>  S |- b
> (if "S entails (a and b)", then "S entails b").
>
> The point here is that Gentzen did not actually intend
> his  horizontal line notation to represent any sort of
> bijection.  In fact, I rather suspect that he borrowed
> the line from elementary-school arithmetic:
>  24
>  73
>  92
> ----
>  189.
>
> [The only reason for writing
> S |- a       S |- b
> -------------------
>     S |- a/\b
> instead of
>  S |- a
>  S |- b
> ---------
> S |- a/\b
> is in case you want to append proofs of S |- a and
> S |- b.  In this manner one represents (complete)
> proofs as trees, where the leaves are axioms, and
> the root is the theorem being proven.]
>
> But I don't think the fact that Gentzen did not intend
> this horizontal line notation to represent the bijection
> which is obviously there should stop us from doing it:
> it's a very convenient way of discussing adjunctions,
> and there is as little chance of confusing the older
> use of this symbol with the newer one as confusing
> either with elementary school arithmetic.
>
> Cheers,
> Jeff.
>


The turnstile |- can be viewed as the hom functor (which in a poset is
a truth value), while the horizontal bar is a (di)natural
transformation.  A double bar is a natural isomorphism.  An empty
"numerator" is the constant bifunctor T:C^op x C -> Set that picks out
the one-element set.

So, for example, we have

------ (id)
X |- X

which is a dinatural transformation from T to (X, X); the
corresponding commuting hexagon says that the identity is a left and a
right unit.

Y |- Z     X |- Y
----------------- (cut)
     X |- Z

is a transformation that's natural in X, Z and dinatural in Y.  The
commuting hexagon says that composition is associative.

Currying is usually written as two rules, one for introduction of -o
(linear implication = internal hom) and one for eliminating it.  But
it's equivalent to use this natural isomorphism:

X, Y |- Z
=========== (curry)
X |- Y -o Z

which is an adjunction.
-- 
Mike Stay - metaweta@gmail.com
http://math.ucr.edu/~mike
http://reperiendi.wordpress.com

Re: Horizontal line notation.

[Toby Bartels]

David Ellerman wrote in part:

>The horizontal line notation was introduced by Gerhard Gentzen in his
>logical sequent calculus. If a set of formulas S  implies a and b, then S
>implies a/\b and vice-versa which was written as:

 S |- a,b
 _________
 S |- a/\b

>Going from top to bottom was conjunction-introduction, and going in the
>other direction was conjunction-elimination.

But much of sequent calculus is irreversible.
If nothing else, structural rules such as weakening:

   S |- b
 --------
 S:a |- b

where S:a is the list or set S followed by a.
(Thank all the Haskell recently for making me write it like this.)
This is valid downwards, but not upwards.

I see sequent-calculus people using a double line if it's good both ways:

   S |- a=>b
 ===========
 S:a |- b

(This is a propositional version of the example in the original question.)

Incidentally, your first example I would write as

 S |- a;   S |- b
 ================
 S |- a/\b

because if you have a set, such as {a,b}, of propositions on the right,
then this is interpreted disjunctively (not conjunctively as on the left).
But I suppose that you can be lax about this if you agree beforehand
that you'll only be doing "intuitionistic" sequents
(that is those with only one statement on the right).


--Toby

Re: Horizontal line notation.

[PETER EASTHOPE]

Apologies for the faulty messages.

Eleven replies!  Thanks to everyone.

Two obvious benefits: a line is easier to
type and occupies less space than a vertical
arrow.

Ross Street wrote,
"It means there is a natural bijection. ..."

Micah Blake McCurdy wrote,
"... The notation itself goes back to Gentzen, I think, but the meaning was
not the same there -- he meant that the implication below the line
could be deduced from the implication above the line."

Andrej Bauer wrote,
"In logic ... you put a double horizontal
line if you want to emphasize that the
rule goes both ways."

So in Cat. Th., a single line might represent
an arrow while a double line would represent
a bijection?  Apparently this convention
isn't well established.

Regards,       ... Peter E.

-- 
http://members.shaw.ca/peasthope/
http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/

Re: Horizontal line notation.

[David Ellerman]

The horizontal line notation was introduced by Gerhard Gentzen in his
logical sequent calculus. If a set of formulas S  implies a and b, then S
implies a/\b and vice-versa which was written as:

S |- a,b
______
S |- a/\b

Going from top to bottom was conjunction-introduction, and going in the
other direction was conjunction-elimination. After Lawvere noted that these
Gentzen rules were simple adjunctions, he started writing all adjunctions
using this Gentzen-style notation with the two adjoint transposes on top and
on bottom and the arrow replacing the turnstile ( |- ) symbol. The notation
caught on.


__________________
David Ellerman

Visiting Scholar
University of California at Riverside

Email: david@ellerman.org
Webpage: www.ellerman.org

View my social science research on my SSRN Author page:
http://ssrn.com/author=294049

View my mathematics research at:
http://arxiv.org/find/math/1/au:+Ellerman_D/0/1/0/all/0/1

Now out in paperback: Helping People Help Themselves: From the World Bank to
an Alternative Philosophy of Development Assistance. University of Michigan
Press. 2006. For more information, see the table of contents:
http://www.ellerman.org/Davids-Stuff/Books/NEW%20RELEASE%20NOTICE.pdf . Book
available at better booksellers online.


-----Original Message-----
From: categories@mta.ca [mailto:categories@mta.ca] On Behalf Of PETER
EASTHOPE
Sent: Sunday, March 15, 2009 8:36 AM
To: categories@mta.ca
Subject: categories: Horizontal line notation.

Lawvere & Schanuel use a horizontal line notation.  Page 326 for example.

X --> 1^T
---------
TxX --> 1

This is unfamiliar.  Does the line have a name?  How is it read?  I'll guess
either "(X --> 1^T) is equivalent to (TxX --> 1)"
or
"(X --> 1^T) is isomorphic to (TxX --> 1)".

Thanks,     ... Peter E.

--
http://members.shaw.ca/peasthope/
http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/

Re: Horizontal line notation.

[Miles Gould]

On Sun, Mar 15, 2009 at 07:35:37AM -0800, PETER EASTHOPE wrote:
> Lawvere & Schanuel use a horizontal line
> notation.  Page 326 for example.
>
> X --> 1^T
> ---------
> TxX --> 1
>
> This is unfamiliar.  Does the line have a
> name?  How is it read?

It's read "(X --> 1^T)" is the transpose of (TxX --> 1)", but I'm not
aware of a name for the line itself. This is reasonably standard
notation, by the way.

Miles

-- 
Besides, don't think aircraft carrier, think mecha. The type
system is a great amplifier of careful reasoning and propagator of
intent. If somebody starts muttering about bondage, just tell them
"those straps are there so the servos can follow *me*".
  -- skew, on #haskell

Horizontal line notation.

[PETER EASTHOPE]

Lawvere & Schanuel use a horizontal line
notation.  Page 326 for example.

X --> 1^T
---------
TxX --> 1

This is unfamiliar.  Does the line have a
name?  How is it read?  I'll guess either
"(X --> 1^T) is equivalent to (TxX --> 1)"
or
"(X --> 1^T) is isomorphic to (TxX --> 1)".

Thanks,     ... Peter E.

-- 
http://members.shaw.ca/peasthope/
http://carnot.yi.org/ = http://carnot.pathology.ubc.ca/