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