Re: Horizontal line notation.

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

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