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