2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I think that there is no substitute for "/" in a "linear" representation of sequent rules (or inference rules in general). Of course, with Latex you may represents them bi-dimensionally (see some example in this site). $\endgroup$ – Mauro ALLEGRANZA Apr 27 '14 at 9:22
  • $\begingroup$ @Mauro ALLEGRANZA, I know about LaTex, however, the question matters precisely in contexts where there is no LaTeX, like with general purpose forums or computer languages, which all favours linear writing and meaning rather than presentation. Thanks for your concern anyway. $\endgroup$ – Hibou57 Apr 27 '14 at 11:04
3
$\begingroup$

(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/

$\endgroup$
  • $\begingroup$ The character is U+2234, whose name is THEREFORE, so that seems to be a good match. Thanks for the mention of this character. For the reason, I commented on this in reply to Mauro ALLEGRANZA. It's a matter only in contexts where there is not support for a “presentational notation” and only in flow linear writing, like general purpose forums and ha‑doc computer notations. In these cases, of course, hairy things are to be avoided. Otherwise, I agree with you it's not the most common case. $\endgroup$ – Hibou57 Apr 27 '14 at 11:18
  • $\begingroup$ This PDF paper, “Mathematical Proof and Computer Science (uchicago.edu)”, uses $\Rightarrow$ for a linear notation of the sequent. At “2.3 Sequent Calculus”, they say “A sequent is of the form $\Gamma \Rightarrow \Delta$ in which $\Gamma$ represents the context or assumptions” (anyway, I still prefer , which I feel is less ambiguous). $\endgroup$ – Hibou57 Jul 27 '14 at 21:22
  • $\begingroup$ For chaining inferences, why not use a combination of newlines, indentation and ? $\endgroup$ – CMCDragonkai Apr 13 '16 at 6:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.