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/
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
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/
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.
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/
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
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
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
participants (7)
-
David Ellerman -
Jeff Egger -
Mike Stay -
Miles Gould -
PETER EASTHOPE -
Toby Bartels -
Vaughan Pratt