Is there any known Unicode character which can be used as a substitute for the horizontal line which is normally used in texts presenting sequent calculus?
I actually use the oblique bar /, which I believe is a reasonable substitute as it stands for the division (at least in several countries) which recalls the horizontal line of fractions.
Example: Γ ⊢ t = s, Δ ⊢ t = u / Γ ∪ Δ ⊢ s = u
However, I would like to know if there is a better alternative, and if possible, a standard alternative. Searching the web did not help.
Extra question: was a proper name ever given to this horizontal line?
(1) To take the extra question first: "inference line" is, I think, the usual term for the horizontal line used in Gentzen-style layouts for natural deduction or for sequent proofs. (Thus, Jan von Plato, in his recent Elements of Logical Reasoning, p. 21)
(2) The inference line, then, marks an inference. And, speaking for myself, one way I'd read out loud the inference
$$\underline{\Gamma \vdash t = s \quad \quad \quad \Delta \vdash t = u}\\ \Gamma \cup \Delta \vdash s = u$$
written on the blackboard in a lecture is the same as if I'd written
$${\Gamma \vdash t = s, \Delta \vdash t = u} \ \therefore\ \Gamma \cup \Delta \vdash s = u$$
So I guess you could use $\therefore$ as an alternative to $/$ if on a particular occasion you wanted to write things on one line. But why do so? It seems we rarely need to: flicking through a couple of proof theory books from my shelves, I can't find any usage of the inline version. (Maybe I've not look hard enough.)
(3) Things we get hairy anyway as soon as you try to chain inferences. Thus consider.
$$\underline{\Gamma \vdash t = s \quad \quad \quad \Delta \vdash t = u} \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \quad \\ \underline{\Gamma \cup \Delta \vdash s = u\quad\quad\quad\quad\quad\quad \Gamma \cup \Delta \vdash Fs}\\ \Gamma \cup \Delta \vdash Fu$$
Even writing something as simple as this in one line is not wonderfully readable, and complications soon escalate as we try to linearise more complex proofs. So there's a good reason for the traditional layout. And you can easily typeset it using Bussproofs or other packages, see http://www.logicmatters.net/latex-for-logicians/nd/